Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
Résumé
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.
Dans cet article, nous nous concentrons sur la formalisation des preuves d'équivalence entre différentes versions du 5ème postulat d'Euclide.
Notre étude est réalisée dans le contexte de la géométrie neutre de Tarski, ou de manière équivalente dans la géométrie de Hilbert définie par les trois premiers groupes d'axiomes,
et utilise une logique intuitionniste, en supposant le tiers-exclu uniquement pour l'égalité des points.
Notre formalisation clarifie les conditions dans lesquelles différentes versions des postulats sont équivalentes.
Comme Beeson, nous étudions quelles versions du postulat sont équivalentes, constructivement ou non.
Nous distinguons quatre groupes de postulats des parallèles.
Dans chaque groupe, la preuve de leur équivalence est mécanisée en utilisant la logique intuitionniste sans hypothèses de continuité.
Pour l'équivalence entre les groupes, des hypothèses supplémentaires sont nécessaires. L'équivalence entre les 34 postulats est formalisée dans la géométrie neutre planaire d'Archimède.
Nous formalisons également un théorème dû à Szmiliew. Ce théorème stipule que, en supposant l'axiome d'Archimède, tout énoncé qui est valable dans le plan euclidien et qui ne l'est pas dans le plan hyperbolique est équivalent au 5ème postulat d'Euclide.
Pour obtenir tous ces résultats, nous avons développé une large bibliothèque en géométrie plane neutre, incluant la formalisation du concept de somme d'angles et la preuve du théorème de Saccheri-Legendre, qui stipule que, en supposant l'axiome d'Archimède, la somme des angles dans un triangle est au plus égale à deux angles droits.
Origine : Fichiers produits par l'(les) auteur(s)