Subcountability under realizability
In constructive mathematics, a set a is discrete if it satisfies \(x,y\in a\to x=y\vee x\neq y.\) A set is countable if it is the range of a function on the integers, and subcountable if it is a subset of a countable set. Unlike in classical mathematics, subcountable sets need not be countable; even Baire space might be subcountable (e.g. if Church's thesis CT is true). All known discrete sets are subcountable, and if CT holds so are separable metric spaces. So the problem was raised whether it is consistent to assume (SCDS) all discrete sets are subcountable, or perhaps even the stronger (SCMS) all metric spaces are subcountable. (It is stronger because a discrete set can be given the discrete metric.) The paper shows the consistency of both these principles with intuitionistic ZF set theory IZF. The method is straightforward: the principles turn out to be recursively realized. The proof itself is not quite straightforward, requiring a clever ``reflection in which the realizer of \(x,y\in a\to x=y\vee x\neq y\) is shown to contain an object realized to be a ``subcounting function of a. (Lemma 2).
- Subbase countable compact- ness
- Realcompact subspaces
- The number of countable models in realizability toposes
- Subfields of a real closed field of countable codimension
- Borel subrings of the reals
- scientific article; zbMATH DE number 427681
- scientific article; zbMATH DE number 2103326
- Realizability and recursive set theory
- scientific article; zbMATH DE number 3337966
- Countable subsets of Suslinian continua
This page was built for publication: Subcountability under realizability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1098849)
