Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



   they have built a large Coq library about high school geometry.
   [...] But this [ Coq declarative proof] language is not used much
   by the Coq community so you may encounter bugs.

Julien, I think that you and your coauthors in
http://hal.inria.fr/docs/00/58/49/18/PDF/iccsaConf.pdf are using Coq
to figure out how to teach the course, and not asking the students to
write Coq code proofs.  This sentence in your paper concerns me:

   The work closest to ours is the one by
   P. Scott and J. Fleuriot [17].
http://www.springerlink.com/content/b715100716u1t347/?MUD=MP

I know I just got here, and I'm not trying to fight with anyone, but I
think this paper shows I have some value to the group already.  

Scott and Fleuriot took on a challenging and interesting HOL Light
project, to fill in the gaps of Hilbert's book FoG.  That will show
the power of HOL Light and their programming skill.

But their paper doesn't seem helpful in teaching a rigorous Hilbert
geometry course.  Reading Greenberg's & Hartshorne's books (or my
paper http://www.math.northwestern.edu/~richter/hilbert.pdf) would
much more helpful.  The authors don't seem to understand the gaps in
Euclid's work which were fixed by Hilbert's axioms.  Euclid messed up
every single result that involved angle addition, including the
triangle sum theorem (sum 3 angles = 180).  That's a result kids
taking a Hilbert geometry course need to know!  The authors study
instead possible deficiencies of Hilbert's book FoG, and there may be
plenty, but you can't teach a geometry course out of FoG, as there
isn't enough interesting material.  Euclid's errors are much more
interesting, as Euclid was often used as a textbook (for centuries?).
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

In my paper I explain (following Moise's rigorous book) how to handle
this solid geometry biz.  Basically, for all the 2-dim stuff you have
to say "in a plane" and in the 3-dim part you then use the planar
stuff plus extra incidence axioms.  Euclid's book XI is a fantastic
treatment of solid geometry, which Moise simplifies.

-- 
Best,
Bill 





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