Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
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
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
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
. 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 .
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),
This archive was generated by a fusion of
Pipermail (Mailman edition) and