ℕ surjects onto ℝ. Subsets of ℕ surject onto ℕ^ℕ. ℕ^ℕ injects into ℕ. All that.

subcountability.tex

Shownotes to the video:
https://youtu.be/q-mjO9Uxvy0

For a related and relevant video constructive logic basics and upshots is at
https://youtu.be/-lPrjPHElik
For a related and relevant discussion on computably enumerable sets and their compliments, see this 4yo video
https://youtu.be/Ox0tD58DTG0
For some of the non-theorems in the list it helps to understand \Pi_0^2-complete sets.
The references video on how the Axiom of Choice and Regularity each imply LEM is at
https://youtu.be/2EOW23uVcRA

===== ℕ surjects onto ℝ. Or subsets of ℕ surject onto ℕ^ℕ. Or ℕ^ℕ injects into ℕ. All that. =====
==== Bauer-Hansen paper - The Countable Reals ====
Previous ℕ^ℕ into ℕ paper:
https://math.andrej.com/wp-content/uploads/2011/06/injection.pdf
April ℕ onto ℝ paper:
https://arxiv.org/abs/2404.01256
2022 talk on the latter:
https://www.youtube.com/live/4CBFUojXoq4

Bauer-Hansen topos doesn't validate
$\bullet$ LEM
$\bullet$ countable choice
$\bullet$ every real has a digit expansion

but validates
$\bullet$ Dedekind reals are countable (epi from ${\mathbb N}$ to ${\mathbb R}$)
$\bullet$ $\forall (x\in{\mathbb R}). (x\le 0\lor 0\le x)$, lesser limited principle of omniscience, LLPO
$\bullet$ intermediate value theorem, IVT
$\bullet$ Brouwer’s fixed-point theorem
$\bullet$ Markov's principle
And
$\bullet$ all real-valued maps are continuous
$\bullet$ ...

Topics overview:
$\bullet$ 45 pages
$\bullet$ pp. 1-5     some intuitionistic math backround
$\bullet$ pp. 6-9     oracle-computable maps and Miller sequences
$\bullet$ pp. 10-15   Chapter "3. Parameterized partial combinatory algebras"
$\bullet$ pp. 16-...  Chapter "4. Parameterized realizability"
$\bullet$ pp. 26-...  Chapter "5. The real numbers", Dedekind reals discussion, especially in a INTEGRATION_SCHEME_OPTIONS
$\bullet$ p. 30       The Cauchy reals
$\bullet$ pp 33-44    Chapter "5.  A topos with countable reals", discussion of LLPO and other properties
$\bullet$ p. 45       References

