Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Jens:

>Has anyone seen a constructive version of the
>diagonalization function, i.e. is (e.g. Cantor's)
>diagonalization function computable?

It is certainly possible to prove in Coq (= constructively,
I hope)  that there is no surjection from a set to its
powerset.  I am not a regular Coq user so my proof probably
is twice as long as is necessary, and also it feels rather
strange to post a Coq script to an Isabelle mailing list,
but something like

  Lemma diagonal : forall A : Type,
    ~(exists F : A -> (A -> Prop), forall f, exists x, f = F x).
  unfold not. intros A [F H]. set (f := fun x => not (F x x)).
  elim (H f). clear H. intros x H. assert (H' : f x <-> F x x).
  rewrite H. tauto. unfold f in H'. tauto.
  Qed.

seems to work.

Freek





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.