<p>I tried to address the questions you raise in &quot;<a href="http://dx.doi.org/10.1090/bull/1556" rel="nofollow noreferrer">Five stages of accepting constructive mathematics</a>&quot;.</p>
<p>And here are some textbooks:</p>
<ol>
<li><a href="https://www.springer.com/gp/book/9783642649059" rel="nofollow noreferrer">Constructive analysis</a> by D. Bridges and E. Bishop is the &quot;bible&quot; of constructive mathematics.</li>
<li><a href="https://books.google.si/books/about/Varieties_of_Constructive_Mathematics.html?id=oN5nsPkXhhsC&amp;redir_esc=y" rel="nofollow noreferrer">Varieties of constructive mathematics</a> by D. Bridges and F. Richman considers several varieties of constructive mathematics, and discusses some of the pathologies and niceties that they possess.</li>
<li><a href="https://books.google.si/books?id=-tc2qp0-2bsC&amp;printsec=frontcover&amp;dq=constructivism+in+mathematics&amp;hl=en&amp;sa=X&amp;ved=2ahUKEwjT2qjDjrnrAhUwNOwKHejXBB0Q6wEwAHoECAMQAQ#v=onepage&amp;q&amp;f=false" rel="nofollow noreferrer">Constructivism in mathematics (volumes 1 and 2)</a> by D. van Dalen and A. Troelstra provides an in-depth treatment of constructive mathematics.</li>
</ol>

CC BY-SA 4.0
2020-08-26T14:42:59.323Z
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 :)
Siddharth Bhat
CC BY-SA 4.0
2020-08-26T14:44:48.093Z
Textbook that accomplishes what precisely?
Andrej Bauer
CC BY-SA 4.0
2020-08-26T14:48:20.207Z
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", ...
Siddharth Bhat
CC BY-SA 4.0
2020-08-26T14:50:17.090Z
Ok, I suggested some.
Andrej Bauer
CC BY-SA 4.0
2020-08-26T13:42:49.423Z
2020-08-26T14:49:38.980Z
2020-08-26T14:49:38.980Z
Andrej Bauer
<p>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:</p>
<p>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 <span class="math-container">$\mathfrak{M}$</span> of ZFC that is countable (as ZFC is formulated with just a single non logical symbol).
So, when you look from <em>outside into</em> this model, you can easily see that it is countable.
However, when you are working within this model, you still have <span class="math-container">$\omega$</span> and you still have stuff like <span class="math-container">$\mathfrak{M} \models (\omega, 0^\omega, S^\omega) \models^\mathfrak{M} PA$</span>, so <span class="math-container">$\mathfrak{M}$</span> proves that <span class="math-container">$\omega$</span> together with an appropriate constant and an appropriate function are a model of the Peano Axioms. You also have theorems like <span class="math-container">$\mathfrak{M} \models |P(\omega)| &gt; |\omega|$</span>, iterated as much as you want, so <span class="math-container">$\mathfrak{M}$</span> still knows that there are more sets (although from the <em>outside</em>, you can see that actually <span class="math-container">$|\omega^\mathfrak{M}| = |\mathfrak{M}|$</span>). And <span class="math-container">$\mathfrak{M}$</span> does <em>not know</em> that it missed any <span class="math-container">$w \subset \omega$</span>.</p>
<p>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).</p>
<p>That's one anomaly, regarding the second one you mentioned:</p>
<p>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 <span class="math-container">$X = P(X)$</span>. However, there are weird models. By the First Incompleteness Theorem of Gödel we know that if ZFC is consistent, then <span class="math-container">$ZFC \not \models Con(ZFC)$</span> and even worse, in that case <span class="math-container">$ZFC + \neg Con(ZFC) \not \models \bot$</span>, i.e. ZFC and the assumption that it is not consistent has a model as well.</p>
<p>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.</p>
<p>There are a lot of these questions and discussions around these topics on MathOverflow, e.g. here:
<a href="https://mathoverflow.net/questions/77628/question-about-godels-2nd-theorem">https://mathoverflow.net/questions/77628/question-about-godels-2nd-theorem</a></p>

CC BY-SA 4.0
2020-08-26T13:25:29.900Z
2020-08-26T13:25:29.900Z
Fabian
<p>I've read snippets here and there <a href="http://comonad.com/reader/2011/searching-infinity/#comment-92198" rel="nofollow noreferrer">that inside intuitionistic logic, uncountable can be a subset of the naturals</a> ?</p>
<ol>
<li>What is the correct intuition to think about this? Andrej Bauer replied above, saying that:</li>
</ol>
<blockquote>
<p>Given any sequence alleged enumeration <code>e : Integer -&gt; (Integer -&gt; Bool)</code>, <code>e</code> will miss the sequence <code>contra i = not (e i i)</code>. Hence, we cannot enumerate the type in Haskell.</p>
</blockquote>
<p>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 <code>powerset(X) = X</code>? How should one think about the difference between what happens 'inside' and 'outside'?</p>
<ol start="2">
<li>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?</li>
</ol>

<lo.logic><type-theory><haskell>
Uncountability in intuitionistic logic
Siddharth Bhat
# Uncountability in intuitionistic logic

(Asked by: username_0 on 2020-08-26)

I've read snippets here and there [that inside intuitionistic logic, uncountable can be a subset of the naturals](http://comonad.com/reader/2011/searching-infinity/#comment-92198) ?

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'?

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

**Tags:** lo.logic, type-theory, haskell

---

## 2 answers

### Answer by username_1 on 2020-08-26. Score: 3 | Accepted answer

I tried to address the questions you raise in "[Five stages of accepting constructive mathematics](http://dx.doi.org/10.1090/bull/1556)".

And here are some textbooks:

1. [Constructive analysis](https://www.springer.com/gp/book/9783642649059) by D. Bridges and E. Bishop is the "bible" of constructive mathematics.
2. [Varieties of constructive mathematics](https://books.google.si/books/about/Varieties_of_Constructive_Mathematics.html?id=oN5nsPkXhhsC&redir_esc=y) 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)](https://books.google.si/books?id=-tc2qp0-2bsC&printsec=frontcover&dq=constructivism+in+mathematics&hl=en&sa=X&ved=2ahUKEwjT2qjDjrnrAhUwNOwKHejXBB0Q6wEwAHoECAMQAQ#v=onepage&q&f=false) by D. van Dalen and A. Troelstra provides an in-depth treatment of constructive mathematics.

> **Comments:**
> **username_0**: 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 :)  
> **username_1**: Textbook that accomplishes what precisely?  
> **username_0**: 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", ...  
> **username_1**: Ok, I suggested some.  

---

### Answer by username_2 on 2020-08-26. Score: 2

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>


---

