To obtain all these results, we have developed a large library in planar neutral geometry, including the formalization of the concept of sum of angles and the proof of the Saccheri–Legendre theorem, which states that assuming Archimedes’ axiom, the sum of the angles in a triangle is at most two right angles.Īvigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s elements. This variant states that, assuming Aristotle’s axiom, any statement which hold in the Euclidean plane and does not hold in the Hyperbolic plane is equivalent to Euclid’s 5th postulate. We also formalize a variant of a theorem due to Szmielew.
![parallel postulate definition geometry parallel postulate definition geometry](https://i.pinimg.com/736x/23/fd/33/23fd33f38d4e19d1437d6b8caefabfda.jpg)
The equivalence between the 34 postulates is formalized in Archimedean planar neutral geometry. For the equivalence between the groups additional assumptions are required. In each group, the proof of their equivalence is mechanized using intuitionistic logic without continuity assumptions. We distinguish four groups of parallel postulates. Following Beeson, we study which versions of the postulate are equivalent, constructively or not. Our formalization provides a clarification of the conditions under which different versions of the postulates are equivalent. Our study is performed in the context of Tarski’s neutral geometry, or equivalently in Hilbert’s geometry defined by the first three groups of axioms, and uses an intuitionistic logic, assuming excluded-middle only for point equality.
![parallel postulate definition geometry parallel postulate definition geometry](http://image.slidesharecdn.com/geosection3-2-111214162850-phpapp02/95/geometry-section-32-1112-5-728.jpg)
In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid’s 5th postulate.