Subcountability under realizability (Q1098849)

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).