The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Btw, concerning the status of ~nat=(nat->bool) (mentionned by JF Monin),
> Gilles and I have also the feeling that it's unprovable as such. But
> it might be provable with enough axioms (excluded middle, plus maybe a
> form of axiom of choice). We can at least prove that there isn't any
> surjective function from nat to nat->bool (Cantor argument), but that does
> not gives us the falsity of nat = (nat->bool).

  It does!

Lemma Cantor: ~(EX f : nat -> nat->bool | (g:nat->bool)(EX n:nat | (f n)=g)).
Proof.
Red; NewDestruct 1 as [f H].
Elim H with g:=[n](if (f n n) then false else true).
Intros m H0.
Assert H1: (f m m) = ([n:nat]if (f n n) then false else true m).
  Pattern 1 (f m); Rewrite -> H0; Reflexivity.
Simpl in H1; NewDestruct (f m m); Simpl; Discriminate.
Qed.

Lemma nat_identity: (EX f : nat -> nat | (g:nat)(EX n:nat | (f n)=g)).
Proof.
Exists [n:nat]n; Intro g; Exists g; Reflexivity.
Qed.

Lemma powerset_discr: ~nat==(nat->bool).
Proof.
Intro Heq; Apply Cantor; Rewrite <- Heq; Apply nat_identity.
Qed.

  Hugo