Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

At the end of February, I submitted my Master's thesis, which was about
an Isabelle formalization of the independence of the parallels
postulate.  Specifically, I chose Tarski's axioms, and showed that his
Euclidean axiom (Axiom 10 in Metamathematische Methoden in der
Geometrie) is independent of the others, by proving that the
Klein--Beltrami model of the hyperbolic plane satisfies the rest of
Tarski's axioms, but not the Euclidean axiom.

As you will have gathered, my work was primarily about models of
Tarski's axioms, rather than consequences of them, but if you're
interested, ask me off-list, and I can send you a copy of my thesis, or
my Isabelle files, or whatever interests you.  Please understand,
though, that I haven't heard back from the examiners yet, and I think
they're entitled to ask me to make changes to my thesis, so what I send
you shouldn't be considered to be the final version of my thesis.


On 29/04/12 08:58, Bill Richter wrote:
> Hi, I'm a mathematician writing a rigorous axiomatic geometry paper
> using Hilbert's axioms.  I want to cite geometry proofs nicely coded
> and checked by proof-checker like Isabelle.  I've written Mizar code
> and I want to port it to Isabelle, which Freek Wiedijk seems to
> suggest is an improvement.  Makarius has been helping me, and he said
> I should ask here about formalizations of geometry.  My feeling, which
> could be mistaken, is that Coq and HOL Light are primarily
> theorem-provers (procedural) and require considerable tweaking to
> allow folks to type in readable axiomatic geometry (declarative)
> proofs, but that Isabelle is both procedural and declarative.  
> My Mizar code is a largely a port of Julien Narboux's Coq pseudo-code
>  I partially prove
> the theorem of the 1983 book Metamathematische Methoden in der
> Geometrie by Schwabhäuser, Szmielew, and Tarski, that Tarski's
> (extremely weak!) plane geometry axioms imply Hilbert's axioms.  I get
> about as far as Narboux, with Gupta's amazing proof which implies
> Hilbert's axiom I1 that two points determine a line.  I don't think my
> Mizar code is that great, but it's a lot more readable than Julien's
> Coq pseudo-code.  No doubt some Mizar experts could improve my code,
> but I'm putting them off as a last resort, because Mizar seems
> unsuitable as a language to use in a high school math class.
> So I'd appreciate your Isabelle help, including the easiest way run
> Isabelle programs.  Do I really need Proof General?  I'll also accept
> geometry help!  I haven't seen Schwabhäuser's book, and I can't see
> how to go any farther with Tarski's axioms.  I'm basically missing
> Hilbert's Pasch Betweenness axiom (Tarski's axiom is about 1/3 of it)
> and Hilbert's angle construction axiom.

Attachment: signature.asc
Description: OpenPGP digital signature

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