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

What is the correct intuition to think about this? Andrej Bauer replied above, saying that:


Given any sequence alleged enumeration e : Integer -&gt; (Integer -&gt; 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 &quot;inside the model&quot; versus &quot;outside the model&quot;. 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'?

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 &quot;Five stages of accepting constructive mathematics&quot;.
And here are some textbooks:

Constructive analysis by D. Bridges and E. Bishop is the &quot;bible&quot; of constructive mathematics.
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.
Constructivism in mathematics (volumes 1 and 2) by D. van Dalen and A. Troelstra provides an in-depth treatment of constructive mathematics.