Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Abstract : In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th postulate. 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. Our formalization provides a clarification of the conditions under which different versions of the postulates are equivalent. Following Beeson, we study which versions of the postulate are equivalent , constructively or not. We distinguish four groups of parallel postulates. In each group, the proof of their equivalence is mechanized using intuitionistic logic without continuity assumptions. For the equivalence between the groups additional assumptions are required. The equivalence between the 34 postulates is formalized in Archimedean planar neutral geometry. We also formalize a theorem due to Szmiliew. This theorem states that, assuming Archimedes' axiom, any statement which hold in the Euclidean plane and does not hold in the Hyperbolic plane is equivalent to Euclid's 5 th postulate. 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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, pp.68. <10.1007/s10817-017-9422-8>
Liste complète des métadonnées

https://hal.inria.fr/hal-01178236
Contributeur : Julien Narboux <>
Soumis le : mercredi 8 mars 2017 - 16:17:51
Dernière modification le : lundi 11 septembre 2017 - 09:23:22
Document(s) archivé(s) le : vendredi 9 juin 2017 - 13:50:03

Fichier

parallel_postulates_revised.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, Springer Verlag, 2017, pp.68. <10.1007/s10817-017-9422-8>. <hal-01178236v2>

Partager

Métriques

Consultations de
la notice

148

Téléchargements du document

180