Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?

Question

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?

Answer 1

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 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. 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 that Markov principle cannot be eliminated.

Answer 2

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