<p>To answer very directly: You have a <em>constructive proof</em> in Coq but it is not the case that the <code>enum : nat -&gt; nat</code> is assumed (in Coq) to be computable. In a sense, it's a constructive proof about a larger domain of things than can actually be constructed in Coq.</p>
<p>Andrej's answer gives a deeper mathematical understanding of why the map should or shouldn't be assumed to be computable. But in Coq, it isn't.</p>

CC BY-SA 4.0
2023-03-23T20:44:21.460Z
2023-03-23T20:44:21.460Z
ezrakilty
<p>What you actually prove is that there is no function that enumerates all the functions that takes a natural number and returns a natural number. The proof is constructive in the sense that in order to prove this fact, you explicitly construct a function <code>f</code> that is not reached. You get a witness.</p>
<pre><code>Definition surj {A B : Type} (f : A -&gt; B) :=
  forall b, exists a, f a = b.

Theorem Cantor_theorem :
  forall (enum : nat -&gt; nat -&gt; nat), ~ surj enum.
Proof.
  intros enum enum_surj.
  pose (f n := S (enum n n)).
  destruct (enum_surj f) as [n f_in_enum].
  assert (enum n n = f n) as H_eq by (rewrite &lt;- f_in_enum ; reflexivity).
  assert (enum n n &lt;&gt; f n) as H_neq by (intros _ ; destruct (n_Sn (enum n n) H_eq)).
  contradiction.
