Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeJun 2nd 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe following interesting question(s) have been raised by Martin Escardó on the Agda mailing list and the constructive-news list. 1. Is there a constructive proof that there is no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$? 1. 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 sub*quotient* 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 following interesting question(s) have been raised by Martin Escardó on the Agda mailing list and the constructive-news list.

   1. Is there a constructive proof that there is no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$?

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

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeJun 2nd 2011
   • (edited Jun 2nd 2011)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe 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]].)

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

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeJun 17th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexAndrej 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$).

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

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJun 18th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks! 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.

   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.