Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
>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.
seems to work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and