Return to Answer

[Update 2015-04-15: The preprint The countable reals is now available.]

A set $A$ is uncountable if it is not countable. A stronger property is sequence-avoiding: for every sequence $\mathbb{N} \to A$ there is an element of $A$ that is not a term of the sequence.

[Update 2024-04-15: The preprint The countable reals is now available.]

A set $A$ is uncountable if it is not countable. For an inhabited set, a stronger property is sequence-avoiding: for every sequence $\mathbb{N} \to A$ there is an element of $A$ that is not a term of the sequence.

Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.

[Update 2015-04-15: The preprint The countable reals is now available.]

Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.

Proof. Cantor's diagonal method is constructive. Given $f : \mathbb{N} \to \lbrace 0, 1\rbrace^\mathbb{N}$, the sequence $n \mapsto 1 - f(n)(n)$ differs from $f(n)$ in the $n$-th place. Similarly, given $g : \mathbb{N} \to \mathcal{P}(\mathbb{N})$, the set $\lbrace n \in \mathbb{N} \mid n \notin f(n) \rbrace$ differs from $f(n)$ at $n$. $\Box$

It has also been known since at least the 1980's that in the effective topos $\mathbb{R}_d$ is subcountable and sequence-avoiding.

Proof. Cantor's diagonal method is constructive. Given $f : \mathbb{N} \to \lbrace 0, 1\rbrace^\mathbb{N}$, the sequence $n \mapsto 1 - f(n)(n)$ differs from $f(n)$ in the $n$-th place. Similarly, given $g : \mathbb{N} \to \mathcal{P}(\mathbb{N})$, the set $\lbrace n \in \mathbb{N} \mid n \notin f(n) \rbrace$ differs from $g(n)$ at $n$. $\Box$

It has also been known since at least the 1980s that in the effective topos $\mathbb{R}_d$ is subcountable and sequence-avoiding.