*To*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Mon, 30 Apr 2012 23:56:25 -0500*Cc*: jnarboux at narboux.fr, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F9F1B2B.1020209@gmail.com> (tjm1983@gmail.com)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com> <201204292118.q3TLI5TK018411@poisson.math.northwestern.edu> <4F9F1B2B.1020209@gmail.com>

Thanks, Tim! I'll look carefully at your code, and study locales. I should read Scott and Fleuriot's HOL Light article carefully, and also Meikle and Fleuriot's Isabelle paper you cited http://www.springerlink.com/content/6ngakhj9k7qj71th/fulltext.pdf. I'm annoyed Hilbert wrote such an unreadable book FoG, and I wonder he didn't take too much credit from Pasch. So I can learn from Scott, Fleuriot & Meikle. But they need to learn how Euclid's errors were corrected using Hilbert's axioms. I explain this nicely in http://www.math.northwestern.edu/~richter/hilbert.pdf Almost no working mathematicians understand the Euclid and Hilbert's-axiom story, and I only learned it this year, to help my son with Geometry, as his textbook was incredibly unrigorous. He read my paper and my Mizar code quite carefully, and that's why I'm here. What Meikle and Fleuriot write here is misleading: It is generally accepted that Hilbert’s work managed to eradicate the need for INTUITION in deriving results. That's OK if we replace INTUITION by `drawing pictures instead of using axioms'. What is generally accepted is that Hilbert’s work managed to eradicate Euclid's pervasive angle-addition errors. Back to Scott and Fleuriot, you may be correct that they found an error involving solid geometry vs plane geometry. I'll look into it. But Scott and Fleuriot's full quote is very misleading: in their attempt to formalise the axiomatics and its elementary theorems, Meikle and Fleuriot found many missing lemmas [11]. Indeed, IT IS SUFFICIENT to note that Hilbert followed Euclid in one pervasive omission: they both give proofs on an ambient plane when the axioms characterise solid geometry [8]. It is not sufficient. We must note that textbooks by Greenberg & Hartshorne gave acceptably rigorous treatments using Hilbert's axioms, and nobody has ever given rigorous proofs using Euclid's axioms. Tim, you really ought to understand the Euclid and Hilbert-axiom story, being a Tarski geometry guy. Can you find M. Greenberg, Euclidean and non-Euclidean geometries, W. H. Freeman and Co., 1974. R. Hartshorne, Geometry, Euclid and Beyond, Undergraduate Texts in Math., Springer, 2000. Greenberg's recent survey is quite readable and has interesting mathematical logic relating Tarski's axioms to Hilbert's. Old and new results in the foundations of elementary plane Euclidean and non-Euclidean geometries, Amer. Math. Monthly 117 (2010), 198--219. -- Best, Bill

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Jeremy Avigad

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tim (McKenzie) Makarios

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] Multi-dimensional arrays
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list