The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Adam Chlipala a écrit :
> AUGER Cédric wrote:
> > I may be wrong, but there is also cardinal impossibility for that
> > isomorphism:
> >
> > cnat is a lot bigger than nat and even bigger than reals (true reals, not
> > floating ones), since for each real x, there exists a cnat c such that "c
> > real 0 _ = x", and as there is no bijection between nat and reals, there
> > is no bijection between nat and cnat.
> >   
>
> Isn't every type not provably bigger than [nat] in Coq, since every 
> nameable value of every type (and thus every value that we're sure 
> exists in every model of CIC) corresponds to a finite string of Coq 
> syntax?  I'm not so up on the meta-theoretic issues here, but it seems 
> like constructivity should break the usual cardinality arguments.

You can encode Cantor's diagonal argument to prove that any mapping from 
nat to nat->nat cannot be surjective:

Section Cantor.
Variable f : nat -> (nat -> nat).
Variable f_surj : forall x, exists n, x = f n.

Definition diag n := S (f n n).

Lemma cantor : False.
elim f_surj with diag; intros.
assert (f x x = diag x) by (rewrite H in |- *; trivial).
unfold diag in H0.
apply n_Sn in H0.
trivial.
Qed.

End Cantor.

However, this does not imply that there is no countable model of Coq. It 
just means that in this case, the function that enumerates all the 
values of nat->nat does not belong to the model.
Considering the lambda-term model again, nat->nat denotes an enumerable 
set of lambda-terms, but such an enumeration function cannot be 
represented as a lambda-term.

Bruno Barras.