*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Tue, 01 May 2012 11:07:23 +1200*Cc*: Julien Narboux <jnarboux at narboux.fr>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201204292118.q3TLI5TK018411@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com> <201204292118.q3TLI5TK018411@poisson.math.northwestern.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120412 Thunderbird/11.0.1

On 30/04/12 09:18, Bill Richter wrote: > Scott and Fleuriot say something misleading in their intro: > > 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]. > > First, they're citing Heath (a valuable Euclid resource), who mentions > Hilbert quite often but shows absolutely no understanding of how > Hilbert's work fixes Euclid's pervasive angle-addition errors. > > Second, is there even an error, as Scott and Fleuriot quote Heath as > saying? I don't see any plane/solid-geometry error in Hilbert's > axioms listed http://en.wikipedia.org/wiki/Hilbert%27s_axioms I don't think they're saying that there's a problem with the axioms; they're saying that there's a problem with some of Hilbert's proofs. See, for example, Meikle, L. I., and Fleuriot, J. D. Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In Theorem Proving in Higher Order Logics, D. Basin and B. Wolff, Eds., vol. 2758 of Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2003, pp. 319–334. In particular, on page 327, they say "The Grundlagen proof then applied Axiom(II,4). This was not possible in the mechanical proof until all nine assumptions of the axiom were present. ... Hilberts_missing_assumptions was a lemma used to achieve this. Its proof was difficult, especially having to show that EG lay on the plane AFC. Hilbert failed to mention these difficulties." Tim <><

**Attachment:
signature.asc**

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

- Next by Date: 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