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

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

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?

2 Answers 2


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.
  • $\begingroup$ 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 :) $\endgroup$ Commented Aug 26, 2020 at 14:42
  • 1
    $\begingroup$ Textbook that accomplishes what precisely? $\endgroup$ Commented Aug 26, 2020 at 14:44
  • $\begingroup$ 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", ... $\endgroup$ Commented Aug 26, 2020 at 14:48
  • 1
    $\begingroup$ Ok, I suggested some. $\endgroup$ Commented Aug 26, 2020 at 14:50

I can't give you a (easily translatable) answer to the question regarding Haskell and the types, but the following might help you since you already mentioned ZFC:

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

To have an easy way of grasp this, consider the following game: I challenge you to give me a set of natural numbers and I will honestly answer if I have thought about this set before. You win if you find a set that I didn't think about. Here's my winning tactic: I just think about all sets that are describable in our language. Since the cardinality of the language is countable, these are only counably many setsm that can be described with it. So you will not be able to come up with a set I haven't thought about and still, you and I both know that I thought about 0% of all sets (more or less applying measure theory here).

That's one anomaly, regarding the second one you mentioned:

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.

These models can grow as weird as you want them to. What you want to do in these cases is you want to look at models/ theories that have the property that for any sentence they prove about the natural numbers as you know them from the outside, that this sentence still holds.

There are a lot of these questions and discussions around these topics on MathOverflow, e.g. here: https://mathoverflow.net/questions/77628/question-about-godels-2nd-theorem


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.