Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2011

    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: H\colon \mathbb{N}^\mathbb{N} \to \mathbb{N}, there exist functions f,g:f,g\colon \mathbb{N}\to\mathbb{N} and kk\in \mathbb{N} such that H(f)=H(g)H(f)=H(g) but f(k)g(k)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.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJun 2nd 2011
    • (edited Jun 2nd 2011)

    The diagonalisation argument proves that there is no surjection from SS to V SV^S, given a nontriviality hypothesis on VV (which is satisfied for \mathbb{N}). By the axiom of choice, there is thus no injection from V SV^S to SS, 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 𝒫S\mathcal{P}S to SS into the nonexistence of an injection from SS to 𝒫S\mathcal{P}S; however, the argument cannot be generalised. (It’s a neat argument, on the Lab at Cantor’s Theorem.)

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeJun 17th 2011

    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 LPOLPO even though it contradicts EMEM).

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 18th 2011

    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.