<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 -> nat`s 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 -> nat`s*, 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**: @username_4: thanks for the comment, I fixed the proof (but it was the first occurrence that needed a negation).  
> **username_0**: @username_1 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/@username_1/110005159861304000).  
> **username_4**: @username_1 - 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.

username_1'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.
```

```


---

