Thanks, Lorenzo! I'd be grateful if you could teach me some Tarski
geometry, apart from any proof assistant formalization. The last time
I looked, it seemed that Julien Narboux hadn't quite proved the
existence of midpoints, nor Hilbert's full Pasch axiom
let B3 = new_axiom
`! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C
==> (Between A B C \/ Between B C A \/ Between C A B) /\
~(Between A B C /\ Between B C A) /\
~(Between A B C /\ Between C A B) /\
~(Between B C A /\ Between C A B)`;;
I'm embarrassed that I can't prove these things myself, and I'm even
starting to wonder if Tarski actually proved these things. There is
no paper written in English proving Hilbert's axioms from Tarski's.
Your Tarski book, which I don't have, is written in German, by
Schwabhäuser I believe. Can you read it and post some proofs?
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
