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

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 \mathbf{R}\rightarrow {\mathbf L}\rightarrow {\mathbf L}(\exists)\] Each of the 34 axioms turns out to be intuitionistically equivalent to one of the above five. The deductions are mechanically checked by \texttt{Coq}, a proof assistant, The authors refer to \({\mathbf L}(\exists)\) as ``Legendre's axiom,'' but the reviewer is not aware of any place in Legendre's \textit{Éléments de géométrie} where such an axiom is stated. Legendre asks that any angle of measure \(\leq 60^{\circ}\) should have the property that, through any point in its interior, there be a line intersecting both legs of the angle. It thus appears that this is the first instance in print where this axiom appears. The authors of the paper [Beitr. Algebra Geom. 60, No. 4, 733--748 (2019; Zbl 1429.51004)] were unaware of this precedent, and were under the impression of having been the first to stumble upon \({\mathbf L}(\exists)\).