Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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
Description: OpenPGP digital signature



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