2. The argument formerly used a direct port of the original
Diaconescu proof as presented in Beeson's "Foundations of
Constructive Mathematics". But in July 2009 I changed it to a
somewhat optimized variant shown to me by Mark Adams. This is
noted in the CHANGES file but not in the comments (I'll fix
that).
John, thanks for clarifying Konrad's remark! Maybe I can add that Michael
Beeson's work is important to my Hilbert axiomatic geometry. The only proof
that Tarski's geometry axioms imply Hilbert's axioms is the book of
Schwabhauser, Szmielew and Tarski, published in German by Ishi Press, primarily
a publisher of Go book, and Michael has convinced me that Schwabhauser's proofs
are correct. That's not an ideal situation, but it's a lot better than nothing,
and Tarski's proof that (Tarski elementary) Geometry is decideable rest on this
publication.
--
Best,
Bill
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
