Uncountability in intuitionistic logic

I've read snippets here and there that inside intuitionistic logic, uncountable can be a subset of the naturals ?

Given any sequence alleged enumeration e : Integer -> (Integer -> Bool), e will miss the sequence contra i = not (e i i). Hence, we cannot enumerate the type in Haskell.

I understand this argument, and yet, I am uncomfortable with it. I'm not sure when to think "inside the model" versus "outside the model". This seems to imply that things inside the model can believe as absurd facts as they want, perhaps something even like powerset(X) = X? How should one think about the difference between what happens 'inside' and 'outside'?

1. I have been picking up fragmentary references to the weirdness of intuitionistic logic (relative to, say, ZFC) here and there. I'm unaware of a textbook that lays out these results in an orderly fashion. Can I please have a textbook recommendation?

I tried to address the questions you raise in "Five stages of accepting constructive mathematics".

And here are some textbooks:

1. Constructive analysis by D. Bridges and E. Bishop is the "bible" of constructive mathematics.
2. Varieties of constructive mathematics by D. Bridges and F. Richman considers several varieties of constructive mathematics, and discusses some of the pathologies and niceties that they possess.
3. Constructivism in mathematics (volumes 1 and 2) by D. van Dalen and A. Troelstra provides an in-depth treatment of constructive mathematics.
• Hm, is there a textbook reference in the document? If so, could the name of the textbook be appended into the answer? I think that's preferred on stackexchange, since link rot happens on the internet :) Aug 26 '20 at 14:42
• Textbook that accomplishes what precisely? Aug 26 '20 at 14:44
• A textbook that describes constructive mathematics and meta-theoretic questions that arise. Something like "constructive set theory"? I'm not sure what I'm asking for, but I'm imagining a book that perhaps covers these notions of "constructive set theory", "constructive real numbers", ... Aug 26 '20 at 14:48
• Ok, I suggested some. Aug 26 '20 at 14:50

Take the axioms of ZFC and let's assume that ZFC is consistent. By the Löwenheim-Skolem Theorem Downwards (as a corollary to the Completeness Theorem for First-Order Predicate Logic) there is a model $$\mathfrak{M}$$ of ZFC that is countable (as ZFC is formulated with just a single non logical symbol). So, when you look from outside into this model, you can easily see that it is countable. However, when you are working within this model, you still have $$\omega$$ and you still have stuff like $$\mathfrak{M} \models (\omega, 0^\omega, S^\omega) \models^\mathfrak{M} PA$$, so $$\mathfrak{M}$$ proves that $$\omega$$ together with an appropriate constant and an appropriate function are a model of the Peano Axioms. You also have theorems like $$\mathfrak{M} \models |P(\omega)| > |\omega|$$, iterated as much as you want, so $$\mathfrak{M}$$ still knows that there are more sets (although from the outside, you can see that actually $$|\omega^\mathfrak{M}| = |\mathfrak{M}|$$). And $$\mathfrak{M}$$ does not know that it missed any $$w \subset \omega$$.
We can prove from ZFC that a set is always smaller than it's power set, so no model (still relying on ZFC being consistent) will prove that $$X = P(X)$$. However, there are weird models. By the First Incompleteness Theorem of Gödel we know that if ZFC is consistent, then $$ZFC \not \models Con(ZFC)$$ and even worse, in that case $$ZFC + \neg Con(ZFC) \not \models \bot$$, i.e. ZFC and the assumption that it is not consistent has a model as well.