Re: [isabelle] rigorous axiomatic geometry proof in Isabelle




Dear all,

At the risk of taking the discussion too far from Isabelle, I'd like to mention that Ed Dean, John Mumma, and I have carried out a detailed analysis of the style of reasoning one finds in Euclid:

  A formal system for Euclid's Elements
  Review of Symbolic Logic, 2:700-768, 2009
  http://journals.cambridge.org/repo_A674ohNM
  (additional links and errata are on my web page)

We argue that Euclid is more rigorous than is commonly acknowledged, in that there are clearly discernible norms to diagrammatic reasoning (though they are different from the norms of axiom-based proof). We also note that Euclidean theorems have a very restricted logical form, and show that his methods are complete (for that class of sentences) with respect to the modern semantics of ruler-and-compass constructions.

Best wishes,

Jeremy

On 05/01/2012 12:56 AM, Bill Richter wrote:
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.






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