Using predicate logic to verify the theorems of Euclid's elements?
I wanted to make a "logical" march through the entirety of Euclid's elements by proving and verifying, step by step, each theorem using Hilbert's axioms as a basis. Of course, I would want to do this all in the symbolic language of predicate logic using a natural deduction format. Has anyone out there done anything like this yet? What would Hilbert's axioms look like when translated into predicate logic? Any tips or pointers would be welcome. Thank you!
$\endgroup$2 Answers
$\begingroup$We (the GeoCoq team) are currently formalizing some propositions of Euclid's Elements using the Coq proof assistant. Our formalization is based on either Tarski's axioms or Hilbert's axiom as we have shown formally that the first three groups of Hilbert's axiom are bi-interpretable with the corresponding Tarski's axioms (excluding continuity) (). You can find a formalization in predicate logic of Hilbert's axioms and a discussion about the formalization and related works in the above paper. It is not completely trivial, because Hilbert's axioms are stated in natural language, and one need to find what is the right interpretation. For example, the concept of a point being inside an angle is not defined by Hilbert. Our formal proofs, shows that our interpretation is enough to reconstruct an ordered field and also prove Tarski's axiom. You can find Hilbert's axioms formalized in Coq here:
Most of the propositions of the first book of Euclid can be found in the GeoCoq library ().
$\endgroup$ $\begingroup$See :
- Sara Negri & Jan von Plato, Proof Analysis : A Contribution to Hilbert’s Last Problem (2011) : Part III. Proof systems for geometric theories, page 131-on.
