Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The following interesting question(s) have been raised by Martin Escardó on the Agda mailing list and the constructive-news list.
Is there a constructive proof that there is no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$?
Is there a constructive proof that given any function $H\colon \mathbb{N}^\mathbb{N} \to \mathbb{N}$, there exist functions $f,g\colon \mathbb{N}\to\mathbb{N}$ and $k\in \mathbb{N}$ such that $H(f)=H(g)$ but $f(k)\neq g(k)$?
Both are obviously true assuming classical logic, and the latter can apparently also be proven if one assumes “continuity principles”. As far as counterexamples go, in the effective topos, $\mathbb{N}^\mathbb{N}$ is a subquotient of $\mathbb{N}$, but not a subobject of it. In D4.1.9 of the Elephant there is a Grothendieck topos in which $\mathbb{N}^\mathbb{N}$ is a subquotient of $\mathbb{N}$, namely the classifying topos of the theory of a partial surjection from $\mathbb{N}$ to $\mathbb{N}^\mathbb{N}$ – but afterwards he explains why that approach wouldn’t work for an injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, and how one can prove constructively that there is no surjection $\mathbb{N}\to \mathbb{N}^\mathbb{N}$.
It seems like surely the answer to (1), at least, should be known… but I don’t know it.
The diagonalisation argument proves that there is no surjection from $S$ to $V^S$, given a nontriviality hypothesis on $V$ (which is satisfied for $\mathbb{N}$). By the axiom of choice, there is thus no injection from $V^S$ to $S$, but of course that’s not constructive. The most famous application of diagonalisation (besides to $\mathbb{R}$, which is not constructively an example of this version anyway) is to the power set, and there one can construcitvely (but impredicatively) turn the nonexistence of a surjection from $\mathcal{P}S$ to $S$ into the nonexistence of an injection from $S$ to $\mathcal{P}S$; however, the argument cannot be generalised. (It’s a neat argument, on the Lab at Cantor’s Theorem.)
Andrej Bauer (et al) seem to have shown that the theorem (nonexistence of an injection) fails in certain realisability toposes. I’ve added this result to Cantor’s theorem and LPO (since the existence of such an injection, which holds there, implies $LPO$ even though it contradicts $EM$).
Thanks! I noticed Andrej’s post about this yesterday. It’s very interesting! I’m curious about what other “ominous” facts might hold in the realizability topos in question.
1 to 4 of 4