==== What holds constructively ====
Positive:
$\bullet$ We have $X = X$ and so $X\le X$ i.e. any set $X$ injects into itself ... via the identity function
$\bullet$ We have $X < {\mathcal P}X$, i.e. any set $X$ injects onto its powerset, e.g. $x\mapsto \{x\}$ (very monad'ish)
$\bullet$ We have $\{0,1\}^X \le {\mathcal P}X$ ... via $f\mapsto\{n\in{\mathbb N}\mid f(n)=1\}$
$\bullet$ We have ${\mathbb N} \le \{0,1\}^{\mathbb N}$ ... e.g. as $n=m$ is decidable, consider $n\mapsto (m\mapsto 1$ if $n=m$ else $0)$)
$\bullet$ We have $\{0,1\}^{\mathbb N} \le {\mathbb N}^{\mathbb N}$ ... because $\{0,1\}\subset{\mathbb N}$  
Negative:
$\bullet$ No set $X$ surjects onto ${\mathcal P}X$
... For a candidate $h$, consider $\{x\in X\mid x\notin f(x)\}$ (simplest version of the Cantor proof, even only uses bounded Separation)
$\bullet$ We have ${\mathcal P}X\nleq X$, i.e. no powerset inject into its base set
... For a candidate $h$, consider $\{x\in X\mid \exists(S\in{\mathcal P}X). x=h(S)\land x\notin S\}$
$\bullet$ ${\mathbb N}$ does not surject onto $\{0,1\}^{\mathbb N}$ ... For a candidate $h$, consider $n\mapsto h(n)(n)+d$ for non-zero $d$
$\bullet$ Indeed no index set $I\subset {\mathbb N}$ surjects onto ${\mathcal P}{\mathbb N}$ (it's actually $\omega$-productive.)
With countable choice (or LEM)
$\bullet$ ${\mathbb R}_C$ are iso to the ${\mathbb R}_D$, the Dedekind reals (iirc)
$\bullet$ ${\mathbb R}_C$, the Cauchy reals, are Cauchy-complete (iirc even without explicit modulus of convergence)
$\bullet$ The reals are sequence avoiding (see e.g. talk/papers), and thus is uncountable
But...
$\bullet$ The reals may fail to have a digit expansion
$\bullet$ An index set $I\subset {\mathbb N}$ may surject onto ${\mathbb N}^{\mathbb N}$ (and then, $\{0,1\}^{\mathbb N}$ etc.) As noted, this doesn't work for $I={\mathbb N}$. The $I$ will be quite complicated, e.g. $\Pi_2^0$-complete.
(after all, we can enumerate computer programs and $\{0,1\}^{\mathbb N}$ doesn't need to be stuff with anything else.)
$\bullet$ ${\mathcal P}\{0\}$ may be a proper class even when $\{0,1\}^{\{0\}}$ is finite.
In particular, ${\mathcal P}{\mathbb N}$ may be very different than the tamer $\{0,1\}^{\mathbb N}$.
Watch this video.
$\bullet$ In turn, if ${\mathcal P}{\mathbb N}$ is taken to be a propert class, then it's consistent to postulate that all sets $X$ are surjected onto by some $I_X\subset {\mathbb N}$ (Subcountability axiom)
(This works with ${\mathsf{CZF}}$ and notably ${\mathsf{CZF}}$ has a ML1V type theory model. It also works at least for the sets with apartness relation in ${\mathsf{IZF}}$.)
(If you don't got function spaces, then even more is possible. But okay in that case you're basically just doing second order artihemtic, really..)
Bauer papers. Keywords: Realizability topoi, infinite time & oracle Turing machines:
$\bullet$ ${\mathbb N}^{\mathbb N}$ and ${\mathbb R}_D$ may inject into ${\mathbb N}$
(see "An injection from the Baire space to natural numbers")
$\bullet$ ${\mathbb N}$ may surject onto ${\mathbb R}_D$ (different topos, present paper)
There's a bunch more results (some more obvious than others) which of those properties can't happen simultanously
Relatedly:
$\bullet$ Schröder-Bernstein theorem is equivalent to LEM. (Fairly recent result) (Semi-related: See Myhill isomorphism theorem)
$\bullet$ All subsets of finite sets being finite is also equivalent to LEM ... Consider $1$'s subset $\{n\in 1\mid {\mathrm{Con}_T}\}$
$\bullet$ Relatedly, full choice is equivalent to LEM (Diaconescu, see long 2022 video of mine)
$\bullet$ In ${\mathsf{ZF}}$ it's consistent for $X\times X$ to surject onto $\{0,1\}^X$ (Fairly recent result)
Vaguely related sketch of a warning:
$\bullet$ Talk of "definable real" too often unknowingly blends object language and metalanguage. There's a gap between the mere countably many formulas, and the higher order concept of definitions. This is related to countable model of ZFC. (Keywords: Tarksi-undefinability, Math tea argument, pointswise definable models.)

==== Preliminary for the prelude to the review, to avoid any smartypants comments ====
We assume whatever theory we use is sound and consistent.
We have a model for $\mathbb{N}$ and use $0 \neq 1$.
(So that I can use canonical independent statement, and so that I have a canonical decidable statement)
In set theory, we use $0:=\{\}$ and $1:=\{0\}$.

$X\le Y$ ... $\exists f$ that's an injection from $X$ to $Y$,
with the definition of injection (and surjective) function given below.
This is a non-strict partial order, e.g. we can chain those relations.
Over ${\mathsf{ZF}}$, full choice proves this also total, i.e. any two sets can successfully be compared.

$X$ being countable means $\mathbb{N}$ surjects onto $X$.
There's the evident patches for empty sets (use image $X\cup\{X\}$) or speaking of epimorphisms.

We don't "just" do Skolem-paradox tricks in this video.

==== Note on existence and logic ====
Important and interesting to look at the logical structure.
Very roughly:
$\forall\exists$ ... Relation-like
$\forall\exists!$ ... Function-like
$\exists\forall$ ... global bound-like
$\exists!\forall$ ... unique global bound-like

Note: Unique existence $\exists!x. Q(x)$ ... $\exists x. \forall y. \big(y=x \leftrightarrow Q(y)\big)$
Already global bound-like

$\bullet$ Function ... $\forall (x\in X).\, \exists! (y\in Y). f(x)=y$

Main point: Which definition consistute a function according to your theory depends on the inference rules and  axioms of your theory.

$\bullet$ Surjection onto $Y$ ... $\forall (y\in Y). \exists(x\in X). y=f(x)$

$\bullet$ Injection ... $\forall(x, z\in X). f(x)=f(z)\to x=z$

==== Note on set theory ====
Comprehension with some predicate $Q$:
$A$ some set $\Longrightarrow$ $A_Q:=\{x\in A\mid Q(x)\}$ another set.

In some setty model: Everything is a set.
Any function term is a subset of the set of pairs $X\times Y$ and function-value-equality really means
$f(x)=y$ $\Leftrightarrow$ $\langle x, y\rangle \in f$
Function space $X\to Y$, modeled as a set called $Y^X$ ... is some subset of ${\mathcal P}(X\times Y)$

Candidate for characteristic function on $A$ deciding $Q$:
${\mathrm X}_Q^A:=\big\{\langle x,y\rangle \in A\times \{0,1\} \mid (Q(x)\land y=1) \lor (\neg Q(x)\land y=0)\}$

For any $a\in A$ one has
$Q(a) \ \leftrightarrow\, \langle a, 1\rangle\in {\mathrm X}_Q^A$
$\neg Q(a) \ \leftrightarrow\, \langle a, 0\rangle\in {\mathrm X}_Q^A$

So for any $a\in A$ one has
$\big(Q(a) \lor \neg Q(a)\big)\ \leftrightarrow\ \exists!(y\in\{0,1\}). \langle a, y\rangle\in {\mathrm X}_Q^A$.

So iff $Q$ is decidable (for all $x\in A$), then ${\mathrm X}_Q^A$ models a characteristic function.

Example:
$A={\mathbb N}$ and $Q(n):=\exists m. (n=7\cdot m)$,
i.e. "The natural number $n$ is a multiple of seven."
Decidability statement
$\forall (n\in \mathbb N).\ \big(\exists m. (n=7\cdot m) \big)\lor \big(\neg \exists m. (n=7\cdot m)\big)$

Rationale why this holds for any $n$ in the standard model (and e.g. the finite Von Neumann ordinals):
All numbers are of the form $SSS\cdots SSS0$ and $n=7\cdot m$ can be decided by length comparison.
If $m\ge n$, say, it will always be false and otherwise we have a finite number to check.

This predicate has a python implementation:
<code>def q_witness(n):
    for m in range(n):  # Range could be optimized
        if n == 7 $\bullet$ m:
            return m
    return None

def X(n):
    return q_witness(n) is not None
</code>

LEM $\Longrightarrow$ Your classical theory proves all function candidates of the above
${\mathrm X}_Q^A:=\big\{p \in A\times \{0,1\} \mid (Q(x)\land y=1) \lor (\neg Q(x)\land y=0)\}$
to be functions (not dependent on there being a python implementation)

==== Note on Gödel ====
For an enumeration of all your proofs/programs of your theory $T$, consider the statement saying "n is a proof proving '0=1'",
$P(n):={\mathrm{Prf}_T(n, \lceil 0=1\rceil)}$
This is primitive recursive, i.e. we can check for any $n$. Nice.
But
${\mathrm{Con}}_T:=\neg\exists n. P(n)$
is unprovable in a consistent theory and further independent in a sound theory.
So a brute force proof search, for the inconsistency $0=1$ and for the negation of its arithmetization ${\mathrm{Con}}_T$, is both futile.

==== Real number equality ====
The (Cauchy) sequence
$a_P(m) := \sum_{n=0}^m\frac{1}{2^n}\cdot(1$ if $P(n)$ else $0)$
looks like $0\in{\mathrm Q}$ for every $m$.
So the the real number $p:=\lim_{m\to \infty} a_P(m)$ is provably extremely tiny.
But $p=0$ (here now $0\in{\mathbb R}$) is independent, also for e.g. $T={\mathrm{ZFC}}$
Hence
$\forall (x\in{\mathbb R}).(x=0\lor \neg(x=0))$
won't be constructively provable either.

==== Note on Turing ====
See
https://youtu.be/-lPrjPHElik?si=6Ju3aGgmYJscbuGi

Somewhat more generally (see recursion theory),
we have $Q$'s such that $\{n\in {\mathbb N}\mid Q(n)\}$ is not decidable and so has no programmatic implementation
E.g. that's the case for
$M(n)$ ... its not the case that the $n$'th program ever halts.

And so
$\forall (n\in {\mathbb N}). M(n)\lor \neg M(n)$
is not constructively provable.

So
${\mathrm X}_M^{\mathbb N}:=\big\{p \in {\mathbb N}\times \{0,1\} \mid (M(x)\land y=1) \lor (\neg M(x)\land y=0)\}$
which has
${\mathrm X}_M^{\mathbb N}\ \subset\ {\mathbb N}\times \{0,1\}$

is not provably a function, i.e.

$\nvdash {\mathrm X}_M^{\mathbb N} \in \{0,1\}^{\mathbb N}$


The set of indices of non-halting programs, $\{n\in {\mathbb N}\mid M(n)\}$, will also not be countable.
In particular, not all subsets of ${\mathbb N}$ are countable.


Notably,
$\{0,1\}^{\mathbb N} \hookrightarrow {\mathcal P}{\mathbb N}$
i.e.
$\{0,1\}^{\mathbb N} \le {\mathcal P}{\mathbb N}$
But the other way around is immediately equivalent to LEM.

===== Cauchy reals, Dedekind reals, MacNeil reals, etc. =====
Models of the reals (a (pseudo-)ordered collection extending the rationals with some other nice properties):
$\bullet$ Cauchy sequence equivalent classes ${\mathbb R}_C$
$\bullet$ Dedekind cuts ${\mathbb R}_D$
$\bullet$ ...

Those are very different w.r.t. to properties other than the arithmetic/topology of the reals, etc.
E.g., say in $\mathsf{ZF}$, typically $|7_{{\mathbb R}_C}| = |{\mathbb R}|$
while $|7_{{\mathbb R}_D}| = |{\mathbb N}|$

Only if you got countable choice, much of their outside properties collapses/unified.