Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
type: Item
instance of: scholarly article
title: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
zbMATH Open document ID: 1441.03011
author: Pierre Boutry
author: Charly Gries
author: Julien Narboux
author: Pascal Schreck
published in: Journal of Automated Reasoning
publication date: 2019-02-15T00:00:00Z
full work available at URL: parallel postulates revised.pdf
review text: This is an important paper, which extends results obtained by \textit{M. Beeson} [Bull. Symb. Log. 22, No. 1, 1--104 (2016; Zbl 1403.03130)], by showing which forms of Euclidean-like parallel postulates are equivalent within intuitionistic logic, with absolute geometry with decidable point equality as the background theory. While inside classical logic we know (see the reviewer and \textit{C. Schacht} [Beitr. Algebra Geom. 60, No. 4, 733--748 (2019; Zbl 1429.51004)]) that, with Hilbert's (or Tarski's) absolute geometry as background, (*) \({\mathbf P}\rightarrow {\mathbf R}\rightarrow {\mathbf L}\rightarrow {\mathbf L}(\exists)\), where \(\mathbf{P}\) stands for the Eucidean parallel postulate, \(\mathbf{R}\) stands for Clairaut's axiom (``There is a rectangle''), \(\mathbf{L}\) stands for Bachmann's \textit{Lotschnittaxiom} (``The perpendiculars raised to the legs of a right triangle intersect''), and \(\mathbf{L}(\exists)\) for ``There exists an angle, such that, through any point in its interior, there is a line intersecting both legs of the angle''. None of the arrows in (*) is reversible. The authors consider many more versions -- 34 altogether -- of axioms resembling the Euclidean parallel postulate, all of which are equivalent with the Euclidean parallel postulate in the presence of the Archimedean axiom, but not in its absence. In the intuitionistic setting, there is an additional axiom in the chain (*), namely between \({\mathbf P}\) and \({\mathbf R}\), where \(\mathbf{P}\) stands for either Euclid's version of the parallel postulate or for Tarski's version thereof (``Through any point in the interior of an angle there is a line intersecting both legs''), there is \({\mathbf H}\), Hilbert's version of the parallel postulate, which states that through a point \(P\) to a line \(g\) not incident with \(P\) there do not pass two parallels to \(g\). The chain (*) thus becomes (each arrow cannot be reversed): \[{\mathbf P}\rightarrow {\mathbf H}\rightarrow \math…
reviewed by: Victor V. Pambuccian
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 51F05
Mathematics Subject Classification ID: 51M05
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7024051
zbMATH Keywords: Euclid
zbMATH Keywords: parallel postulate
zbMATH Keywords: formalization
zbMATH Keywords: neutral geometry
zbMATH Keywords: Coq
zbMATH Keywords: classification
zbMATH Keywords: foundations of geometry
zbMATH Keywords: decidability of intersection
zbMATH Keywords: Aristotle's axiom
zbMATH Keywords: Archimedes' axiom
zbMATH Keywords: Saccheri-Legendre theorem
zbMATH Keywords: sum of angles
zbMATH Keywords: Lotschnittaxiom
zbMATH Keywords: Hilbert
zbMATH Keywords: Tarski
describes a project that uses: Coq
describes a project that uses: GeoCoq
MaRDI profile type: Publication
OpenAlex ID: W2741938952
cites work: A FORMAL SYSTEM FOR EUCLID’SELEMENTS
cites work: Q4755462
cites work: From absolute to affine geometry in terms of point-reections, midpoints, and collinearity
cites work: Zur Parallelenfrage
cites work: Q5667677
cites work: Herbrand's theorem and non-Euclidean geometry
cites work: Formalization of the arithmetization of Euclidean plane geometry and applications
cites work: From Tarski to Hilbert
cites work: A constructive version of Tarski's geometry
cites work: CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE
cites work: Hilbert's ϵ‐operator in intuitionistic type theories
cites work: A set of postulates for plane geometry, based on scale and protractor
cites work: A synthetic proof of Pappus' theorem in Tarski's geometry
cites work: Q3270252
cites work: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
cites work: Q4210022
cites work: Q4531863
cites work: Q4789443
cites work: Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
cites work: Aristotle's axiom in the foundations of geometry
cites work: Q3851216
cites work: Old and New Results in the Foundations of Elementary Plane Euclidean and Non-Euclidean Geometries
cites work: Q4485800
cites work: Q3998128
cites work: Mathematical Expeditions
cites work: Q4391438
cites work: Q3943565
cites work: Formalizing complex plane geometry
cites work: Mechanical Theorem Proving in Tarski’s Geometry
cites work: On the stepwise construction of the parallel postulate
cites work: Q5482811
cites work: On the equivalence of Lagrange's axiom to the Lotschnittaxiom
cites work: Another equivalent of the Lotschnittaxiom
cites work: Strasbourg master class on geometry
cites work: Q4094049
cites work: Die Modelle des Hilbertschen Axiomensystems der absoluten Geometrie
cites work: Q3288579
cites work: Q3678266
cites work: Q3268765
cites work: A new analytic approach to hyperbolic geometry
cites work: Q5807665

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (cites work)
cites work: Tarski's System of Geometry

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (cites work)
cites work: Q4399901

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (DOI)
DOI: 10.1007/S10817-017-9422-8