Qed.
<span class="math-container">```</span>
</code></pre>

CC BY-SA 4.0
2023-03-11T08:13:44.613Z
2023-03-11T08:13:44.613Z
lolo
<p>First, let me say that &quot;constructive&quot; does <em>not imply</em> &quot;all maps are Turing computable&quot;. It means “no excluded middle and axiom of choice were used“. In constructive mathematics the statement</p>
<blockquote>
<p>For every <span class="math-container">$f : \mathbb{N} \to \mathbb{N}$</span> there exists a Turing machine <span class="math-container">$M$</span> that computes <span class="math-container">$f$</span></p>
</blockquote>
<p>is known as <em>formal Church's thesis</em>. Let us abbreviate it with <span class="math-container">$\mathrm{CT}$</span>.</p>
<blockquote>
<p><strong>Theorem:</strong></p>
<ol>
<li>Constructive mathematics does <strong>not</strong> prove <span class="math-container">$\mathrm{CT}$</span>.</li>
<li>Constructive mathematics does <strong>not</strong> prove <span class="math-container">$\neg \mathrm{CT}$</span>.</li>
</ol>
</blockquote>
<p><em>Proof.</em> The first statement holds because classical set theory is a model of constructive mathematics in which <span class="math-container">$\neg\mathrm{CT}$</span> is valid. The second statement holds because the effective topos is a model of constructive mathematics in which <span class="math-container">$\mathrm{CT}$</span> is valid. <span class="math-container">$\Box$</span></p>
<p>The upshot of this is that in a constructive argument you <em>cannot</em> assume that all functions are computable. If you do that, you are not doing constructive mathematics anymore, but rather something like <a href="https://plato.stanford.edu/entries/mathematics-constructive/#RecuConsMath" rel="noreferrer">Russian recursive mathematics</a> which assumes additional axioms (<span class="math-container">$\mathrm{CT}$</span>, countable choice, Markov's principle).</p>
<p>Your question then really is: Why is the usual proof of uncountability of <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span> valid in Russian recursive mathematics, given that there are only countably many Turing machines computing functions <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span>?</p>
<p>The answer is: you are mixing two different kinds of mathematics:</p>
<ol>
<li><p>In <strong>classical mathematics</strong> there are countably many Turing machines computing functions <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span>.</p>
</li>
<li><p>In Russian constructivism there are <strong>uncountably many</strong> such Turing machines.</p>
</li>
</ol>
<p>How is this possible? First, note that in constructive mathematics it can well happen that a subset of a countable set is uncountable, see the explanation below. Second, let
<span class="math-container">$$
T = \{n \in \mathbb{N} \mid \text{$n$ encodes a TM computing a map $\mathbb{N} \to \mathbb{N}$}\}
$$</span>
be the set of indices of Turing machines computing maps <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span>. There is no constructive proof that <span class="math-container">$T$</span> is countable. In fact, <span class="math-container">$T$</span> is <em>not</em> computably enumerable, which in Russian recursive mathematics means precisely that it is not countable.</p>
<p>The moral of the story is: the diagonalization proof of uncountabilty of <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span> is constructive, but your understanding of &quot;countable&quot; is not.</p>
<p>P.S. The set of indices of <em>all</em> Turing machines is countable, constructively.</p>
<p>P.P.S. The OP asked about the fact that &quot;subsets of countable sets are countable&quot; only holds classically. Here's why.</p>
<p><strong>Theorem:</strong> <em>If every subset of <span class="math-container">$\mathbb{N}$</span> is countable and Markov's principle holds then excluded middle holds.</em></p>
<p><em>Proof.</em> See Proposition 2.6 in <a href="https://arxiv.org/pdf/1804.00427.pdf" rel="noreferrer">this paper</a>. Briefly, given any truth value <span class="math-container">$p$</span>, let <span class="math-container">$S = \{n \in \mathbb{N} \mid n = 0 \lor p \}$</span> and let <span class="math-container">$e : \mathbb{N} \to S$</span> be an enumeration of <span class="math-container">$S$</span>, which exists by assumption. Then <span class="math-container">$p \Leftrightarrow \exists k \in \mathbb{N} .\, f(k) \neq 0$</span>. By Markov's principle <span class="math-container">$\exists k \in \mathbb{N} .\, f(k) \neq 0$</span> is <span class="math-container">$\neg\neg$</span>-stable, therefore <span class="math-container">$\neg\neg p \Rightarrow p$</span>. We showed that every truth value is <span class="math-container">$\neg\neg$</span>-stable, therefore excluded middle holds too. <span class="math-container">$\Box$</span></p>
<p>I do not know how to get rid of the assumption of Markov's principle. In any case, the theorem shows that one cannot have a purely constructive proof of &quot;every subset of <span class="math-container">$\mathbb{N}$</span> is countable&quot;, because Markov's principle is consistent with constructive mathematics.</p>
<p><strong>Supplemental:</strong> Douglas Bridges pointed out in this <a href="https://groups.google.com/g/constructivenews/c/xXr8PX8c06Q/m/vevJSKTaCgAJ" rel="noreferrer">constructivenew post</a> that Markov principle cannot be eliminated.</p>

CC BY-SA 4.0
2023-03-11T13:22:10.283Z
in the Proof, do you mean not CT in the last sentence?
Dima Pasechnik
CC BY-SA 4.0
2023-03-11T14:17:05.483Z
> but your understanding of "countable" is not.
My understanding that "countable set `A`" means "there exists a bijection between `nat` and `A`". And the proof in the OP states that `nat -> (nat -> nat)` has no bijection. So, it states that `nat -> nat` functions are not countable. 

The question is: does it mean that `(nat -> nat) : Set` in Coq speaks about all `nat -> nat` maps including those which can not be computed by a Turing machine?
Zazaeil
CC BY-SA 4.0
2023-03-11T14:21:43.473Z
The standard definition of countable in constructive mathematics is: $A$ is countable when there is a surjection $\mathbb{N} \to 1 + A$. When $A$ is inhabited this is equivalent to there being a surjection $\mathbb{N} \to A$. Requiring a bijection is too strong.
Andrej Bauer
CC BY-SA 4.0
2023-03-11T14:22:59.247Z
In any case, whatever notion you're using, the fact remains that you assumed that a certain subset of $\mathbb{N}$ is countable, when in fact this cannot be proved constructively.
Andrej Bauer
CC BY-SA 4.0
2023-03-11T14:23:59.367Z
@DimaPasechnik: thanks for the comment, I fixed the proof (but it was the first occurrence that needed a negation).
Andrej Bauer
CC BY-SA 4.0
2023-03-11T14:26:04.343Z
@AndrejBauer thanks, I will try to find more about the "Have you tried to prove constructively that a subset of a countable set is countable?". If you can, please update your post and add few more words about it and I will accept it.
Zazaeil
CC BY-SA 4.0
2023-03-11T14:26:32.110Z
A few more words about what?
Andrej Bauer
CC BY-SA 4.0
2023-03-11T14:26:55.463Z
It is really surprising that subset of naturals numbers can not be proved to be countable constructively.
Zazaeil
CC BY-SA 4.0
2023-03-11T14:45:27.420Z
Ok, I wrote a little more. Regarding an improvement of the theorem in the P.P.S., we shall see what comes up [in this Mathstodon thread](https://mathstodon.xyz/@andrejbauer/110005159861304000).
Andrej Bauer
CC BY-SA 4.0
2023-03-11T16:32:18.180Z
@AndrejBauer - oops, apologies - some 40 years ago I managed to pass an exam where a textbook was Maltsev's "Algorithms and recursive functions". I guess it was long evaporated from my brain :-)
Dima Pasechnik
CC BY-SA 4.0
2023-03-13T07:06:51.480Z
Douglas Bridges pointed out on constructivenews that Markov principle is necessary. I think this resolves all questions.
Andrej Bauer
CC BY-SA 4.0
2023-03-11T12:13:25.120Z
2023-03-13T07:06:16.890Z
2023-03-13T07:06:16.890Z
Andrej Bauer
<p>Here is a Coq proof I've came up with:</p>
<pre><code>Definition inj {A B : Type} (f : A -&gt; B) :=
  forall b, exists a, f a = b.

Definition surj {A B : Type} (f : A -&gt; B) :=
  forall a1 a2, f a1 = f a2 -&gt; a1 = a2.

Definition bij {A B : Type} (f : A -&gt; B) :=
  inj f /\ surj f.

Theorem Cantor_theorem :
  forall (f : nat -&gt; nat -&gt; nat), ~ bij f.
Proof.
  intros enum [H_inj H_surj].
  pose (f := fun n =&gt; S (enum n n)).
  destruct (H_inj f) as [n H_contra_f].
  assert (enum n n = f n) as H_eq by (rewrite &lt;- H_contra_f ; reflexivity).
  assert (enum n n &lt;&gt; f n) as H_neq by (intros _ ; destruct (n_Sn (enum n n) H_eq)).
  contradiction.
Qed.
</code></pre>
<p>I am having hard times to grasp <em>a constructivism</em> here. To my understanding <code>nat -&gt; (nat -&gt; nat)</code> talks only about constructive <code>nat -&gt; nat</code>s rather than an (possible undecidable) arbitrary <code>nat -&gt; nat</code>. For each <em>constructive</em> <code>nat -&gt; nat</code> there must be a corresponding Turing machine that computes it for an arbitrary input <code>n</code>, otherwise it is not constructive (thus is undecidable) by the definition. Moreover, there are countably many Turning machines. At this point I conclude: <em>there are countably many <em>constructive</em> <code>nat -&gt; nat</code>s</em>, which also means: the <code>nat -&gt; nat</code> <em>Coq's <code>Type</code> (due it's constructive nature)</em> describes countably many functions.</p>
<p>Nonetheless, I am wrong: the proof states: those are actually uncountable...</p>
<p>Where am I mistaken? How does &quot;constructivism&quot; reveals itself in this particular example?</p>

CC BY-SA 4.0
2023-03-11T11:53:32.867Z
Your definitions of injective and surjective are switched around.
Andrej Bauer
<coq><calculus-of-constructions><constructive-mathematics>
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
Zazaeil
# Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?

(Asked by: username_0 on 2023-03-10)

Here is a Coq proof I've came up with:
Definition inj {A B : Type} (f : A -> B) :=
  forall b, exists a, f a = b.

Definition surj {A B : Type} (f : A -> B) :=
  forall a1 a2, f a1 = f a2 -> a1 = a2.

Definition bij {A B : Type} (f : A -> B) :=
  inj f /\ surj f.

Theorem Cantor_theorem :
  forall (f : nat -> nat -> nat), ~ bij f.
Proof.
  intros enum [H_inj H_surj].
  pose (f := fun n => S (enum n n)).
  destruct (H_inj f) as [n H_contra_f].
  assert (enum n n = f n) as H_eq by (rewrite <- H_contra_f ; reflexivity).
  assert (enum n n <> f n) as H_neq by (intros _ ; destruct (n_Sn (enum n n) H_eq)).
  contradiction.
Qed.

I am having hard times to grasp a constructivism here. To my understanding nat -> (nat -> nat) talks only about constructive nat -> nats rather than an (possible undecidable) arbitrary nat -> nat. For each constructive nat -> nat there must be a corresponding Turing machine that computes it for an arbitrary input n, otherwise it is not constructive (thus is undecidable) by the definition. Moreover, there are countably many Turning machines. At this point I conclude: there are countably many constructive nat -> nats, which also means: the nat -> nat Coq's Type (due it's constructive nature) describes countably many functions.
Nonetheless, I am wrong: the proof states: those are actually uncountable...
Where am I mistaken? How does "constructivism" reveals itself in this particular example?

**Tags:** coq, calculus-of-constructions, constructive-mathematics

> **Comments:**
> **username_1**: Your definitions of injective and surjective are switched around.  

---

## 3 answers

### Answer by username_1 on 2023-03-11. Score: 18 | Accepted answer

First, let me say that "constructive" does *not imply* "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the statement

> For every $f : \mathbb{N} \to \mathbb{N}$ there exists a Turing machine $M$ that computes $f$

is known as *formal Church's thesis*. Let us abbreviate it with $\mathrm{CT}$.

> **Theorem:**
>
> 1. Constructive mathematics does **not** prove $\mathrm{CT}$.
> 2. Constructive mathematics does **not** prove $\neg \mathrm{CT}$.

*Proof.* The first statement holds because classical set theory is a model of constructive mathematics in which $\neg\mathrm{CT}$ is valid. The second statement holds because the effective topos is a model of constructive mathematics in which $\mathrm{CT}$ is valid. $\Box$

The upshot of this is that in a constructive argument you *cannot* assume that all functions are computable. If you do that, you are not doing constructive mathematics anymore, but rather something like [Russian recursive mathematics](https://plato.stanford.edu/entries/mathematics-constructive/#RecuConsMath) which assumes additional axioms ($\mathrm{CT}$, countable choice, Markov's principle).

Your question then really is: Why is the usual proof of uncountability of $\mathbb{N} \to \mathbb{N}$ valid in Russian recursive mathematics, given that there are only countably many Turing machines computing functions $\mathbb{N} \to \mathbb{N}$?

The answer is: you are mixing two different kinds of mathematics:

1. In **classical mathematics** there are countably many Turing machines computing functions $\mathbb{N} \to \mathbb{N}$.
2. In Russian constructivism there are **uncountably many** such Turing machines.

How is this possible? First, note that in constructive mathematics it can well happen that a subset of a countable set is uncountable, see the explanation below. Second, let
$$
T = \{n \in \mathbb{N} \mid \text{$n$ encodes a TM computing a map $\mathbb{N} \to \mathbb{N}$}\}
$$
be the set of indices of Turing machines computing maps $\mathbb{N} \to \mathbb{N}$. There is no constructive proof that $T$ is countable. In fact, $T$ is *not* computably enumerable, which in Russian recursive mathematics means precisely that it is not countable.

The moral of the story is: the diagonalization proof of uncountabilty of $\mathbb{N} \to \mathbb{N}$ is constructive, but your understanding of "countable" is not.

P.S. The set of indices of *all* Turing machines is countable, constructively.

P.P.S. The OP asked about the fact that "subsets of countable sets are countable" only holds classically. Here's why.

**Theorem:** *If every subset of $\mathbb{N}$ is countable and Markov's principle holds then excluded middle holds.*

*Proof.* See Proposition 2.6 in [this paper](https://arxiv.org/pdf/1804.00427.pdf). Briefly, given any truth value $p$, let $S = \{n \in \mathbb{N} \mid n = 0 \lor p \}$ and let $e : \mathbb{N} \to S$ be an enumeration of $S$, which exists by assumption. Then $p \Leftrightarrow \exists k \in \mathbb{N} .\, f(k) \neq 0$. By Markov's principle $\exists k \in \mathbb{N} .\, f(k) \neq 0$ is $\neg\neg$-stable, therefore $\neg\neg p \Rightarrow p$. We showed that every truth value is $\neg\neg$-stable, therefore excluded middle holds too. $\Box$

I do not know how to get rid of the assumption of Markov's principle. In any case, the theorem shows that one cannot have a purely constructive proof of "every subset of $\mathbb{N}$ is countable", because Markov's principle is consistent with constructive mathematics.

**Supplemental:** Douglas Bridges pointed out in this [constructivenew post](https://groups.google.com/g/constructivenews/c/xXr8PX8c06Q/m/vevJSKTaCgAJ) that Markov principle cannot be eliminated.

> **Comments:**
> **username_4**: in the Proof, do you mean not CT in the last sentence?  
> **username_0**: > but your understanding of "countable" is not. My understanding that "countable set `A`" means "there exists a bijection between `nat` and `A`". And the proof in the OP states that `nat -> (nat -> nat)` has no bijection. So, it states that `nat -> nat` functions are not countable.   The question is: does it mean that `(nat -> nat) : Set` in Coq speaks about all `nat -> nat` maps including those which can not be computed by a Turing machine?  
> **username_1**: The standard definition of countable in constructive mathematics is: $A$ is countable when there is a surjection $\mathbb{N} \to 1 + A$. When $A$ is inhabited this is equivalent to there being a surjection $\mathbb{N} \to A$. Requiring a bijection is too strong.  
> **username_1**: In any case, whatever notion you're using, the fact remains that you assumed that a certain subset of $\mathbb{N}$ is countable, when in fact this cannot be proved constructively.  
> **username_1**: @DimaPasechnik: thanks for the comment, I fixed the proof (but it was the first occurrence that needed a negation).  
> **username_0**: @AndrejBauer thanks, I will try to find more about the "Have you tried to prove constructively that a subset of a countable set is countable?". If you can, please update your post and add few more words about it and I will accept it.  
> **username_1**: A few more words about what?  
> **username_0**: It is really surprising that subset of naturals numbers can not be proved to be countable constructively.  
> **username_1**: Ok, I wrote a little more. Regarding an improvement of the theorem in the P.P.S., we shall see what comes up [in this Mathstodon thread](https://mathstodon.xyz/@andrejbauer/110005159861304000).  
> **username_4**: @AndrejBauer - oops, apologies - some 40 years ago I managed to pass an exam where a textbook was Maltsev's "Algorithms and recursive functions". I guess it was long evaporated from my brain :-)  
> **username_1**: Douglas Bridges pointed out on constructivenews that Markov principle is necessary. I think this resolves all questions.  

---

### Answer by username_2 on 2023-03-23. Score: 1

To answer very directly: You have a *constructive proof* in Coq but it is not the case that the `enum : nat -> nat` is assumed (in Coq) to be computable. In a sense, it's a constructive proof about a larger domain of things than can actually be constructed in Coq.

Andrej's answer gives a deeper mathematical understanding of why the map should or shouldn't be assumed to be computable. But in Coq, it isn't.


---

### Answer by username_3 on 2023-03-11. Score: -3

What you actually prove is that there is no function that enumerates all the functions that takes a natural number and returns a natural number. The proof is constructive in the sense that in order to prove this fact, you explicitly construct a function f that is not reached. You get a witness.
Definition surj {A B : Type} (f : A -> B) :=
  forall b, exists a, f a = b.

Theorem Cantor_theorem :
  forall (enum : nat -> nat -> nat), ~ surj enum.
Proof.
  intros enum enum_surj.
  pose (f n := S (enum n n)).
  destruct (enum_surj f) as [n f_in_enum].
  assert (enum n n = f n) as H_eq by (rewrite <- f_in_enum ; reflexivity).
  assert (enum n n <> f n) as H_neq by (intros _ ; destruct (n_Sn (enum n n) H_eq)).
  contradiction.
Qed.
```


---

