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 5th 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 variant of a theorem due to Szmielew. 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. 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.

1 Introduction

In this paper we focus on the formalization of results about Euclid’s 5th postulate:

If two lines are drawn which intersect a third in such a way that the sum of the inner angles on one side is less than two right angles, then the two lines inevitably must intersect each other on that side if extended far enough.

This postulate is of historical importance because for centuries, many mathematicians believed that this statement was rather a theorem which could be derived from the first four Euclid’s postulates. History is rich with incorrect proofs of Euclid’s 5th postulate. In 1763, Klügel provided, in his dissertation written under the guidance of Kästner, a survey of about 30 attempts to “prove” Euclid’s parallel postulate” [39]. Legendre published a geometry textbook Eléments de géométrie in 1774. Each edition of this popular book contained an (incorrect) proof of Euclid’s postulate. Even in 1833, one year after the publication by Bolyai of an appendix about non-euclidean geometry, Legendre was still convinced of the validity of his proofs of Euclid’s 5th postulate:

Il n’en est pas moins certain que le théoréme sur la somme des trois angles du triangle doit être regardé comme l’une de ces vérités fondamentales qu’il est impossible de contester, et qui sont un exemple toujours subsistant de la certitude mathématique qu’on recherche sans cesse et qu’on n’obtient que bien difficilement dans les autres branches des connaissances humaines.¹

                                                                                                – Adrien Marie Legendre [40]

These proofs are incorrect for different reasons. Some proofs rely on an assumption which is more or less explicit but that the author takes for granted. Some other proofs are incorrect because they rely on a circular argument.

Proving the equivalence of different versions of the parallel postulate requires extreme rigor, as Richard J. Trudeau has written:

Pursuing the project faithfully will require that we take the extreme measure of shutting out the entreaties of our intuitions and imaginations - a forced separation of mental powers that will quite understandably be confusing and difficult to maintain [...].

                                                                                                – Richard J. Trudeau [62]

To help us in this task, we have a perfect tool which possesses no intuition: a computer. In this paper we provide formal proofs, verified using the Coq proof assistant, that 34 different versions of Euclid’s 5th postulate are equivalent in the theory defined by a subset of the axioms of Tarski’s geometry, namely the 2-dimensional neutral geometry² using Archimedes’ axiom. We also provide more precise results showing the equivalence in intuitionistic logic of four groups of axioms without any continuity assumption.

Our formal proofs rely on the systematic development of geometry based on Tarski’s system of geometry [57] that Schwabhäuser, Szmielew and Tarski produced. Those results have been formalized previously [8, 16, 17, 47] using the Coq proof assistant, and completed by some new results in neutral geometry for this study. The equivalence between 26 versions of Euclid’s 5th postulate can be found in [44]. Greenberg also proves (or leaves as exercises) the equivalence between several versions of the parallel postulate [33]. However, these proofs are not checked mechanically and sometimes only sketched. Moreover, since we restrict ourselves to intuitionistic logic and we use continuity axioms only when necessary, we could not reuse directly all these proofs in our context, because some proofs in these books use the law of excluded middle or a continuity axiom (see Sect. 3).

Following the classical approach to prove that Euclid’s 5th postulate is not a theorem of neutral geometry, Timothy Makarios has provided a formal proof of the independence of Tarski’s Euclidean axiom [43]. He used the Isabelle proof assistant to construct the Klein–Beltrami model, where the postulate is not verified. A close result is due to Filip Marić and Danijela Petrović who formalized the complex plane using the Isabelle/HOL proof assistant [46]. Recently, Michael Beeson has also studied the equivalence of different versions of the parallel postulate in the context of a constructive geometry [11].

The paper is structured as follows. In Sect. 2, we describe the axiom system that we use and its formalization in Coq. In Sect. 3, we give an overview of the results that we formalized, based on four example postulates, each representing a group of postulate which are equivalent. Then, in the following Sects. 4, 5, 6 and 7 (one for each group of postulates), we give the precise statements and an overview of the proofs. The list of all the studied postulates is given in “Appendix A”, and the summary of the main definitions and notations is given in “Appendix B”.

2 The Context

In this section, we will first present the axiomatic system that we used as a basis for our proofs.

It is crucial to be precise about the context and the definitions. This paper is about equivalence properties, but an equivalence is relative to a theory and a logic. We prove the equivalences within the higher order intuitionistic logic of Coq and using Tarski’s axiom system for neutral geometry. Using the language of logic, the assertion saying that P and Q are equivalent formally means³ that: $T \models P \Leftrightarrow Q$ holds for a given theory T. It could be the case that $T \models P \Leftrightarrow Q$ holds because both $T \models P$ and $T \models Q$ hold. For every version P of the parallel postulates presented in this paper it is also true that $T \not \models P$, but we do not prove the independence results. Defining accurately the theory T is of primary interest because the equivalence results depend on the precise definition of T. For example, Millman and Parker [45, p. 226] have shown that the Pythagorean theorem is equivalent to the parallel postulate in the context of an axiom system in the style of Birkhoff axioms based on a ruler and protractor [14]. Yet there is a Cartesian plane over a (non-archimedean) Pythagorean field⁴ which does not verify the parallel postulate: see Example 18.4.3 [36, p. 161]).

2.1 A Set of Axioms for Neutral Geometry

Proofs are given within Tarski’s system of neutral geometry. We adopted the axioms given in [57] excluding the axiom corresponding to Euclid’s 5th postulate. For an explanation of the axioms and their history see [61]. Table 1 lists the axioms for neutral geometry. The consistency of this axiom system has been mechanically proven by Makarios [43]. As we already mentioned, Makarios has also proven formally the independence of the parallel postulate in this axiom system using the Klein–Beltrami model [21]. One should notice that he could have employed the Poincaré disk model, which also satisfies the axioms of Table 1. These two properties make Tarski’s system of geometry suitable for proofs of equivalence of statements of Euclid’s parallel postulate.

Let us recall that Tarski’s axiom system is based on a single primitive type depicting points and two predicates, namely congruence and betweenness. ${AB} \mathbin {\equiv } {CD}$ states that the segments $\overline{AB}$ and $\overline{CD}$ have the same length. means that A, B and C are collinear and B is between A and C (and B may be equal to A or C).

Table 1 Tarski’s axiom system for neutral geometry

The symmetry axiom (A1 on Table 1) for equidistance together with the transitivity axiom A2 for equidistance imply that the equidistance relation is an equivalence relation between pair of points.

The identity axiom for equidistance A3 ensures that only degenerated segments can be congruent to a degenerated segment.

Fig. 1

Axiom of segment construction A4

The axiom of segment construction A4 allows to extend a segment by a given length (Fig. 1⁵).

Fig. 2

Five-segment axiom A5

The five-segment axiom A5 corresponds to the well-known Side-Angle-Side postulate but is expressed with the betweenness and congruence relations only. The lengths of $\overline{AB}$, $\overline{AD}$ and $\overline{BD}$ and the fact that fix the angle $\angle CBD$ (Fig. 2).

The identity axiom for betweenness A6 expresses that the only possibility to have B between A and A is to have A and B equal. It also insinuates that the relation of betweenness is non-strict, unlike Hilbert’s one. As Beeson suggests in [10], this choice was probably made to have a reduced number of axioms by allowing degenerated cases of the Pasch’s axiom.

The inner form of Pasch’s axiom A7 is the axiom Pasch introduced in [53] to repair the defects of Euclid. It intuitively says that if a line meets one side of a triangle, then it must meet one of the other sides of the triangle. There are three forms of this axiom. Thanks to Gupta’s thesis [35], one knows that the inner form and the outer form of this axiom are equivalent and that both of them allow us to prove the weak form. The inner form enunciates Pasch’s axiom without any case distinction. Indeed, it indicates that the line BP must meet the triangle ACQ on the side $\overline{AQ}$, as Q is between B and C (Fig. 3).

The lower 2-dimensional axiom A8 asserts that the existence of three non-collinear points.

Fig. 3

Pasch’s axiom A7

Fig. 4

Upper dimensional axiom A9

The upper 2-dimensional axiom A9 means that all the points are coplanar. Since A, B and C are equidistant to P and Q, which are different, they belong to the hyperplane consisting of all the points equidistant to P and Q. Because the upper 2-dimensional axiom specifies that A, B and C are collinear, this hyperplane is of dimension one and it fixes the dimension of the space to two. It forbids the existence of the point $C'$ (Fig. 4).

2.1.1 Formalization in Coq

Contrary to the formalization of Hilbert’s axiom system [9, 16, 25], which leaves room for interpretation of natural language, the formalization in Coq of Tarski’s axiom system is straightforward, as the axioms are stated very precisely. We defined the axiom system using three type classes (Table 2). The first class regroups the axioms for neutral geometry in any dimension greater than or equal to two (A1–A8).

With the second class, we also assume that we can reason by cases on the point equality (point_equality_decidability). This axiom does not appear in [57], although reasoning by cases on point equality is done as soon as the second chapter (the first chapter being dedicated to the axioms), because it is a tautology in classical logic, while the logic of Coq is intuitionistic. We say that a predicate is decidable when it verifies the excluded middle property. We have shown previously [18], by modifying and reordering the proofs of [57] that we had formalized that decidability of point equality implies decidability of the main predicates defined in [57] besides the intersection of two lines.

Finally, the third class corresponds to the axioms of planar neutral geometry (A1–A9) with excluded middle for point equality.

We have proven formally that Hilbert’s axioms Group I, II and III are bi-interpretable with Tarski’s axiom A1–A9 [9, 16]. Hence, the result presented in this paper are also valid in this axiom system, the models of which are called Hilbert-planes by Hartshorne [36].

Table 2 Formalization of the axiom system in Coq

3 Four Categories of Parallel Postulates

In this paper, we classify different statements of the parallel postulate into four categories. Throughout this section, we will focus on one postulate for each of these four categories. These four main postulates are equivalent in Archimedean neutral geometry using classical logic. However, in an intuitionistic logic, and in a non-Archimedean context, they are not equivalent.

3.1 Independent Parallel Postulates

Let us consider four versions of the parallel postulate.

• 1. The first postulate that we present was chosen by Tarski [60] and retained in [57]. Therefore, we will refer to it as Tarski’s parallel postulate. It expresses that given a point D between the points B and C and a point T further away from A than D on the half line AD, one can build a line which goes through T and intersects the sides BA and BC of the angle $\angle ABC$ respectively further away from B than A and C (Fig. 13).

• 2. The second postulate that we will study in this paper was adopted by Hilbert in [37] and is known as Playfair’s postulate. It states that there is a unique parallel to a given line going through some point (Fig. 14).

• 3. The third postulate, which we will designate as the triangle postulate, corresponds to the implicit assumption made by Legendre in the quote by him from the introduction. It asserts that the sum of the interior angles of a triangle is equal to two right angles (Fig. 15).

• 4. Finally, the fourth postulate is due to Bachmann [5]. Following Pambuccian [50], we will refer to it as Bachmann’s Lotschnittaxiom. It formulates that given the lines l, m, r and s, if l and r are perpendicular, r and s are perpendicular and s and m are perpendicular, then l and m must meet.

In classical logic, these four postulates are equivalent in Archimedean neutral geometry. By Archimedean planar neutral geometry we mean neutral geometry in which Archimedes’ axiom⁶ holds. Archimedes’ axiom is a corollary of the continuity axiom of Tarski (A11, which we do not present here) which can be expressed in the following way. Given two segments $\overline{AB}$ and $\overline{CD}$ such that A is different from B, there exist some positive integer n and $n+1$ points $A_1, \ldots , A_{n+1}$ on line CD, such that $A_j$ is between $A_{j-1}$ and $A_{j+1}$ for $2< j < n$, $A_j A_{j+1}$ and AB are congruent for $1< j < n$, $A_1 = C$ and D is between $A_n$ and $A_{n+1}$.

Nevertheless, by weakening the theory, this equivalence ceases to hold. We presented these postulates, which fall into four distinct categories, in decreasing order of strength.

3.1.1 Tarski’s Parallel Postulate is Strictly Stronger than Playfair’s Postulate

By dropping the law of excluded middle,⁷ Tarski’s parallel postulate becomes strictly stronger than Playfair’s postulate. Indeed, a particular instance of the law of excluded middle, namely the decidability of intersection of lines, is required to prove that Tarski’s parallel postulate follows from Playfair’s postulate. We will present this proof in Sect. 5 since we did not prove a direct implication, and therefore first need to introduce some other postulates. Now, to prove that the decidability of intersection of lines is indeed needed for the proof, it suffices to show that Tarski’s parallel postulate implies the decidability of intersection of lines and that Playfair’s postulate does not. We will prove the first of these facts in Sect. 5. The second of these facts can be proven in the same fashion as the independence of the parallel postulate from the other axioms of Tarski’s system of geometry was proved in [7]. This proof consists in remarking that Tarski’s parallel postulate allows us to construct arbitrary far away points while the other axioms do not. This remark together with Herbrand’s theorem give an independence proof. Here the same remark can be made about the decidability of the intersection of lines and the other axioms of Tarski’s system of geometry plus Playfair’s postulate.

However, Playfair’s postulate can be proved in neutral geometry with decidable point equality assuming Tarski’s parallel postulate. This proof is actually in [57]: it corresponds to Satz 12.11 which we formalized. In this proof, one does not need to reason by cases on the possibility for two lines to intersect.

3.1.2 Playfair’s Postulate is Strictly Stronger than the Triangle Postulate

Just as Tarski’s parallel postulate becomes strictly stronger than Playfair’s postulate by dropping the law of excluded middle, Playfair’s postulate becomes strictly stronger than the triangle postulate when dropping Archimedes’ axiom. Indeed, Max Dehn, a student of Hilbert, has shown that Playfair’s postulate is independent from the axioms of planar neutral geometry extended with the triangle postulate [26]: he gave a non-Archimedean model in which the triangle postulate holds and Playfair’s postulate does not. One could then think that Archimedes’ axiom is the missing link between these postulates. Actually, Greenberg has showed that, in order to prove that the triangle postulate implies Playfair’s postulate, a corollary of Archimedes’ axiom is sufficient [34], which we will refer to as Greenberg’s axiom⁸ (Fig. 18). In fact, Greenberg proves that this axiom is a corollary of Archimedes’ axiom by proving that it follows from Aristotle’s axiom⁹ (Fig. 17), itself following from Archimedes’ axiom. Greenberg defines Aristotle’s and Greenberg’s axioms in the following way.

Given any acute angle, any side of that angle, and any challenge segment PQ, there exists a point Y on the given side of the angle such that if X is the foot of the perpendicular from Y to the other side of the angle, then $YX > PQ$.

Given any segment PQ, line l through Q perpendicular to PQ, and ray r of l with vertex Q, if $\theta$ is any acute angle, then there exists a point R on r such that ${P} \, {R} \, {Q} {{\mathrm{\mathbin {\widehat{<}}}}}\theta$.¹⁰

3.1.3 The Triangle Postulate is Strictly Stronger than Bachmann’s Lotschnittaxiom

Similarly, when dropping Archimedes’ axiom, the triangle postulate becomes strictly stronger than Bachmann’s Lotschnittaxiom. Bachmann demonstrated that this postulate, that he named Lotschnittaxiom, was strictly weaker than the triangle postulate [6]. Pambuccian proved that Aristotle’s axiom is sufficient to prove that the triangle postulate is implied by Bachmann’s Lotschnittaxiom [48]. Pambuccian’s proof uses Pejas’ classification of Hilbert planes [54] and, up to our knowledge, there is no synthetic proof of the fact that this corollary is sufficient, therefore we did not formalize this proof.

We can summarize the results from the previous subsections using Fig. 5.

Fig. 5

Graphical summary of the independence results from Sects. 3.1.1–3.1.3

These independence results confirm that the theory in which the statements are proven needs to be precisely defined. Moreover, they illustrate the fact that some postulates can cease to be equivalent if the logic is changed. Therefore, the notion of equivalence is not only relative to the theory but also to the logic. Since, in this paper, we classify parallel postulates according to the theory and the logic in which they are equivalent, we will now introduce a few notations for the different kinds of equivalence that will be considered. Let us denote by N the axioms of planar neutral geometry (A1–A9) with decidability of point equality, by A Archimedes’ axiom and by G Greenberg’s axiom. We adopt the symbols $\models _{LJ}$ and $\models _{LK}$ to differentiate the intuitionistic and the classical setting. We say that two properties P and Q are respectively $\mathcal {N}_{LJ}$-equivalent, $\mathcal {N}_{LJ}^{\mathcal {G}}$-equivalent, $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalent or $\mathcal {N}_{LK}$-equivalent if $N \models _{LJ} P \Leftrightarrow Q$, $\,N; G \models _{LJ} P \Leftrightarrow Q$, $\,N; A \models _{LJ} P \Leftrightarrow Q$ or $N \models _{LK} P \Leftrightarrow Q$. The rest of this paper will be organized according to Fig. 5. In order to determine in which category a version of the parallel postulate belongs we will formalize its $\mathcal {N}_{LJ}$-equivalence with one of this four postulates. For the sake of avoiding references to the $\mathcal {N}_{LJ}$-equivalence of some postulates, we will start by studying the postulates $\mathcal {N}_{LJ}$-equivalent to Playfair’s postulate. Then we will proceed in decreasing order of strength, thus considering the postulates $\mathcal {N}_{LJ}$-equivalent to Tarski’s parallel postulate, then those $\mathcal {N}_{LJ}$-equivalent to the triangle postulate and finally those $\mathcal {N}_{LJ}$-equivalent to Bachmann’s Lotschnittaxiom.

3.2 Formal Definitions of Acute Angles, Parallelism and the Sum of Non-oriented Angles

In order to formalize these four postulates and these four axioms, we first need to define acute angles, parallelism and the sum of non-oriented angles. Indeed, Tarski’s parallel postulate is the only postulate expressed without any definition.¹¹ Thus this subsection will be dedicated to defining these concepts. In this paper, the exact Coq syntax of the axioms, definitions and main theorems is listed without any pretty printing, to give the reader the opportunity to check what is the exact statement we proved. For the auxiliary lemmas and all the proofs, we will use classical mathematical notations. The proofs given in this paper serve only as a documentation; the correctness of the results is assured by the mechanical proof checker. Recall that for each postulate, we will provide the figure representing the statement in the Euclidean plane and a counter-example in Poincaré disk model. Having a counter-example in non-Euclidean geometry is interesting, as Szmielew proved (assuming Dedekind’s axiom for first-order formulas) that every statement which is false in hyperbolic geometry and correct in Euclidean geometry is equivalent to the fifth parallel postulate [58] (we formalize a variant of this theorem in Sect. 7.4).

Fig. 6

Definition of Coplanar

3.2.1 Formal Definition of Parallelism

In this subsection we define parallelism, which will be one of the most important definitions for this work. In [57] one can find two definitions of parallelism. The common way of defining it is to consider two lines as parallel if they belong to the same plane but do not meet. This implies that we will also define collinearity and coplanarity. The other definition of parallelism includes the previous one and add the possibility for the lines to be equal. Therefore we will talk about strict parallelism in the first case and about parallelism in the second.

This predicate corresponds to Definition 4.10 of [57]. Among the first definitions which are introduced, there is the predicates expressing collinearity. It can be defined using only the betweenness predicate. ${{\mathrm{Col}}}\, {A} \, {B} \, {C}$ expresses that A, B and C are collinear if and only if one of the three points is between the other two.

We did not define coplanarity in the same way as in [57]; we chose to express coplanarity as a 4-ary predicate to avoid the definition of a predicate with an arbitrary number of terms. Restricting ourselves to characterize coplanarity of four points, we could use Satz 9.33 in [57] as a definition of coplanarity. This definition states that 4 points are coplanar if two out of these four points form a line which intersect the line formed by the remaining two points (either $X_1$, $X_2$ or $X_3$ on Fig. 6). Since we are in a 2-dimensional space in this paper, 4 points are always coplanar. Yet we keep this definition, because we plan to extend our formalization to higher dimensions in the future, as a large part of our library is available in arbitrary dimension. In fact, in [57] the proofs are performed in a n-dimensional space for a fixed positive integer n, given by the statement of variants of the dimensional axioms.

This predicate corresponds to Definition 12.2 of [57]. Note that one could have chosen other definitions. For instance, one could have defined two lines (when we consider lines, it is implied that the two points defining them are distinct) to be parallel when they are at constant distance. According to Papadopoulos [52], this definition was introduced by Posidonius, an early commenter of Euclid’s Elements. As we will see in Sect. 6, an implicit change in a definition can have severe consequences in the validity of a proof.

This predicate corresponds to Definition 12.3 of [57]. This definition asserts that two lines are parallel if they are strictly parallel or if they are equal, since with the previous definition, one line is not parallel to itself.

3.2.2 Formal Definition of the Sum of Non-oriented Angles

This subsection will be devoted to the definition of the sum of non-oriented angles. It is based on the notions of congruence of angles and sides of line, which will be presented in this subsection. It should be pointed out that there is no definition for the sum of non-oriented angles in [57].

Fig. 7

Definition of CongA

This predicate corresponds to Definition 11.2 of [57]. Two angles are said to be congruent if one can prolong the sides of the angles to obtain congruent triangles (Fig. 7). ${A} \, {B} \, {C} {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$ means that angles $\angle ABC$ and $\angle DEF$ are congruent. It should be noticed that even though the definition does not explicitly states that ${BA'} \mathbin {\equiv } {EF'}$ or ${BC'} \mathbin {\equiv } {ED'}$, these congruences are provable thanks to Satz 2.11 of [57]. This proposition corresponds to a degenerate case of the five-segment axiom A5 (Fig. 2). This is technically important in Tarski’s system of geometry, as it allows us to have fewer axioms in the system. However, the non-degenerate case of this axiom is independent of the other axioms of our theory to which one would add the degenerate case of this axiom [37]. It is therefore questionable to assume such axioms when using intuitionistic logic. Nevertheless, as proved in [10, 18], assuming the decidability of point equality suffices to recover all the propositions of [57] in an intuitionistic setting.

Fig. 8

Definition of TS

Fig. 9

Definition of OS

This predicate corresponds to Definition 9.1 of [57]. The name of this predicate corresponds the abbreviation for two sides. It describes a special case of the coplanarity (Fig. 6), namely when the intersection point is between the two points defining one of the lines (Fig. 8). In this case one says that these first two points are on opposite sides of the other line. indicates that P and Q are on opposite sides of line AB. This definition being a special case of coplanarity, it has the advantage of being valid in spaces of dimension higher than two. This notion is absent in Euclid’s Elements [28], in which the relative position of the points on the figure is not justified, but inferred from the figure.

The last predicate needed to be able to define the sum of non-oriented angles captures the property for two points to be on the same side of a line. This predicate corresponds to Definition 9.7 of [57]. The name of this predicate corresponds the abbreviation for one side. Two points are said to be on the same side of a line if there exists a third point with which both of the points are on opposite side of this line (Fig. 9). indicates that P and Q are on the same side of line AB.

Fig. 10

Definition of SumA

As we want to study the impact of Archimedes’ axiom, we cannot define the sum of angles through the use of a measure for the angles. Indeed, Archimedes’ axiom would be needed to define a measure function [56]. Another approach could be to define a function that given two angles would return an angle representing their sum. Again this approach would necessitate an extra axiom: the axiom of choice. As a matter of fact, the axiom of choice would be used to select a representative within the equivalence class of the angles congruent to the sum of our given angles. Thus the sum of angles has to be defined geometrically.

To obtain the sum of two angles $\angle ABC$ and $\angle DEF$, one constructs a point J such that $\angle ABC$ and $\angle CBJ$ are adjacent and ${C} \, {B} \, {J} {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$ (Fig. 10). Then the sum of the angles $\angle ABC$ and $\angle DEF$ is $\angle GHI$ if ${A} \, {B} \, {J} {{\mathrm{\mathbin {\widehat{=}}}}}{G} \, {H} \, {I}$. One thing which could be surprising is the fact that we specified that the angles $\angle ABC$ and $\angle CBJ$ are adjacent by the fact that A and J are not on the same side of line BC. This choice allows us to do without a disjunction of cases (either A and J are on opposite side of line BC or J belongs to line BC). Actually one cannot simply state that these points are on opposite sides of line BC, as this would imply that the sum of angles is not defined when one of the angles is straight or null.

The triangle postulate expresses a property about the sum of the interior angles of a triangle, so we decided to define a predicate stating that the sum of the interior angles of a triangle is congruent to a specific angle. Namely, ${{\mathrm{\mathcal {S}}}}(\bigtriangleup {A}{B}{C}) {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$ means that the sum of the interior angles of triangle ABC is congruent to angle $\angle DEF$. The fact that we did not define the sum of angles as a function but as a predicate motivated this choice. Indeed, it avoids carrying the witness of the partial sum of the first two angles. Of course, to be able to talk about the sum of the angles of a triangle, it has to be commutative and associative. We will later see that it is only the case under certain conditions that are fulfilled when considering the interior angles of a triangle.

3.2.3 Formal Definition of Acute Angles

In order to be able to formalize a predicate specifying that an angle is acute, we need to define the concepts of angle comparison and right triangles. Defining these concepts was straightforward, as both of them were already present in [57]. For the sake of completeness we will now present them.

To express a predicate specifying that an angle is acute, we do not need a definition for perpendicularity, but only for right triangles. The definition of a right triangle is more general than the definition of a right angle since it includes the case of a degenerate triangle. In [57], right triangles are defined through midpoints. Following, we first present Tarski’s definition of midpoint and right triangle.

This predicate corresponds to Definition 7.1 of [57]. It states that M is the midpoint of A and B. It is the case when M is between A and B and equidistant from them. It is interesting to notice that the existence of the midpoint appears quite late in [57]. This is because its proof, which does not involve the continuity axiom and is due to Gupta [35], cannot be done earlier in the development.

Fig. 11

Definition of Per

This predicate corresponds to Definition 8.1 of [57]. In the case where B is different from A and C, (Fig. 11) means that A, B and C form a right triangle with the right angle at vertex B. But is also true when B is equal to A and/or C. Therefore, we will need either to specify that these points are different or a new definition to avoid this case.

The notion of angle comparison is defined by means of a predicate stating that a point belongs to the interior of an angle, itself formulated using a predicate asserting that a point belongs to a ray.

This predicate corresponds to Definition 6.1 of [57]. indicates that P belongs to line AB but does not belong to the segment $\overline{AB}$. This implies that A and B belong to the same ray with initial point P and that neither of these points coincide with P. This predicate is symmetric in its last two points, but we usually choose to prioritize the first of these points to define the ray. Thus, most of the time, will express the fact that B belongs to the ray PA.

Fig. 12

Definition of InAngle

This predicate corresponds to Definition 11.23 of [57]. ${P} {{\mathrm{\mathbin {\widehat{\in }}}}}{A} \, {B} \, {C}$ states that P belongs to the interior of angle $\angle ABC$ (Fig. 12). A point P is said to belong to the angle ABC if this angle is well defined, meaning that B is distinct from both A and C, and if there exists a point X on the segment $\overline{AC}$ such that either P belongs to the ray BX or B and X are equal. This last case occurs when angle $\angle ABC$ is straight and one consider that any point belongs to a straight angle, except its vertex. An alternative to this definition would have been the one Greenberg uses in [33], namely that P belongs to the interior of the angle ABC if P and A are one the same side of line BC and if P and C are on the same side of line BA. The definition from [57] is more general, because according to Greenberg’s definition, a point on one of the sides of an angle is not inside it. Assuming that the point we consider is not on a side of the angle, the one we adopted trivially implies the one Greenberg uses, and the converse can be proved by applying Pasch’s axiom. However, we chose to adopt the version from [57] since it directly provides the point X. Let us here emphasize again the importance of definitions. The reader could be tempted to define ${P} {{\mathrm{\mathbin {\widehat{\in }}}}}{A} \, {B} \, {C}$ as the existence of a segment with endpoints on the sides of a given angle which passes through P. Yet, it is not always the case that this segment exists. Indeed, this property corresponds to Tarski’s parallel postulate.

This predicate corresponds to Definition 11.27 of [57]. An angle $\angle ABC$ is said to be smaller than or equal to another angle $\angle DEF$ if there exists a point P in the interior of this second angle such that angle $\angle DEP$ is congruent to the first angle. The witness point P, which is needed for proving different properties about this order relation, is omitted by this predicate.

This predicate corresponds to Definition 11.38 of [57]. It is more straightforward to first define the non-strict comparison between angles. However, in order to obtain a predicate characterizing acute angles, we need to define the strict comparison between angles. This is done by simply excluding the case where the angles are congruent.

Finally, we can define a predicate characterizing acute angles. This predicate corresponds to Definition 11.39 of [57]. An angle $\angle ABC$ is said to be acute if there exists a right triangle $A'B'C'$ with the right angle at vertex $B'$ such that angle $\angle ABC$ is strictly smaller than angle $\angle A'B'C'$. One can recall that means that angle $\angle A'B'C'$ is right only in the case where $B'$ is distinct from both $A'$ and $C'$. This is the case thanks to the definition of the angle comparison. This enforces that the angle to which we compare the angle ABC is indeed right.

3.3 Formalization of the Four Particular Versions of the Parallel Postulate and of the Continuity Axioms

In this subsection, we formalize Tarski’s parallel postulate, Playfair’s postulate, the triangle postulate and Bachmann’s Lotschnittaxiom, as well as the decidability of intersection of lines, Archimedes’, Aristotle’s and Greenberg’s axioms. Now that we defined acute angles, parallelism and the sum of non-oriented angles, we will be able to define these postulates and axioms easily, except for Archimedes’ axiom, which requires a few extra definitions.

3.3.1 Tarski’s Parallel Postulate

Fig. 13

Tarski’s parallel postulate (Postulate 1)

This postulate (Fig. 13) is the official version of the parallel postulate found in [57]. The statement, due to Lorentz [35], is a modification of an implicit assumption made by Legendre while attempting to prove that Euclid’s parallel postulate was a consequence of Euclid’s other axioms, namely Legendre’s parallel postulate which will be introduced in Sect. 7.3. This version is particularly interesting, as it has the advantages of being easily expressed only in term of betweenness, and being valid in spaces of dimension higher than two.

3.3.2 Playfair’s Postulate

Fig. 14

Playfair’s postulate (Postulate 2)

Playfair’s postulate (Fig. 14) is one of the best-known versions of the parallel postulate for the modern reader. This postulate corresponds to Satz 12.13 in [57]. Note that it does not state the existence of the parallel line but only its uniqueness, because the existence can be proved from the axioms of Tarski’s neutral geometry (Satz 12.10 of [57]). Proclus, another early commenter of Euclid’s Elements, already recognized that an incorrect proof of Euclid’s postulate by Ptolemy was making this implicit assumption.

3.3.3 Triangle Postulate

Fig. 15

Triangle postulate (Postulate 3)

The triangle postulate (Fig. 15) corresponds to Proposition I.32 in [28] and Satz 12.23 in [57]. We formalized it slightly differently, as it precisely formulates that the sum is equal to a straight angle instead of two right angles. Nevertheless, we have proved that the sum of an angle with itself is equal to a straight angle if and only if the angle is right. This postulate results of a failed attempt at proving Euclid’s parallel postulate due to Legendre. This statement was implicitly used in one of Legendre’s proofs. Interestingly, the sum of the angles of a triangle allows to set apart hyperbolic, Euclidean and elliptic geometry. This sum is respectively lower, equal or higher than two right angles in hyperbolic, Euclidean and elliptic case.

3.3.4 Bachmann’s Lotschnittaxiom

This postulate (Fig. 16) expresses that, given that the lines PQ and QR are perpendicular, the lines PQ and $P P_1$ are perpendicular and the lines QR and $R R_1$ are perpendicular, we know that the lines $P P_1$ and $R R_1$ must intersect. Here, the perpendicularity hypotheses are expressed using the Per predicates, hence we had to add non-degeneracy hypotheses to exclude the cases where the points P and Q, as well as the points Q and R, are equal. However, since the property is trivially true in the cases where $P = P_1$ or $R = R_1$, we did not exclude these cases. According to Hartshorne [36], it “characterizes geometries in which the angle sum of a triangle differs at most infinitesimally” from two right angles.

3.3.5 Decidability of Intersection of Lines

Fig. 16

Bachmann’s Lotschnittaxiom (Postulate 4)

This axiom corresponds to a simple decidability property. However, it holds a special place in this study. Indeed, we previously studied the impact of working in an intuitionistic setting in Tarski’s system of geometry [18]. During this work, we were trying to either prove that Axiom 1 could be derived from the axioms of Tarski’s system of geometry with decidable point equality or find an argument justifying its independence. Once we discovered its close relationship with the parallel postulates, we started to investigate which versions of the parallel postulates were implying it. Thus Axiom 1 can be considered as the starting point of the classification of the parallel postulates that we present in this paper.

3.3.6 Archimedes’ Axiom

Archimedes’ axiom can be expressed almost directly using the betweenness and congruence predicates. Following Duprat’s work [27], we defined it inductively without introducing the natural numbers. To state Archimedes’ axiom, we first formalized the fact that “there exists some positive integer n and $n+1$ points $A_1, \ldots , A_{n+1}$ on line AB, such that $A_j$ is between $A_{j-1}$ and $A_{j+1}$ for $2< j < n$, $A_j A_{j+1}$ and AB are congruent for $1< j < n$, $A_1 = A$ and $A_{n+1}=C$” as the Grad predicate. This predicate and its variants, which will be presented in Sect. 7.3, represent the only inductive definitions of our library. Actually, we will not specify that “D is between $A_1$ and $A_{n+1}$” in our definition but we will use the definition for non-strict comparison between segments from [57].

This predicate corresponds to Definition 5.4 of [57]. A segment AB is said to be less than or equal to another one CD if one can construct a point E such that this point is between C and D and the segments AB and CE are congruent. For convenience, this witness, which is needed for proving different properties about this order relation, is omitted by this predicate.

Using this predicate, it suffices to assert that $CD \le A_1 A_{n+1}$, which allow us to set $A_1 = A$ and to have $A_1, \ldots , A_{n+1}$ on line AB.

Grad A B C expresses that C is on the graduation based on the segment $\overline{AB}$. Then, this definition allows us to define Archimedes’ axiom in a straightforward manner.

3.3.7 Aristotle’s Axiom

Before defining Aristotle’s axiom, we need to introduce the notion of strict comparison between segments.

This predicate corresponds to Definition 5.14 of [57]. The reason for the non-strict comparison to appear before the strict one is simple. Unlike Hilbert, Tarski uses a non-strict betweenness relation. In order to obtain a strict comparison of segments, it suffices to exclude the case where they are congruent.

We are now ready to state Aristotle’s axiom.

Fig. 17

Aristotle’s axiom (Axiom 3)

This axiom is very close to the statement from Greenberg [34] that we gave in Sect. 3.1.2. Here the acute angle is the angle $\angle ABC$ (Fig. 17). Compared to Greenberg’s statement, we had to add the condition that this angle is non-null.¹² Moreover, since the triangle BXY can be proved non-degenerate from the other assumptions, we can establish that X is the foot of the perpendicular from Y to the other side of the angle by specifying that BXY is a right triangle with the right angle at vertex X. The other subtle difference is the fact that our version states the existence of both points X and Y. This is due to the fact that one cannot define a function for the orthogonal projection in our current axiom system. In order to obtain such a function, one would either need a stronger axiom system where one would introduce function symbols in the axioms which are not already quantifier-free, or one would require an extra axiom. For example, one could have used the constructive_definite_description axiom provided by the standard library:

It allows us to convert a relation which has been proved to be functional to a proper Coq function. As the use of the $\epsilon$ axiom turns the intuitionistic logic of Coq into an almost classical logic [13], we decided to avoid adding this axiom.

3.3.8 Greenberg’s Axiom

Fig. 18

Greenberg’s axiom (Axiom 4)

As for Aristotle’s axiom, this axiom does not differ much from Greenberg’s statement seen in Sect. 3.1.2. Again the acute angle is the angle $\angle ABC$ (Fig. 18). The ray r is given through point R. In order to make sure this ray is well defined we had to add the condition that points Q and R are different. Finally the point S asserted to exist corresponds to the point R from the statement given by Greenberg.

Both of these axioms are consequences of Archimedes’ axiom, but not conversely [32, 34]. Indeed Aristotle’s axiom is a weaker axiom than Archimedes’ axiom and Greenberg’s axiom is a consequence of Aristotle’s axiom.

4 Postulates Equivalent to Playfair’s Postulate

In this section, we present the postulates which are $\mathcal {N}_{LJ}$-equivalent to Playfair’s postulate in planar neutral geometry. Some of these properties are expressed using definitions present in [57]. Thus we also give these definitions in this section. Then we will discuss the formalization of the equivalence proofs.

4.1 Statements of Postulates Equivalent to Playfair’s Postulate

Here, we introduce eight postulates which are $\mathcal {N}_{LJ}$-equivalent to Postulate 2 (Playfair’s postulate). They correspond to properties about various subjects, namely parallelism, perpendicularity, angles and distance. This variety of subjects represents a specificity of the parallel postulate. We will see in the next subsection how this variety affected the way we proved the equivalence of all of these statements.

Fig. 19

Postulate of transitivity of parallelism (Postulate 5)

The first of these postulates (Fig. 19) is the postulate of transitivity of parallelism. It states that, given two lines $A_1 A_2$ and $C_1 C_2$ parallel to the same line $B_1 B_2$, these lines are also parallel. This postulate, which corresponds to Proposition I.30 in [28] and Satz 12.15 in [57], would have been inconsistent with the other axioms if we would have taken Euclid’s definition of the parallelism (wikipedia’s translation), which matches what we identify as strict parallelism:

“Parallel straight lines are straight lines which, being in the same plane and being produced indefinitely in either direction, do not meet one another in either direction.”

Indeed, it is possible for lines $A_1A_2$ and $C_1C_2$ to be equal. One should notice here that again definitions are essential.

Fig. 20

Midpoint converse postulate (Postulate 6)

This postulate (Fig. 20) is a part of the converse of the midpoint theorem and corresponds to a special case of the intercept theorem. We will therefore refer to it as midpoint converse postulate. This postulate expresses that, in a non-degenerate triangle ABC, the intersection point Q of side AC with the parallel to a side AB which passes through the midpoint P of side BC is the midpoint of side AC. One should notice that the midpoint theorem is valid in planar neutral geometry, whereas its converse is equivalent to the parallel postulate. Indeed, it follows easily from the Satz 13.1 of [57]. It is interesting to remark that the second part of the converse of the midpoint theorem, namely that, in any triangle, the midline (the segment $\overline{P Q}$ on Fig. 20) is congruent to half of the basis (the segment $\overline{A B}$ on Fig. 20), is equivalent to another statement of the parallel postulate which is strictly weaker than the triangle postulate in the theory of metric planes [4, 6].

Fig. 21

Alternate interior angles postulate (Postulate 7)

This postulate (Fig. 21) is commonly known as alternate interior angles theorem. It asserts that a line falling on parallel lines makes the alternate angles equal to one another. One can remark that this postulate, like others, was a proposition in [28] (a part of Proposition I.29) as well as in [57] (Satz 12.21). However, Satz 12.21 of [57] is an equivalence and enunciates more than the alternate interior angles theorem. One side of the equivalence corresponds to the alternate interior angles theorem, while the other corresponds to its converse, which is valid in neutral planar geometry, just as for the previous postulate.

Fig. 22

Consecutive interior angles postulate (Postulate 8)

This postulate (Fig. 22) is commonly known as consecutive interior angles theorem. It states that a line falling on parallel lines makes the sum of interior angles on the same side equal to two right angles. It was proved together with the previous postulate in [28] (as a part of Proposition I.29) but not in [57], since the notion of supplementary angles is never introduced in this book. Similarly to the triangle postulate, we formalized this postulate slightly differently, as it precisely formulates that the sum is equal to a straight angle.

With a view to defining the next postulate, we need to define perpendicularity, something which we postponed. We adopted the definition given in [57], which used the following intermediate definition.

We recall that we already defined a predicate for right triangles, but this definition included the case where the sides of the right angle could be degenerate. Therefore, in order to define perpendicularity using this predicate, one must know the intersection point of the perpendicular lines and exclude the case of the degenerate right triangle. ${A B} \mathbin {\underset{X}{\perp }} {C D}$ means that lines AB and CD meet at a right angle in X (Fig. 23). The part of the definition that specifies that any point on the first line together with any point on the second line and the intersection point form a right angle is essential to the possibility of choosing any couple of different points to represent the lines.

This predicate and the previous one correspond to Definition 8.11 of [57]. Most of the time, we just want to consider the perpendicularity of two lines AB and CD without specifying the point in which they meet. In such cases, we will use ${A B} \mathbin {\perp } {C D}$.

Fig. 23

Definition of Perp_at

Fig. 24

Perpendicular transversal postulate (Postulate 9)

This postulate (Fig. 24) is commonly known as perpendicular transversal theorem. It expresses that given two parallel lines, any line perpendicular to the first line is perpendicular to the second line. Just as for the previous postulates, the converse of the perpendicular transversal postulate is valid in neutral planar geometry. It corresponds to Satz 12.9 in [57] and the perpendicular transversal postulate corresponds to a special case of Satz 12.22 in [57].

This postulate (Fig. 25), which will be designated as postulate of parallelism of perpendicular transversals, is less known than the previous ones. This is probably due to the fact that it can be easily deduced from the perpendicular transversal postulate and its converse. This could explain why it does not appear as a proposition in the most well-known axiomatic developments of Euclidean geometry, which are those of Euclid [28], Hilbert [37] and Tarski [57]. Nevertheless, it is listed amongst the statements equivalent to the parallel postulate in [33, 44]. It asserts that two lines, each perpendicular to one of a pair of parallel lines, are parallel. It is easy to take this property for granted and assume it implicitly since it corresponds to Satz 12.9 in [57], which is valid in neutral planar geometry, when the two lines known to be parallel are equal.

Fig. 25

Postulate of parallelism of perpendicular transversals (Postulate 10)

Fig. 26

Universal Posidonius’ postulate (Postulate 11)

This postulate (Fig. 26) is a property of parallel lines in Euclidean geometry which was taken as definition of parallelism by Posidonius. We will refer to it as universal Posidonius’ postulate because another postulate (Postulate 22), known as Posidonius’ postulate, can be expressed in a similar way with the exception that the points $A_1$, $A_2$, $B_1$ and $B_2$ are quantified existentially and not universally and that the hypothesis of parallelism is replaced by a non-degeneracy condition. It states that, if two lines $A_1 A_2$ and $B_1 B_2$ are parallel, then they are everywhere equidistant. This can be formalized by specifying that any two points $B_3$ and $B_4$ on $B_1 B_2$ form with the feet of the orthogonal projection of these points onto the line $A_1 A_2$, respectively $A_3$ and $A_4$, congruent segments. However, as we will later see, everywhere equidistant lines only exist in Euclidean geometry. This statement being equivalent to the parallel postulate motivates the fact that we list all of the definitions we chose, since, as already mentioned, definitions are critical when studying statements of the parallel postulate.

The last postulate we will analyze in this section is a special case of Playfair’s postulate where one of the parallel lines shares a common perpendicular with its parallel. Thus, to state this postulate, we first present a refinement of this property which was defined in [57].

Fig. 27

Definition of Perp2

This predicate corresponds to Definition 13.9 of [57]. not only means that the lines AB and CD have a common perpendicular XY but also that XY passes through the point P (Fig. 27). One should remark that implies, in neutral planar geometry, that the lines AB and CD are parallel. However, not any pair of parallel lines share a common perpendicular. In fact, in hyperbolic geometry, ultraparallel lines only share a unique common perpendicular, and limiting parallels do not share any common perpendicular [21]. Therefore, even in the case of ultraparallel lines, there may be no common perpendicular passing through a given point, since it suffices that this point lies outside their unique common perpendicular.

Fig. 28

Alternative Playfair’s postulate (Postulate 12)

Because of the similarity of Postulate 12 (Fig. 28) with Postulate 2 (Playfair’s postulate) we decided to name it alternative Playfair’s postulate. It asserts that any line parallel to a given line passing through a given point is equal to the line that passes through the given point and shares a common perpendicular with the given line that passes through the given point. One should mention that this postulate does not have the same importance as the other ones, because its role is just to simplify the proofs.

4.2 Formalizing the Equivalence Proof

In this subsection, we focus on the formalization of the proof that the postulates of the previous subsection (Postulates 5–12) are indeed $\mathcal {N}_{LJ}$-equivalent to Postulate 2 (Playfair’s postulate). To make sure it holds, it suffices to prove it within the context of the Tarski_2D type class from Table 2. Thus we need a definition for an n-ary equivalence relation. We use the following definition using lists:

We chose to define this n-ary equivalence relation as a predicate on list of propositions. This list of propositions contains the equivalent predicates. This predicates expresses that any two propositions in this list are equivalent. It allows us to reduce the proof of the equivalence or the implication between two properties by checking the membership of these properties to a list. The Coq statement corresponding to the equivalence of any two of Postulates 2, 5–12 is the following.

In order to lower the number of equivalences to be proven to complete the proof of the previous theorem, we introduced an alternative predicate for n-ary equivalence relation and proved its equivalence with all_equiv.

This definition corresponds to the usual technique to prove equivalences that minimize the number of implications to be proved. Indeed, for a list of length n, n implications would suffice. This is much better than the $2 n^2$ implications required from all_equiv. In Coq, it is convenient to have the two definitions, one for proving that a list of statements are equivalent and the other to use these equivalences.

In practice the all_equiv’ definition is also useful to improve the compilation time of our proofs. Indeed, to prove the n-ary equivalence statements, we put in the context all the implications proved previously manually and we let the tautology checker of Coq (tauto) complete the proof. This technique is convenient, but does not scale well when one uses all_equiv and the number of statements is large. Figure 29 provides a graphical summary of the implications we formalized to prove Theorem 1. On this figure, a circle with a number n in its center represents Postulate n, an arrow between two circles represents an implication, and a double-headed arrow represents an equivalence. One can observe that most of the implications (eight out of fourteen) that we proved involve Postulate 2 (Playfair’s postulate). Indeed, since these postulates correspond to properties about diverse subjects, we found that it was more straightforward, when proving the implication between properties about different subjects, to use parallelism as one of the two subjects. Postulate 2 and Postulate 5 (Postulate of transitivity of parallelism) are the only two postulates about parallelism. Moreover, we have proved that the equality of lines is decidable in planar neutral geometry assuming decidability of point equality, while we could only prove the decidability of parallelism assuming Postulate 5. Therefore, Postulate 2 can be proved by contradiction, whereas Postulate 5 cannot unless we find a proof of the decidability of parallelism valid in planar neutral geometry. Indeed, unless the conclusion is known to be decidable, one cannot use a proof by contradiction to derive it, because the proof by contradiction is not valid in an intuitionistic setting. We should point out that, in the definition of parallelism, the fact that the lines do not meet can be proved by proof of negation,¹³ while the rest of this definition can be proved by contradiction. However, proving the parallelism in such a way is more tedious than proving the equality of lines by contradiction. This explains why Postulate 2 has such a central role in the formalization of Theorem 1. Thus we only proved implications between properties about the same subject, such as the alternate interior angles postulate and the consecutive interior angles postulate, besides these eight implications.

Fig. 29

Overview of the proofs of Sect. 4

With a view to keeping a good balance between mathematical aspects, formalization aspects, and explanations, we decided to focus on only one implication which illustrates the impact of working in an intuitionistic setting rather than a classical one. The reader who is interested in the proofs of the implications can find some of them in the literature.¹⁴ In [57], there is a proof of the implication from Postulate 2 to Postulate 5 (Satz 12.15). In [11], the implication from Postulate 2 to Postulate 7 (Lemma 6.6) as well as the implication from Postulate 2 to Postulate 5 (Lemma 6.8) are proved. Finally, in [44], proofs of the equivalence between Postulate 7 and Postulate 8 (Theorem 21.4) and of the implication from Postulate 9 to Postulate 10 (Theorem 23.7) are provided.

Putting together the implications from Fig. 29, we can prove the following theorem.

Theorem 1

Postulates 2, 5–12 are $\mathcal {N}_{LJ}$-equivalent.

Let us now focus on the proof of the implication from Postulate 6 (Midpoint converse postulate) to Postulate 2 (Playfair’s postulate). In order to present the proof that we formalized, we will collect the lemmas that will be used throughout this proof. We believe it is important to list these lemmas, since we saw that it often happens that a statement is valid in neutral planar geometry and that its converse is equivalent to the parallel postulate. By detailing these lemmas and only deriving new facts from the application of these lemmas in our proofs, we make sure we do not implicitly apply a statement equivalent to the parallel postulate, unless we have proved it to follow from the statement from which we are proving a consequence. However, we chose not to include trivial lemmas which state permutation properties of the predicates (e.g. ${A B}\mathbin {\parallel } {C D} \Rightarrow {C D}\mathbin {\parallel } {A B}$). We also decided to omit lemmas allowing to weaken a statement (e.g. ${A B}\mathbin {\parallel _s} {C D} \Rightarrow {A B}\mathbin {\parallel } {C D}$). Besides, one problem one encounters with Tarski’s system of geometry is the fact that there is no primitive type line. Therefore, when considering a line, one represents it by two different points. This implies that we need a lemma such as $C \ne D' \Rightarrow {A B}\mathbin {\parallel } {C D} \Rightarrow {{\mathrm{Col}}}\, {C} \, {D} \, {D}' \Rightarrow {A B}\mathbin {\parallel } {C D'}$. This kind of lemma are easily proven in neutral geometry. Moreover, the proofs of collinearity can be automated by a reflexive tactic that we developed in [19]. Therefore we will simply use them implicitly, as one would do in a pen-and-paper proof.

Lemma 1

(6.21¹⁵) Two points are equal if they are at the intersection of two different lines.

Lemma 2

(7.8) The symmetric of a point with respect to another point is constructible.

Lemma 3

(7.17) There is only one midpoint to a given segment.

Lemma 4

¹⁶A line PQ which enters a triangle ABC on side AB and does not pass through C must exit the triangle either on side $\overline{AC}$ or on side $\overline{BC}$.

Proposition 1

Postulate 6 implies Postulate 2.

Fig. 30

Postulate 6 implies Postulate 2

Proof

Given that ${A_1 A_2}\mathbin {\parallel } {B_1 B_2}$, ${A_1 A_2}\mathbin {\parallel } {C_1 C_2}$, ${{\mathrm{Col}}}\, {P} \, {B_1} \, {B_2}$ and ${{\mathrm{Col}}}\, {P} \, {C_1} \, {C_2}$, we wish to prove that $B_1$, $B_2$, $C_1$ and $C_2$ are collinear (Fig. 30). We can first eliminate the cases where line $A_1 A_2$ is equal to $B_1 B_2$ and/or $C_1 C_2$. Indeed, if all three lines are equal, we are trivially done, and if two lines are equal and strictly parallel to the third one, then we may also conclude, as we can also prove that this last case is impossible because the lines meet in P. So we may now assume ${A_1 A_2}\mathbin {\parallel _s} {B_1 B_2}$ and ${A_1 A_2}\mathbin {\parallel _s} {C_1 C_2}$. We can then construct the symmetric point X of $A_1$ with respect to P using Lemma 2. Now we will prove that there exists a point $B_3$ on line $B_1B_2$ which is strictly between $A_2$ and X. We know that P is either different from $B_1$ or from $B_2$, as otherwise it would contradict ${A_1 A_2}\mathbin {\parallel _s} {B_1 B_2}$. Let us prove the existence of the point $B_3$ by using Lemma 4 in the triangle $A_1A_2X$ with either line $PB_1$ or $PB_2$, depending on whether P is distinct from $B_1$ or $B_2$. We prove the hypotheses of this lemma in the same way in both cases, so let us only consider the case where P and $B_1$ are distinct. The hypotheses $\lnot {{\mathrm{Col}}}\, {A_2} \, {P} \, {B_1}$ and $\lnot {{\mathrm{Col}}}\, {A_1} \, {X} \, {B_1}$ can be proven by proof of negation. Indeed, assuming ${{\mathrm{Col}}}\, {A_2} \, {P} \, {B_1}$ would contradict ${A_1 A_2}\mathbin {\parallel _s} {B_1 B_2}$, and assuming ${{\mathrm{Col}}}\, {A_1} \, {X} \, {B_1}$ would contradict $P \ne B_1$, as these two points would be on lines $PA_1$ and $PB_1$ and Lemma 1 would imply that they are equal. Finally, $B_3$ cannot be between $A_1$ and $A_2$, as assuming would contradict ${A_1 A_2}\mathbin {\parallel _s} {B_1 B_2}$. Hence, Lemma 4 lets us derive the existence of the point $B_3$ on line $B_1B_2$ which is strictly between $A_2$ and X. In the same way, we can prove there exists a point $C_3$ on line $C_1C_2$ which is strictly between $A_2$ and X. Now, it suffices to prove that $B_3$ and $C_3$ are equal, as it implies that $B_1$, $B_2$, $C_1$ and $C_2$ are collinear. From Postulate 6 and Lemma 3, we know that they both are the midpoint of the segment $\overline{A_2 X}$ and are therefore equal. This completes the proof. $\square$

The proof of Proposition 1, while being simple, illustrates the impact of working in an intuitionistic setting rather than a classical one. Indeed, in this proof we assert the existence of points at the intersection between two lines, namely the points $B_3$ and $C_3$. Since we do not assume Axiom 1 (decidability of intersection of lines), these points can be proved to exist without reasoning by cases on the possibility for some lines to intersect. However, it often happens that, in a proof, the existence of a point at the intersection between two lines is derived by contradiction, rendering it only valid in a classical setting. Thus, with a view to prove Theorem 1, we had to be very careful not to employ such arguments.

5 Postulates Equivalent to Tarski’s Parallel Postulate

This section follows the same outline to that used in the previous section. First, we present the postulates which are $\mathcal {N}_{LJ}$-equivalent to Postulate 1 (Tarski’s parallel postulate), together with the necessary definitions. Second, we will discuss the formalization of the equivalence proofs.

5.1 Statements of Postulates Equivalent to Tarski’s Parallel Postulate

We introduce here eight new postulates. All are $\mathcal {N}_{LJ}$-equivalent to Tarski’s parallel postulate. Three pairs among these eight postulates could appear to be quite similar. Two of these pairs even express a seemingly analogous property, or so it would seem. We will examine the slight differences which, while considering a pair of these postulates, render unclear whether one is stronger, equivalent or weaker than the other one. These postulates will correspond to properties about parallelism, intersection, perpendicularity, triangles or angles. As in the previous section, the subjects of these postulates are widely different.

Fig. 31

Proclus’ postulate (Postulate 13)

The first of these postulates (Fig. 31) is known as Proclus’ postulate. It asserts that if a line intersects one of two parallel lines, then it intersects the other. One can remark that this statement is the contrapositive of Postulate 5 (the postulate of transitivity of parallelism). It is constructively stronger than its contrapositive, which follows from the fact that in intuitionistic logic, an implication is not equivalent to its contrapositive. In fact, only one of the implications remains valid when dropping the law of excluded middle, namely $(P \Rightarrow Q) \Rightarrow (\lnot Q \Rightarrow \lnot P)$.

Fig. 32

Alternative Proclus’ postulate (Postulate 14)

This postulate (Fig. 32) is a special case of Postulate 13. Compared to it, Postulate 14 presents the same modifications as the one we applied to Postulate 2 (Playfair’s postulate) to obtain Postulate 12 (Alternative Playfair’s postulate). Therefore we decided to name it alternative Proclus’ postulate. We recall that there may be more than one parallel to a given line passing by a given point. Thus considering a particular one can be more convenient. We would like to stress that this postulate, unlike the next postulates which will resemble another previously defined postulate, really is just defined as a mean to ease some proofs of implication.

Fig. 33

Triangle circumscription principle (Postulate 15)

This postulate (Fig. 33) is referred to as triangle circumscription principle in [11]. It states that for any three non-collinear points there exists a point equidistant from them. This version was originally used by Szmielew as an axiom, but later Schwabhäuser chose Postulate 1 (Tarski’s parallel postulate) over it [11]. This postulate was the triggering factor for this study. Indeed, we used this version of the parallel postulate in [18], since we could derive Axiom 1 (the decidability of intersection of lines) from it. Thus we wanted to investigate whether or not the same could be done with Tarski’s parallel postulate.

Fig. 34

Inverse projection postulate (Postulate 16)

This postulate (Fig. 34) expresses that, for any given acute angle, any perpendicular raised from a point on one side of the angle intersects the other side. It will be designated as inverse projection postulate. It is interesting to notice that although this postulate belongs to the strongest class of postulates that we will consider, a modification of its statement (Postulate 31) would render it much weaker to the point that it would belong to the weakest class of postulates we will consider. It could seem like it trivially implies Postulate 1 (Tarski’s parallel postulate). Indeed, one could think it suffices to construct the orthogonal projection of the considered point on the bisector of the angle (which makes an acute angle with both sides of the angle) and, with the inverse projection postulate, to assert the existence of a point on each side of the angle which is collinear with these two points. However, betweenness properties required in the statement of Postulate 1 would not be satisfied, and one would not be able to prove the implication in such a fashion.

The next postulates that we will present were introduced by Beeson [11]. In this paper, Beeson uses strict betweenness, similarly to Hilbert. Since we assume the axioms of Tarski’s system of geometry, in which the betweenness is non-strict, we need to define the strict betweenness.

In [10], Beeson mentions that the strict and non-strict betweenness “are interdefinable (even constructively)”. We adopted his definition of the strict betweenness in terms of the non-strict betweenness. One can remark that, since we assumed the decidability of point equality, in case we would have had to define the non-strict betweenness in terms of the strict betweenness, we could have adopted a simpler version of Beeson’s definition. Actually, he applies Gödel–Gentzen translation to the formula that we would have chosen to obtain a constructively valid definition. We could have chosen to define as , while he defines it . Nevertheless, under the assumption of the decidability of point equality, these two definitions are equivalent.

Fig. 35

Euclid 5 (Postulate 17)

This postulate (Fig. 35) is the first of two postulates introduced in [11] by Beeson. It is a formulation of Euclid’s parallel postulate in Tarski’s language. He denotes it as Euclid 5. He writes that Euclid 5 is

“If a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if produced indefinitely, meet on that side on which are the angles less than the two right angles.”

He reads “make the interior angles on the same side less than two right angles” into line PU being in the interior of the angle $\angle QPR$ while lines PR and QS make consecutive interior angles¹⁷ with PQ equal to two right angles. Seeing that, in neutral planar geometry, making consecutive interior angles equal to two right angles is the same as making alternate interior angles equal, he uses this equivalent statement. In his definition, given that the two straight lines that make alternate interior angles equal are PR and QS, he formulates it as the quadrilateral PRQS having its diagonals meeting in their midpoint. Yet, it is not obvious that a quadrilateral having its diagonals meeting in their midpoint means that their opposite sides make alternate interior angles equal. This property follows from Satz 7.13 of [57], which is provable in neutral planar geometry and uses the definition of angle congruence.

Fig. 36

Strong parallel postulate (Postulate 18)

This postulate (Fig. 36), also introduced and named as strong parallel postulate by Beeson in [11], results of the modification of Euclid 5. Both its hypotheses and its conclusion are weaker compared to it. The point U defined in the previous postulate is not supposed to lie inside one of the considered alternate interior angles, but to lie outside line PR. That is, the interior angles on the same side are no longer required to make less than two right angles, but prevented to sum exactly to two right angles. Moreover, the strict betweenness predicates in the conclusion are replaced by collinearity predicates. That is, the two straight lines making interior angles which do not sum to two right angles are asserted to meet without any indication on the side of this intersection. Finally, contrary to Postulate 17, the lines PR and SQ can be equal. This hypothesis was crucial for Postulate 17 as it avoids the case where $P = U$, in which the postulate is false. Because both the hypotheses and the conclusion are weaker compared to Euclid 5, it is not evident whether these modifications render the strong parallel postulate stronger than Euclid 5, equivalent, or weaker.

To have a more faithful version of Euclid’s parallel postulate we introduced a variant of Postulate 17 (Euclid 5). For this sake, we stated this variant in terms of sum of angles. We first introduce a variant of Postulate 18 (Strong parallel postulate) stated in terms of sum of angles.

Fig. 37

Alternative strong parallel postulate (Postulate 19)

This postulate (Fig. 37) greatly resembles the previous one. Therefore we decided to name it alternative strong parallel postulate. In this version we make explicit the concept of sum of angles. In the same fashion as for the triangle postulate, the fact that the interior angles on the same side do not sum to exactly two right angles is formulated as this sum not being equal to a straight angle. Furthermore, one can notice that, compared to the previous postulate, the lines AB and CD, which correspond to the lines PR and QS, are not equal. This is a due to the hypothesis stating that A and D are on the same side of line BC. Nonetheless, since in the axiom system we adopted, the degenerate case of this statement is trivial and the line equality is decidable, this difference does not impact the possibility for these two postulates to be equivalent.

To define a variant of Euclid 5 making an explicit use of the concept of sum of angles, we need to be able to characterize the property for two angles to make less than two right angles. Incidentally, a property very similar to this one is essential when considering the sum of angles. According to Rothe [56], if this property is not satisfied, the considered angles cannot be added, because “the sum would be an over-obtuse angle”. In fact, the sum of angles is neither an order-preserving function nor an associative function when some of the considered sums correspond to over-obtuse angles. For example, $160^{\circ } = (20^{\circ } + 170^{\circ }) + 30^{\circ } \ne 20^{\circ } + (170^{\circ } + 30^{\circ }) = 180^{\circ }$.

The name of this predicate is the abbreviation for sum at most straight. Two angles $\angle ABC$ and $\angle DEF$ do not make an over-obtuse angle if there exists a point J such that ${C} \, {B} \, {J} {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$, the angles $\angle ABC$ and $\angle CBJ$ are adjacent and the angle $\angle ABJ$ is not an over-obtuse angle. As for the definition of sum of angles (SumA), we specified that angles $\angle ABC$ and $\angle CBJ$ are adjacent by the fact that A and J are not on the same side of line BC, to do without the disjunction of cases between the cases where at least one of the angles is degenerate and the case where both angles are non-degenerate and A and J are on opposite sides of line BC. Interestingly, by formalizing straightforwardly “do not make an over-obtuse angle”, one also avoids such a disjunction of cases. This predicate almost corresponds to property for two angles to make less than two right angles. It just does not exclude the case where the two angles make exactly two right angles. Analogously to the predicates for order relations on segments and angles, it is straightforward to exclude this case.

Fig. 38

Euclid’s parallel postulate (Postulate 20)

This variant (Fig. 38) of Postulate 17 (Euclid 5) being intended as a more faithful version of Euclid’s parallel postulate, we will refer to it as Euclid’s parallel postulate. One can notice that, compared to Postulate 17 (Euclid 5), the strict betweenness predicates in the conclusion are replaced by Out predicates (we recall that Out B A Y expresses that Y belongs to the ray BA). This weakening of the conclusion is due to the fact that, in this version, we state the hypothesis that the considered lines “make the interior angles on the same side less than two right angles” without referring to an angle in which one of these lines lies, namely PU being in the interior of the angle $\angle QPR$ in the definition of Postulate 17. Since lying in an angle was expressed in terms of betweenness, it allowed us to be more precise regarding the position of the intersection of the considered lines. This statement is really close to the three previous postulates. However, once more, since both its hypotheses and its conclusion are either stronger or weaker than the ones of these three postulates, it is not obvious that they are equivalent.

5.2 Formalizing the Equivalence Proof

This subsection is dedicated to the formalization of the proof that the postulates of the previous subsection (Postulates 13–20) are indeed $\mathcal {N}_{LJ}$-equivalent to Postulate 1 (Tarski’s parallel postulate) as well as the formalization of the proof that the postulates of Sects. 4.1 and 5.1 are indeed $\mathcal {N}_{LK}$-equivalent to Postulate 2 (Playfair’s postulate) and Postulate 1 (Tarski’s parallel postulate). As in the previous proof of equivalence, these equivalences are proved in the context of the Tarski_2D type class from Table 2. The Coq statement corresponding to the $\mathcal {N}_{LJ}$-equivalence of any two of Postulates 1, 13–20 is the following.

A graphical summary of the implications that we formalized to prove Theorem 2 is displayed on Fig. 39. The circles around Postulates 2, 5–12 and around Postulates 1, 13–20 mean that the postulates inside these circles are $\mathcal {N}_{LJ}$-equivalent. One could think that Postulate 1 does not imply Postulate 15 (the triangle circumscription principle) in an intuitionisctic logic. Indeed, in order to prove this implication, we proved that Postulate 1 implies Postulate 2, which implies Postulate 9 (the perpendicular transversal postulate), itself implying Postulate 15.

Fig. 39

Overview of the proofs of Sect. 5

In fact, even if Postulate 9 ($\mathcal {N}_{LJ}$-equivalent to Postulate 2) does not imply Postulate 15 (equivalent to Postulate 1) in an intuitionisctic logic, we know from Proposition 3 that the decidability of intersection of lines (Axiom 1) follows from Postulate 18, which itself follows from Postulate 1. Furthermore, Proposition 2 demonstrates that, in an intuitionistic logic, assuming Axiom 1 is enough to prove that Postulate 9 implies Postulate 15.

The implications displayed on Fig. 39 allow us to prove the following theorem.

Theorem 2

Postulates 1, 13–20 are $\mathcal {N}_{LJ}$-equivalent and Postulates 1, 2, 5–20 are $\mathcal {N}_{LK}$-equivalent.

In an earlier version of this work, we were proving directly that Postulate 17 (Euclid 5) implies Postulate 18 (the strong parallel postulate). The idea behind this proof was to add an extra hypothesis in Postulate 18, namely that the points P, Q, R and U are coplanar. The motivation behind this idea was double. First, this extra hypothesis is necessary in spaces of dimension higher than two. Second, we could then reason by distinction of cases on the 27 possibilities for these points to be coplanar. This distinction of cases was allowing us to know to which side of lines PR and PS the point U belongs. So we were left with four cases corresponding to the four parts of the plane to which all the considered points belong. We could then use Pasch’s axiom in all of these cases to construct a point permitting to apply Postulate 17 and complete this proof.

We already mentioned that Postulate 1 is valid in spaces of dimension higher than two. This is due to the fact that all the points in its statement are coplanar. Therefore the extra hypothesis that we added to Postulate 18 was not altering the possibility to prove that Postulate 1 follows from it. Because Postulate 1 was the only postulate that was proved to directly follow from Postulate 18, we could then prove that this modified version was equivalent to the postulates of Sect. 5.

This proof was really tedious, even though we could slightly simplify it when we proved that, in the context of planar neutral geometry with decidable point equality, the upper 2-dimensional axiom was equivalent to the fact any four points are coplanar. In doing so, we were in fact proving the “two-sides” principle from [11] without relying on Axiom 1. This principle asserts that two points A and B not on a line l are either on the same side of l or on opposite sides of l. We would like to stress that this demonstrates a profound difference between the axiom system we adopted and Beeson’s modification of Tarski’s axioms [10] to which the results of [11] apply. Indeed, according to Theorem 10.3 from [11], the “two-sides” principle is not provable. Therefore this proof could not be done in his system, which is why he proved that Postulate 17 implies Postulate 18 by showing that “Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically”.

In the current version of this work, this proof is not present anymore. Indeed, when we started to consider Postulate 19 (the alternative strong parallel postulate) and Postulate 20 (Euclid’s parallel postulate) we realized that it was straightforward to prove not only the implication from Postulate 17 to Postulate 20 but, more surprisingly, also the one from Postulate 20 to Postulate 19. This is a result of the fact we started to consider these postulates after the development of a small library for the sum of angles which proved very useful for this proof. Moreover, the proof that Postulate 19 implies Postulate 18 was also not as cumbersome as the proof of the implication from Postulate 17 to Postulate 18. As a matter of fact, we had already proved that Postulate 13 (Proclus’ postulate). implies Postulate 18 and we found a proof of the implication from Postulate 19 to Postulate 13 which was quite direct to formalize. The major idea behind this proof was to use two intermediary steps, namely Postulate 16 (the inverse projection postulate) and Postulate 14 (Alternative Proclus’ postulate). The purpose of using these postulates as an intermediary steps was that they feature hypotheses which could be translated into each other with ease. This highlights a central issue when working with parallel postulates: the variety of the properties which are used to state the different postulates. When proving the equivalence between parallel postulates, one should be careful to which implication one will prove, since the difficulty to translate one property into another is far from being constant.

Similarly to the previous section we will only focus on a few proofs, namely Proposition 2 and Proposition 3. We chose to focus on these proofs because they are the only implications that involve Axiom 1. Unlike the previous section, up to our knowledge, the only synthetic and intuitionistic proofs of Sect. 5 which can be found in the literature are the implication from Postulate 1 to Postulate 17. This implication is proved in [10] (Theorem 8.3). In order to present the proof of Proposition 2, we will collect four lemmas that will be used throughout this proof.

Lemma 5

(8.22) Midpoints are constructible.

Lemma 6

Given two distinct points, their perpendicular bisector is constructible.

Lemma 7

(12.9) Two lines perpendicular to the same line are parallel.

Lemma 8

(12.17) If A and B are distinct and if the segments $\overline{AC}$ and $\overline{BD}$ have the same midpoint, then the lines AB and CD are parallel.¹⁸

The following proposition is a classic, but we still give the proof, because we are in a intuitionistic setting and we want to emphasize the use of the decidability of intersection.

Proposition 2

Axiom 1 and Postulate 9 imply Postulate 15.

Fig. 40

Axiom 1 and Postulate 9 imply Postulate 15

Proof

Given a non-degenerate triangle ABC we wish to prove the existence of point $C_C$ equidistant to A, B and C (Fig. 40). Lemma 6 lets us construct the perpendicular bisector $C_1C_2$ of the segment $\overline{AB}$ and the perpendicular bisector $B_1B_2$ of the segment $\overline{AC}$, since they are non-degenerate segment as ABC is a non-degenerate triangle. We now prove that it is impossible for lines $B_1B_2$ and $C_1C_2$ to not intersect to prove the existence of this intersection.¹⁹ Assuming they do not intersect, then lines $B_1B_2$ and $C_1C_2$ are parallel by definition. Using the perpendicular transversal postulate we can deduce that lines AC and $C_1C_2$ are perpendicular. Finally Lemma 7 establishes that lines AB and AC are parallel as they are both perpendicular to line $C_1C_2$. This implies that A, B and C are collinear, which is false by hypothesis. Since it is impossible for lines $B_1B_2$ and $C_1C_2$ to not intersect, Axiom 1 lets us assert that $C_c$ is their intersection point, which is equidistant from A and B since it belongs to its perpendicular bisector and equidistant from A and C since it belongs to its perpendicular bisector. $\square$

Proposition 3

Postulate 18 implies Axiom 1.

Fig. 41

Postulate 18 implies Axiom 1

Proof

Given 4 points that we name P, Q, S and U (rather than A, B, C and D, to work with the same name as those in the definition of the strong parallel postulate) we wish to prove that either there exists a point I such that ${{\mathrm{Col}}}\, {I} \, {S} \, {Q}$ and ${{\mathrm{Col}}}\, {I} \, {P} \, {U}$ or that there does not exist such a point (Fig. 41). We first eliminate the case where P lies on QS in which there exists such a point I, namely it is P. So we may assume that $\lnot {{\mathrm{Col}}}\, {P} \, {Q} \, {S}$ and we then eliminate the case of P and U being equal, as again there exists such a point I, namely Q (we could have also taken S to be this point). So we may assume P and U to be different. Now we construct the midpoint T of the segment $\overline{PQ}$, using Lemma 5, and the symmetric point R of S with respect to T, using Lemma 2. Finally we will distinguish two cases. Either $\lnot {{\mathrm{Col}}}\, {P} \, {R} \, {U}$ and the strong parallel postulate asserts there exists such a point I, provided that and , which we easily prove as P and Q are different and $\lnot {{\mathrm{Col}}}\, {P} \, {Q} \, {S}$. The other case is when ${{\mathrm{Col}}}\, {P} \, {R} \, {U}$. In this case we can prove that lines QS and PU are strictly parallel, using Lemma 8 and the fact $\lnot {{\mathrm{Col}}}\, {P} \, {Q} \, {S}$, and by definition of two lines being strictly parallel we know that there does not exist such a point I. $\square$

6 Postulates Equivalent to the Triangle Postulate

The same structure that was used in the previous two sections will be used throughout this one. First, we present the postulates which are $\mathcal {N}_{LJ}$-equivalent to Postulate 3 (the triangle postulate), together with the necessary definitions. Second, we will discuss the formalization of the equivalence proofs.

6.1 Statements of Postulates Equivalent to the Triangle Postulate

This subsection will study ten new postulates. All are $\mathcal {N}_{LJ}$-equivalent to the triangle postulate. One, namely Postulate 21, is very similar to Postulate 3 (the triangle postulate) but one could wrongly think it is strictly weaker than it. Furthermore, three pairs of postulates will present the same kind of similarity. Despite these resemblance, the subjects of these postulates are again mostly heterogeneous. In fact, these postulates will affirm properties about triangles, equidistant lines, circles and quadrilaterals.

These two postulates correspond to trivial consequences of Postulate 3 and Postulate 11 (the universal Posidonius’ postulate). Indeed their definitions are nearly the same as those of these last two postulates. Postulate 21 expresses that there exists a triangle whose angles sum to two rights and Postulate 22 expresses that there exists two lines which are everywhere equidistant. They mainly differ in the type of quantifiers used for some of the considered points in these postulates: they replace some of the universal quantifiers by existential ones. Postulate 3 and Postulate 11 are also more general and can be instantiated to cases which are provable in planar neutral geometry. So Postulate 21 and Postulate 22 add non-degeneracy conditions. For example, in the case of the former one adds that the triangle whose angles sum to two rights is non-flat. The latter is particularly interesting because it represents one of the only two postulates²⁰ which is not $\mathcal {N}_{LJ}$-equivalent to its universally quantified version. In this section, we will consider three more pairs of postulates differing in the type of quantifiers, and all of them are $\mathcal {N}_{LJ}$-equivalent. Furthermore, Playfair’s postulate is proved to be equivalent to the existence of a point and line for which there is a unique parallel line passing through the point in [3]. However, we did not formalize this proof since it requires the space to be of dimension higher than two. Indeed, it relies on the existence, for any given plane, of a point not incident to it. The same theorem has also been proven synthetically by Piesyk [55], but his proof needs decidability of intersection of lines.

Fig. 42

Postulate of existence of similar but non-congruent triangles (Postulate 23)

The postulate of existence of similar but non-congruent triangles (Fig. 42) is a simplication suggested by Saccheri to a postulate introduced by Wallis [44]: “To every figure there exists a similar figure of arbitrary magnitude”. It asserts that there exists two similar but non-congruent triangles. Wallis assumed this postulate in order to prove Euclid’s parallel postulate [20] but could have instead assumed Postulate 23. This postulate was also assumed by Laplace [22]. Moreover, Gauss produced a proof of Euclid’s parallel postulate under the assumption of the existence of a right triangle whose area is greater than any given area [41].

Zwar bin ich auf manches gekommen, was den meisten schon für einen Beweis geltend würde, aber was in meinen Augen sogut wie Nichts beweiset, z. B. wenn man beweisen könnte dass ein geradlinigtes Dreieck möglich sei, dessen Inhalt grösser wäre als eine jede gegebne Fläche, so bin ich im Stande die ganze Geometrie völlig streng zu beweisen.²¹

                                                                                                – Carl Friedrich Gauss [29]

It is unclear if the right triangle is required to be similar to another given right triangle. If so,²² and it is probable considering this sentence was part of an informal letter from Gauss to Bolyai, Gauss’ assumption would be a special case of Wallis’ postulate. One should point out that, even though the formalization of this postulate is straightforward, the triangles need to be non-flat, as the non-degeneracy conditions are often omitted in geometry texts.

Fig. 43

Thales’ postulate (Postulate 24), Thales’ converse postulate (Postulate 25) and existential Thales’ postulate (Postulate 26)

Here we discuss simultaneously Postulate 24, Postulate 25 and Postulate 26, because the second one is the converse of the first one. Moreover, the third one corresponds to the result of replacing, in the first or second one, the universal quantifiers by existential ones, and the implication between the hypotheses and the conclusion by a conjunction. Postulate 24 states that, if the circumcenter of a triangle is the midpoint of a side of a triangle, then the triangle is right. Postulate 25 states that, in a right triangle, the midpoint of the hypotenuse is the circumcenter. Finally, Postulate 26 states that there is a right triangle whose circumcenter is the midpoint of the hypotenuse. Figure 43 displays the figure representing the statement of the postulates in the Euclidean plane on the left. A counter-example in Poincaré disk model for Postulate 24 can be found in the center of Fig. 43 and one for Postulate 25 is on the right of Fig. 43. There is no counter-example for Postulate 26, for the reason that it does not state a property that some geometric objects verify in a given configuration, but rather the existence of some geometric objects verifying a given property. Martin qualifies Postulate 24, which is a special case of the inscribed angle theorem (part of Proposition III.31 in [28]), as “certainly one of the oldest theorems in mathematics”. The proofs of Postulate 24 and Postulate 25, as theorems of Euclidean geometry, have already been studied in Coq assuming Tarski’s system of geometry [15]. Nevertheless, Braun et al. proved that they both follow from Postulate 6 (the midpoint converse postulate), which is strictly stronger than both of them. Finally, formalizing these postulates is elementary.

Fig. 44

Definition of Saccheri

We now focus on a postulate due to Saccheri, who made “the most elaborate attempt to prove the ‘parallel postulate”’ according to Coxeter [24] and was “perhaps before its time” [36]. In his attempt to prove Euclid’s parallel postulate, he considered a specific kind of quadrilaterals which have since been named after him. These quadrilaterals arise when one studies points that are equidistant to a line. Indeed, is a quadrilateral such that the angles at A and D are right and ${AB} \mathbin {\equiv } {CD}$ (Fig. 44). Still, one needs to add the fact that B and C are on the same side of line AD.²³ Saccheri’s investigation of such quadrilaterals was influenced by Clavius’ work about Postulate 11 [36]. He considered three cases for these quadrilaterals, when the remaining angles are either acute, right or obtuse, known as Saccheri’s three hypotheses. He was meaning to prove Euclid’s parallel postulate by eliminating the hypotheses of the acute and obtuse angle. As we will see in the next section, in Archimedean neutral geometry, one can eliminate the hypothesis of the obtuse angle. Nonetheless, one cannot eliminate the hypothesis of the acute angle, which corresponds to hyperbolic geometry. Postulate 27 expresses that the hypothesis of the right angle holds and Postulate 28 expresses that there exists a right Saccheri quadrilateral.

Fig. 45

Definition of Lambert

The last postulates that we analyze in this section are closely related to Saccheri quadrilaterals. Indeed, they regard quadrilaterals that were also studied by Saccheri, though they are named after Lambert [34]. has right angles at A, B and D (Fig. 45). The reason why Saccheri studied them is because by taking N such that and M such that in a Saccheri quadrilateral , one obtains two Lambert quadrilaterals and . Lambert proceeded in the same way as Saccheri in his attempt at proving Euclid’s parallel postulate, namely, disproving the obtuse case and trying to derive a contradiction from the acute case [33]. Postulate 29 and Postulate 30 state, respectively, that all Lambert quadrilaterals are rectangles and that there exists a rectangle. One could think that this postulate is close to Postulate 4 (Bachmann’s Lotschnittaxiom), but Postulate 4 asserts the existence of an intersection point, while Postulate 29 states the perpendicularity of two lines known to intersect.

6.2 Formalizing the Equivalence Proof

In this subsection, we address the formalization of the proof that the postulates of the previous subsection (Postulates 21–30) are indeed $\mathcal {N}_{LJ}$-equivalent to Postulate 3 (the triangle postulate), as well as the $\mathcal {N}_{LJ}^{\mathcal {G}}$-equivalence between Postulate 3 and Postulate 2 (Playfair’s Postulate). Exactly like in the previous proofs of equivalence, these equivalences are proved in the context of the Tarski_2D type class from Table 2. The Coq statement corresponding to the $\mathcal {N}_{LJ}$-equivalence of any two of Postulates 3, 21–30 is the following.

One can remark, from the graphical summary of the implications we proved (Fig. 46), that Postulate 27 (the postulate of right Saccheri quadrilaterals) plays a very central role. There is a simple explanation for it: most of these proofs correspond to the formalization of the proofs of some of Saccheri’s propositions given in [44]. In this book, Martin establishes equivalences between each of Saccheri’s three hypotheses and whether certain angles are acute, right or obtuse. Most of these implications follow easily from these propositions. In order to formalize Martin’s proofs, we often proceeded by disjunction of cases on Saccheri’s three hypotheses. One should point out that, because case distinctions cannot be performed in existence proofs in Beeson’s modification of Tarski’s axioms [10], some of the proofs we mechanized would not be valid in his axiomatic system.

Fig. 46

Overview of the proofs of Sect. 6

We can now consider the visual representation of all the implications that we formalized to prove Theorem 3 (Fig. 47). Comparing with Figs. 39 and 46, one can see two extra implications displayed, namely from Postulate 3 to Postulate 12 (the alternative Playfair’s postulate) and from Postulate 7 (the alternate interior angles postulate) to Postulate 3. Indeed, these implications are not necessary to prove that any two postulates that belong to the same circle are equivalent. Nonetheless, in order to prove the following theorem, they are necessary.

Theorem 3

Postulates 3, 21–30 are $\mathcal {N}_{LJ}$-equivalent and Postulates 1–3, 5–30 are $\mathcal {N}_{LJ}^{\mathcal {G}}$-equivalent.

For the sake of completeness, we list the propositions given in [44] that correspond to the implications on Fig. 46. Theorems 22.3 and 22.10 allow us to prove that Postulate 27 implies Postulate 29 and is implied by Postulate 30. The implications from Postulate 28 to Postulate 27 and from Postulate 27 to Postulate 3 are respectively proved in Theorem 22.10 and Corollary 22.13. From Theorem 22.17 we could deduce that Postulate 27 implies Postulate 24 and is implied by Postulate 26. The fact that Postulate 24 implies Postulate 25 and that Postulate 21 implies Postulate 27 are showed in Theorem 23.7. The implications from Postulate 3 to Postulate 21, from Postulate 27 to Postulate 28, from Postulate 29 to Postulate 30 and from Postulate 25 to Postulate 26 are trivial. Indeed, in each of these implications, one needs to prove that a postulate implies another where some of the universal quantifiers are replaced by existential ones. Thus one only needs to assert the existence of a non-degenerate triangle, a Saccheri quadrilateral, a Lambert quadrilateral and a non-degenerate right triangle. The proof that Postulate 27 is equivalent to Postulate 22 is done in Theorem 23.6 for one side of the equivalence (but using the notion of default for a triangle, which we avoided in this section) and in Theorem 23.7 for the other side. Finally, the proof that Postulate 27 is equivalent to Postulate 23 is left as exercise.

Fig. 47

Overview of the proofs of Sects. 4–6

Lastly, we will detail one proof and compare another one to the pen-and-paper proof from which it is inspired.²⁴ Both of these proofs illustrate one of the main difference between a theoretical proof and the actual Coq proof, namely dealing with non-degeneracy conditions and betweenness properties. This difference represents one of the main difficulties that one encounters while formalizing a proof in synthetic geometry. These proofs allow us to study the impact of using the tactics developed in [19] as well as their limitations. The proof we have chosen to study is the fact that Postulate 7 (the alternate interior angles postulate) implies Postulate 3 (the triangle postulate). The pen-and-paper proof is short:

Let ABC be a triangle, construct the parallel to AC through B (Fig. 48). Then, the two pairs of alternate interior angles displayed on the figure are congruent, and hence the sum of the three angles is the straight angle.

Now, we will compare this argument with the formal proof as formalized in Coq. In order to present the rigorous proof of Proposition 4, we will collect five lemmas that will be used throughout this proof.

Lemma 9

(8.18) Dropped perpendiculars²⁵ are constructible.

Lemma 10

(9.8) If and then .

Lemma 11

If and then .

Lemma 12

²⁶A given angle can be laid off upon a given side of a given ray.

Lemma 13

(12.21²⁷) If two lines share a common transversal which makes a pair of alternate angles equal to one another, then the two lines are parallel.

Now, we give in natural language the proof at the level of details needed for the formalization.

Proposition 4

Alternate interior angles postulate (Postulate 7) implies the triangle postulate (Postulate 3).

Fig. 48

Postulate 7 implies Postulate 3

Proof

Given a triangle ABC and knowing that ${{\mathrm{\mathcal {S}}}}(\bigtriangleup {A}{B}{C}) {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$, we wish to prove (Fig. 48). We first eliminate the case where B lies on AC, in which holds trivially. We can construct point $B_1$ such that ${B} \, {C} \, {A} {{\mathrm{\mathbin {\widehat{=}}}}}{C} \, {B} \, {B_1}$ and using Lemma 12. From Lemma 13 and $\lnot {{\mathrm{Col}}}\, {A} \, {B} \, {C}$ we have that ${A C}\mathbin {\parallel _s} {B B_1}$. Then Lemma 2 lets us construct point $B_2$ the symmetric of $B_1$ with respect to B. We know that because, by construction, the segment $\overline{B_1 B_2}$ intersects the line AB in B and neither $B_1$ nor $B_2$ belongs to the line AB, since otherwise it would contradict the fact that ${A C}\mathbin {\parallel _s} {B B_1}$. From Lemma 11 we obtain that . Lemma 10 lets us derive from and that . By construction of $B_2$, $\angle B_1BB_2$ is a straight angle, hence it suffices to show that ${B_1} \, {B} \, {B_2} {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$. By Postulate 7, and ${A C}\mathbin {\parallel } {B B_1}$ imply that ${A} \, {B} \, {B_2} {{\mathrm{\mathbin {\widehat{=}}}}}{C} \, {A} \, {B}$. By construction, ${B} \, {C} \, {A} {{\mathrm{\mathbin {\widehat{=}}}}}{C} \, {B} \, {B_1}$, so we are done. $\square$

The Coq proof for Proposition 4 is the following.

Thanks to the tactics developed in [19] the Coq proof is fairly close to the proof we just gave. The first main difference is that we need to deduce two non-degeneracy conditions, namely HNCol1 and HNCol2. The second main difference is not visible here. In fact, the proof that we just gave is different from usual proof that the sum of the interior angles of a triangle is equal to two right angles, such as the one given by Amiot [2].²⁸ In Amiot’s proof, the fact that the angles $\angle CAB$ and $\angle ABB_2$ are alternate interior angles, HTS2 in the Coq proof, is stated without a proof. This lack of justification for the relative position of the points on the figure is a critique that the modern commentators of Euclid’s Elements often make about Euclid’s proofs. However, Avigad et al. [1] claim that these gaps can be filled by some automatic procedure, justifying in some sense the gaps in Euclid’s original proofs. This is where we reach the limits of our tactics: they only handle incidence problems, permutation properties and compute the consequences of the negation of the non-degeneracy conditions, but do not provide this kind of justification. Therefore, it would be very useful to have an implementation of the procedure proposed in [1].

Our proof that Axiom 4 and Postulate 3 imply Postulate 12 is inspired from the one Greenberg gives in [34]. Nevertheless, we needed to make two modifications to his proof. The first one is due to the fact that we used a different definition for a point belonging to an angle, as we explained in Sect. 3.2.3. The other modification that we made is due to the use of a proof assistant: because of it we cannot skip the justification for the relative position of the points on the figure.

7 Postulates Equivalent to Bachmann’s Lotschnittaxiom and the Role of Archimedes’ Axiom

This section is devoted to the role of Archimedes’ axiom: we study the implications of assuming this property. We will first provide a proof of the independence of Archimedes’ axiom from the axioms of Pythagorean planes.²⁹ Then we will introduce three postulates which we will prove $\mathcal {N}_{LJ}$-equivalent to Postulate 4 (Bachmann’s Lotschnittaxiom). In order to prove these postulates $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalent to the other postulates we presented in this paper we will introduce a new postulate, which was implicitly assumed by Legendre in one of his attempts to prove Euclid’s parallel postulate. Thus we will refer to it as Legendre’s parallel postulate. Having defined this postulate, we will formalize the proofs of Legendre’s Theorems. Finally, we will present the formalization of a variant of Szmielew’s theorem, which opens the path towards a mechanized procedure deciding the equivalence to Euclid’s parallel postulate.

7.1 A Proof of the Independence of Archimedes’ Axiom from the Axioms of Pythagorean Planes

In this subsection, we will first establish the $\mathcal {N}_{LJ}$-equivalence between Axiom 1 (Decidability of intersection of lines), Axiom 3 (Aristotle’s axiom) and Axiom 4 (Greenberg’s axiom) under the assumption that Postulate 2 (Playfair’s postulate) holds. From this equivalence, and using a syntactic proof of the independence of Axiom 1, we obtain a proof for the independence of Archimedes’ axiom from the axioms of Pythagorean planes which is not based on counter-models. We do not prove in Coq this independence property, because it relies on a proof based on Herbrand’s theorem, that we have not formalized.

To demonstrate the equivalence between Axiom 1, Axiom 3 and Axiom 4, we will show the implications that are represented on Fig. 49. With a view to simplifying this overview, we use the equivalences proved in the previous sections to replace any postulate $\mathcal {N}_{LJ}$-equivalent to Postulate 1 by Postulate 1 and similarly for Postulate 2. We already showed that Postulate 1 (Tarski’s parallel postulate) is implied by the conjunction of Postulate 2 and Axiom 1 (Proposition 2) and that Postulate 1 implies Axiom 1 (Proposition 3). In [34], Greenberg proves that Axiom 4 follows from Axiom 3, itself following from Postulate 1. Therefore, it remains to show that Postulate 1 can be derived from the conjunction Axiom 4 and Postulate 2.

Fig. 49

Overview of the proof of the equivalence between Axiom 1, Axiom 3 and Axiom 4

To the best of our knowledge, this proof is new and will therefore be detailed.³⁰

Let us first collect two lemmas from planar neutral geometry needed for it.

Lemma 14

(Crossbar)³¹ If and then ${P} {{\mathrm{\mathbin {\widehat{\in }}}}}{A} \, {B} \, {C}$.

Lemma 15

Given two intersecting lines AB and CD and a point P not on line AB, there exists a point Q on line CD such that .

Proposition 5

Assuming Axiom 4, Postulate 7 implies Postulate 13.

Fig. 50

Assuming Axiom 4, Postulate 7 implies Postulate 13

Proof

Given two parallel lines AB and CD, P a point on line AB and Q a point not on line AB, we wish to prove that lines CD and PQ intersect (Fig. 50). We first eliminate the case of ${{\mathrm{Col}}}\, {C} \, {D} \, {P}$, in which P is the point of intersection. Then we drop a perpendicular from P to line CD, meeting line CD at the foot $C_0$, using Lemma 9. Then we can eliminate the case where $C_0$ lies on PQ, in which $C_0$ is at the intersection between lines CD and PQ. From Lemma 15 we know that there exist a point $Q_1$ on line PQ such that , as well as the points $A_1$ and $C_1$ respectively on lines AB and CD such that and . We now have that ${Q_1} {{\mathrm{\mathbin {\widehat{\in }}}}}{C_0} \, {P} \, {A_1}$ thanks to Lemma 14. Yet we know that $\angle C_0 P A_1$ is right by an application of Postulate 7, and thus the angle $\angle A_1 P Q_1$ is acute. Using Axiom 4, we can construct $C_2$ such that and ${P} \, {C_2} \, {C_0} {{\mathrm{\mathbin {\widehat{<}}}}}{A_1} \, {P} \, {Q_1}$. By another application of Postulate 7, we know that ${A_1} \, {P} \, {C_2} {{\mathrm{\mathbin {\widehat{=}}}}}{P} \, {C_2} \, {C_0}$ and thus ${C_2} {{\mathrm{\mathbin {\widehat{\in }}}}}{A_1} \, {P} \, {Q_1}$. Then we can show that and imply ${Q_1} {{\mathrm{\mathbin {\widehat{\in }}}}}{C_0} \, {P} \, {C_2}$ using Lemma 14. By definition it means that there exists a point Y such that and . Therefore point Y is on both lines CD and PQ. $\square$

Let us recall that Postulate 2 and Postulate 7 (the alternate interior angles postulate) are $\mathcal {N}_{LJ}$-equivalent and that Postulate 1 and Postulate 13 (Proclus’ postulate) are also $\mathcal {N}_{LJ}$-equivalent. Proposition 5 lets us prove our claim.

Theorem 4

Axiom 1, Axiom 3 and Axiom 4 are $\mathcal {N}_{LJ}$-equivalent under the assumption that Postulate 2 holds.

This theorem is quite peculiar because it asserts the equivalence between continuity axioms and a decidability property. Theorem 4 proves this equivalence under the strong assumption that Postulate 2 holds.

Finally, since Axiom 1 is independent from the axioms of planar neutral geometry to which Postulate 2 is added, we get that both Axiom 3 and Axiom 4 are also independent from these axioms. From the following proposition,³² we obtain that Archimedes’ axiom is also independent from these axioms.

Proposition 6

Axiom 3 (Aristotle’s axiom) is implied by Axiom 2 (Archimedes’ axiom).

7.2 Postulates Equivalent to Bachmann’s Lotschnittaxiom

Unlike in the previous three sections, we will mostly just present the postulates which are $\mathcal {N}_{LJ}$-equivalent to Bachmann’s Lotschnittaxiom (Postulate 4), together with the necessary definitions. Indeed, the most interesting proof, in terms of formalization, was the proof that these postulates are $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalent with the previously defined postulates. Therefore, we will focus mainly on the proof of $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalence which will be detailed in the next subsection.

As suggested by the names of these postulates, they correspond to statements similar to postulates that we studied in Sect. 5. More precisely, Postulate 31 and Postulate 32 are respectively weaker version of Postulate 16 (the inverse projection postulate) and Postulate 1 (Tarski’s parallel postulate).

Postulate 31 expresses that for any angle, that, together with itself, make a right angle, any perpendicular raised from a point on one side of the angle intersects the other side. Compared to Postulate 16, this postulate only adds the hypothesis that the considered angle together with itself make a right angle.

Postulate 32 states that, for every right angle and every point T in the interior of the angle, there is a point on each side of the angle such that T is between these two points. The differences in comparison with Postulate 1 are of two kinds. The first one is analogous to the difference between Postulate 31 and Postulate 16. Precisely, the statement is restricted to a certain kind of angle, namely the right angles. The second one resembles the difference between Postulate 17 (Euclid 5) and Postulate 18 (the strong parallel postulate). Indeed, Postulate 32 is less precise than Postulate 1 regarding the position of the points in the hypotheses, which results in a weaker conclusion.

Before introducing the last postulate we need to introduce a definition asserting that some points belong to the perpendicular bisector of a segment.

These predicates correspond to Definition 10.3 of [57]. means that $P'$ is the image of P by the reflection with respect to the line AB. It is interesting to see that for ReflectL P’ P A B to be true when A and B are equal, one must have that $P'$ and P are also equal. To define , which expresses that the line PQ is the perpendicular bisector of the segment $\overline{AB}$, we can therefore just exclude the case where A and B are equal and state that B is the image of A by the reflection with respect to the line PQ.

As for the previous postulates, Postulate 33 presents important similarities with another postulate, namely Postulate 15 (Triangle circumscription principle), although the differences are more substantial. It asserts that the perpendicular bisectors of the legs of a right triangle intersect. Postulate 33 is not only the restriction of Postulate 15 to the case of right triangles. Indeed, Postulate 15 states that for any three non-collinear points there exists a point equidistant from them. As our axioms allow to prove that all points are coplanar, being equidistant from two points is equivalent to belonging to the perpendicular bisector of the segment defined by these two points. However we chose to formalize this postulate using the notion of perpendicular bisector to have a definition which is more faithful to its statement in [44].

Figure 51 provides a graphical summary of the implications we mechanized to prove Theorem 5. Most of these proofs correspond to proofs found in the literature. In [44], there is the proof of the implication from Postulate 33 to Postulate 4 (Theorem 23.7) and in [5], the equivalence between Postulate 4, Postulate 31 and Postulate 32 is proved.

Fig. 51

Overview of the proofs of Sect. 7.2

The implications displayed on Fig. 51 allow us to prove the following theorem.

Theorem 5

Postulates 4, 31–33 are $\mathcal {N}_{LJ}$-equivalent.

Following is the Coq statement corresponding to Theorem 5.

7.3 Legendre’s Theorems

This subsection is dedicated to one of Legendre’s flawed proofs of Euclid’s parallel postulate. In this proof he implicitly assumed Legendre’s parallel postulate, which we will introduce. Following [56], we will split this proof into four Legendre’s Theorems. There are two statements commonly known as Legendre’s theorems, but Rothe mentions four such theorems in [56]. What he refers as Legendre’s third theorem and Legendre’s fourth theorem correspond to the remaining parts of this flawed proof. Throughout this subsection, we will refer to this proof which we mechanized, while emphasizing on the formalization details.

Let us first present Legendre’s parallel postulate.

This posulate formulates that there exists an acute angle such that, for every point T in the interior of the angle, there is a point on each side of the angle such that T is between these two points. Postulate 34 is pretty similar to Postulate 1 (Tarski’s parallel postulate). In fact, Postulate 34 mainly differs from Postulate 1 in two aspects. The first difference comes from the way in which the points A, B and C defining the considered angle are quantified (Fig. 13). In this version of the parallel postulate they are existentially quantified.³³ The second difference is about the relative position of the points, which is more precise in Postulate 1. Here, the same situation as in Postulate 32 (Weak Tarski’s parallel postulate) occurs: the point through which goes the line asserted to exist is not required to be further away from B than the segment $\overline{AC}$, which results in a weaker conclusion, namely that the line intersects the sides of the angles without any precision with regards to the position of the intersections relatively to A and C.

Let us then consider Legendre’s first theorem, which can be stated in the following way.

Theorem 6

(Legendre’s first theorem) In Archimedean neutral geometry, the angles of every triangle make less than or equal to two right angles.

Theorem 6 is now known as Saccheri–Legendre theorem, as Saccheri proved this statement almost a century before Legendre. In order to formalize the proof of this theorem as exposed in [44], we introduced a variant of the predicate Grad. Indeed, the theorem that is central for this proof, namely Theorem 22.18, constructs pairs of points that, given two segments, correspond to the endpoints of segments constructed by extending the given segments by their own lengths the same number of times (the $A_i$ and $B_i$ for $1 \le i \le n$ on Fig. 52³⁴). As our formalization of Archimedes’ axiom does not use the concept of natural number, we had to express that the segments are extended the same number of times, using the following inductive predicate. Grad2 A B C D E F intuitively means that there exists n such that ${AC} \mathbin {\equiv } {nAB}$ and ${DF} \mathbin {\equiv } {nDE}$.

Fig. 52

Considered points in Theorem 22.18 of [44]

As often in induction proofs, the difficulty lied in finding the appropriate inductive hypothesis. Moreover, the same difficulties as the ones presented in Sect. 6 arose. Having mechanized Theorem 22.18 of [44], we could demonstrate Theorem 6. The proposition that we showed is the following.

We should remark that the hypotheses of this theorem are not minimal. Indeed, Greenberg provides a proof only relying on Axiom 3 (Aristotle’s axiom) [33] that we also formalized.

The next theorem has already been proven in Sect. 6. It asserts that Postulate 21 (the postulate of existence of a triangle whose angles sum to two rights) implies Postulate 3 (the triangle postulate) and can be stated in the following way.

Theorem 7

(Legendre’s second theorem) In planar neutral geometry, if the angles of one triangle sum to two right angles, then the angles of all triangles sum to two right angles.

Since Theorem 7 is a corollary of Theorem 3, we will just give the Coq statement corresponding to it.

Legendre’s next theorem expresses that, assuming Axiom 2 (Archimedes’ axiom), Postulate 20 (Euclid’s parallel postulate) is a consequence of Postulate 3. It can be formulated in the following manner.

Theorem 8

(Legendre’s third theorem) In Archimedean neutral geometry, if the angles of every triangle sum to two right angles, then Euclid’s parallel postulate holds.

As for Theorem 6, the hypotheses of Theorem 8 can be weakened: from Theorem 4, we know that Axiom 4 (Greenberg’s axiom) suffices to derive the implication from Postulate 3 to Postulate 20. Hence, in order to obtain this theorem, we chose to formalize the proof that Axiom 2 implies Axiom 3 (Aristotle’s axiom) (Proposition 6). Let us recall Greenberg’s definition of Axiom 3.

“Given any acute angle, any side of that angle, and any challenge segment PQ, there exists a point Y on the given side of the angle such that if X is the foot of the perpendicular from Y to the other side of the angle, then $YX> PQ$.”

Fig. 53

Axiom 2 implies Axiom 3

Let $Y_0$ be a point on the given side of the angle and $X_0$ be the foot of the perpendicular from $Y_0$ to the other side of the angle (Fig. 53). Then, by letting $n_0$ be a positive integer such that $n_0 Y_0 X_0 > PQ$ and B be the vertex of the angle, one could assume that Axiom 2 would let us conclude by constructing Y such that $n_0 {Y_0 B} \mathbin {\equiv } {Y B}$ and dropping a perpendicular from Y on the other side of the angle. Nevertheless, following [44], it is much simpler to choose a positive n such $2^n Y_0 X_0 > PQ$ and prove that a point Y such that $n {2^n Y_0 B} \mathbin {\equiv } {Y B}$ would suffice.³⁵ Therefore, we defined the following exponential variant of the predicate Grad.

GradExp A B C intuitively asserts that there exists n such that $2^n {A B} \mathbin {\equiv } {A C}$. Yet the positive integer n is not explicit in our definition, it is hidden in the number of times the constructor gradexp_stab is used. We then proved the equivalence between being reachable using Grad or GradExp to complete the proof of Theorem 8. We now provide its Coq statement.

Finally, the last theorem will complete Legendre’s flawed proof. It states that, assuming Axiom 2, Postulate 21 (the postulate of existence of a triangle whose angles sum to two rights) is a consequence of Postulate 34 (Legendre’s parallel postulate). It can be phrased as follows.

Theorem 9

(Legendre’s fourth theorem) In Archimedean neutral geometry, if Legendre’s postulate holds, then there exists a triangle for which the angles sum to two right angles.

To demonstrate Theorem 9, we mechanized the proof given in [44]. In this proof, a concept that we have not encountered so far plays a major role: the defect of a triangle. For a given triangle, its defect together with the sum of the angles of this triangle make two right angles. Having the concept of sum of angles, it is straightforward to define this concept in Coq.

Here, ${{\mathrm{\mathcal {D}}}}(\bigtriangleup {A}{B}{C}) {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$ expresses that $\angle DEF$ is the defect of the triangle ABC. This proof eliminates the hypothesis of acute angle by reproducing a construction. Given the acute angle $\angle ABC$ asserted to exist by Postulate 34 and a pair of point $A_k$ and $C_k$ respectively on the sides BA and BC, this construction creates the points $A_{k+1}$ and $C_{k+1}$, respectively on the sides BA and BC, such that the defect of the triangle $A_{k+1} B C_{k+1}$ is at least the double of the defect of the triangle $A_k B C_k$. To conclude its proof, Legendre uses Archimedes’ axiom to deduce that repeating this construction will lead to a triangle $A_n B C_n$ which has a defect greater than two right angles. This last step need to be detailed in Coq, as it makes the implicit assumption that Axiom 2 implies the Archimedean property for angles. More precisely, the implicit assumption is that every non-degenerate angle can be doubled enough times to obtain an obtuse angle. Therefore, we defined the following variant of the predicate Grad.

Hartshorne (Lemma 35.1 in [36]) provides an explicit proof that we formalized. We could then prove Theorem 9. Again, the difficulty lied in finding the appropriate induction hypotheses and justifying the position of the points on the figure. By mechanizing the proof that Postulate 34 can be derived from Postulate 4, which is part of Theorem 23.7 of [44], we obtain the following theorem (Fig. 54 provides a summary of the implications needed for its proof).

Fig. 54

Overview of the proofs

Theorem 10

In Archimedean neutral geometry, Postulates 1–34 are equivalent.

7.4 Towards a Mechanized Procedure Deciding the Equivalence to Euclid’s Parallel Postulate

Another interesting consequence of continuity is a very useful result concerning the parallel postulate, that was established by Szmielew in [58]. It states that “Euclid’s axiom can be replaced in the axiom system of $\mathcal {E}_n$ by any sentence whatsoever which is valid in $\mathcal {E}_n$ but not in $\mathcal {H}_n$”. Here $\mathcal {E}_n$ denotes Tarski’s system of geometry, where A8 and A9 are replaced by the lower n-dimensional axiom and the upper n-dimensional axiom, and $\mathcal {H}_n$ corresponds to $\mathcal {E}_n$ where Postulate 1 (Tarski’s parallel postulate) A10 is replaced by its negation. Hence this result allows us to prove the equivalence of some statements with Tarski’s parallel postulate by checking if it holds in Euclidean geometry and does not in hyperbolic geometry. Moreover, because both of these theories are decidable, this gives a procedure deciding if a statement is equivalent to the parallel postulate. In this subsection, we will formalize a result similar to this and we will then discuss the possibility for the mechanization of such a procedure.

In Sect. 7.3, we formalized the fact that Postulate 1 is equivalent to Postulate 2 when assuming Archimedes’ axiom. With a view to proving this result, we chose to use Postulate 2 in place of Postulate 1. We would like to stress that, while Szmielew obtained her result through metamathematical properties, we present here a synthetic proof, so the choice of the parallel postulate matters. This choice was motivated by the fact that the negation of Postulate 2 was easier to work with. However, her proof is valid in spaces of dimension higher than two, whereas our proof is only valid in planar geometry. Another difference is that her proof assumes the first-order version of the axiom of continuity, while our proof assumes Aristotle’s axiom (Axiom 3). We defined the negation of Postulate 2 in the following way.

We can point out that this definition (we will now refer to it as hyperbolic plane postulate) is in fact the negation of a modification of Postulate 2. This modification expresses the existence of a line and a point not on this line such that there is a unique line parallel to this line passing by this point. This modification was showed to be equivalent with Postulate 2 when assuming Axiom 4 for one of the implications. Because of this, we could not classify this modified version of Postulate 2. This explains why we did not present it in Sect. 4. We now collect four lemmas which will be used in the lemma at the core of this proof.

Lemma 16

Given a right triangle ABD with the right angle at vertex A, a point C is constructible such that ABCD is a Saccheri quadrilateral.

Lemma 17

In a Saccheri quadrilateral ABCD, the sides AD and BC are parallel.

Lemma 18

In a Saccheri quadrilateral ABCD, the sides AB and CD are strictly parallel.

Lemma 19

(12.6) Two points on a line strictly parallel to another one are on the same side of this last line.

Proposition 7

The hyperbolic plane postulate holds under the hypothesis of the acute angle.

Fig. 55

The hyperbolic plane postulate holds under the hypothesis of the acute angle

Proof

Given three non-collinear points $A_1$, $A_2$ and P we wish to prove that there exists two distinct lines $B_1 B_2$ and $C_1 C_2$ both parallel to line $A_1 A_2$ and passing through P (Fig. 55). Lemma 9 lets us drop the perpendicular from P to line $A_1 A_2$ in Q. A tedious distinction of cases would then allow us to prove that there exists a point X on line $A_1 A_2$ distinct from $A_1$, $A_2$ and Q. Lemma 2 lets us construct Y, the symmetric point of X with respect to Q. Using Lemma 16, we construct $B_1$ and $C_1$ such that and . We will now prove that both lines $B_1 P$ and $C_1 P$ are both parallel to line $A_1 A_2$ and pass by P, and that they are distinct. The facts that these lines are parallel to line $A_1 A_2$ and pass by P are respectively due to Lemma 17 and trivial. We proceed by proof of negation to prove that these lines are distinct. So let us assume that they are equal. We can prove that : indeed, we have by definition, as well as and from Lemma 19, hence Lemma 10 applied twice lets us show our claim. We shall now derive a contradiction by proving that ${B_1} \, {P} \, {C_1} {{\mathrm{\mathbin {\widehat{<}}}}}{B_1} \, {P} \, {C_1}$. Since angles $\angle XQP$ and $\angle PQY$ do not make an over-obtuse angle, making exactly two right angles, it suffices to show that ${B_1} \, {P} \, {Q} {{\mathrm{\mathbin {\widehat{<}}}}}{P} \, {Q} \, {X}$, ${Q} \, {P} \, {C_1} {{\mathrm{\mathbin {\widehat{<}}}}}{P} \, {Q} \, {X}$, ${B_1} \, {P} \, {Q} {{\mathrm{\mathbin {\widehat{+}}}}}{Q} \, {P} \, {C_1} {{\mathrm{\mathbin {\widehat{=}}}}}{B_1} \, {P} \, {C_1}$ and ${P} \, {Q} \, {X} {{\mathrm{\mathbin {\widehat{+}}}}}{P} \, {Q} \, {X} {{\mathrm{\mathbin {\widehat{=}}}}}{B_1} \, {P} \, {C_1}$. We have ${B_1} \, {P} \, {Q} {{\mathrm{\mathbin {\widehat{<}}}}}{P} \, {Q} \, {X}$ and ${Q} \, {P} \, {C_1} {{\mathrm{\mathbin {\widehat{<}}}}}{P} \, {Q} \, {X}$ from the hypothesis of the acute angle and ${B_1} \, {P} \, {Q} {{\mathrm{\mathbin {\widehat{+}}}}}{Q} \, {P} \, {C_1} {{\mathrm{\mathbin {\widehat{=}}}}}{B_1} \, {P} \, {C_1}$ by definition. Thus we will be done if we can show that ${P} \, {Q} \, {X} {{\mathrm{\mathbin {\widehat{+}}}}}{P} \, {Q} \, {X} {{\mathrm{\mathbin {\widehat{=}}}}}{B_1} \, {P} \, {C_1}$. We trivially have ${X} \, {Q} \, {P} {{\mathrm{\mathbin {\widehat{=}}}}}{P} \, {Q} \, {X}$ and ${P} \, {Q} \, {Y} {{\mathrm{\mathbin {\widehat{=}}}}}{P} \, {Q} \, {X}$. By definition we have ${X} \, {Q} \, {P} {{\mathrm{\mathbin {\widehat{+}}}}}{P} \, {Q} \, {Y} {{\mathrm{\mathbin {\widehat{=}}}}}{X} \, {Q} \, {Y}$. So it suffices to prove ${X} \, {Q} \, {Y} {{\mathrm{\mathbin {\widehat{=}}}}}{B_1} \, {P} \, {C_1}$, which holds since straight angles are congruent. $\square$

Let us state our variant of Szmielew’s theorem. We will not detail its proof as it is a tautology knowing the Legendre’s first theorem, the previous lemma and the $\mathcal {N}_{LJ}^{\mathcal {G}}$-equivalence between Playfair’s postulate and the hypothesis of right angle. Following are the informal statement as well as its formulation in Coq. Note that it is the only theorem we state in this paper that is expressed using second-order logic. In general, second-order logic is rarely used in our formalization of geometry: it is used only in intermediate definitions and statements needed for the proof of Pappus’ theorem [17].

Theorem 11

Assuming Aristotle’s axiom, any proposition implied by Playfair’s postulate and such that its negation is implied by the hyperbolic plane postulate is equivalent to Playfair’s postulate.

Even if Theorem 11 only allows us to prove $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalence, it is a very powerful tool. Indeed, for any statement presenting only universal quantifiers, it suffices to show it is a consequence of any of our 34 versions of the parallel postulate and to provide a counterexample in hyperbolic geometry to prove its $\mathcal {N}_{LJ}^{\mathcal {A}}$-equivalence with Playfair’s postulate. Moreover, both $\mathcal {E}_n$ and $\mathcal {H}_n$ are decidable [58]. Therefore Theorem 11 renders possible a mechanized procedure deciding if a statement is equivalent to Playfair’s postulate, using the decidability of both theories. Actually, the quantifier elimination algorithm for real closed fields which has been formalized by Cohen and Mahboubi [23] can be connected to Tarski’s system of geometry, thanks to our formalization of the arithmetization of Euclidean geometry [8]. Following [59] we could formalize the arithmetization of hyperbolic geometry and extend the same quantifier elimination algorithm to this system. However, we are not sure whether this method would work in practice, because the quantifier elimination algorithm for real closed field by Cohen and Mahboubi has not been designed to be efficient, but to provide a theoretical result. Furthermore, the Gröbner basis method has already been integrated into Coq by Grégoire et al. [31]. Our work on the arithmetization of Euclidean geometry lets us use this method in our axiomatic system. Thus proving that a statement presenting only universal quantifiers is a consequence of Playfair’s postulate could, in some cases, be done by computation, although this would require a significant formalization work.

8 Conclusion

We have described the formalization within the Coq proof assistant of the proof that 34 versions of the parallel postulate are equivalent. The originality of our proofs relies on the fact that first, the equivalence between these different versions are proved in Tarski’s neutral geometry without using the continuity axiom nor line-circle continuity, and second, we work in an intuitionistic logic. Assuming decidability of point equality, we clarified the role of the decidability of intersection: we obtained the formal proof that assuming decidability of point equality, some versions of the parallel postulate imply decidability of the intersection of lines. The formal proofs of equivalences consist of about 7k lines of code and rely on 44k lines of code corresponding to a library for planar neutral geometry. The proofs make heavy use of the tactics developed previously [19]. The use of a proof assistant was crucial to check these proofs. Indeed, it is extremely easy to make a mistake in a pen-and-paper proof in this context. We have to be careful not to use any of the many statements which are equivalent to the parallel postulate, as well as not use classical reasoning.

This work can have several extensions. First, we can take advantage of our large library in neutral geometry, and of the proof of the equivalence between the different versions of the postulate, to obtain a library in hyperbolic geometry.

Second, we could weaken our axiom systems, to study the more constructive version as defined by Beeson [11] where he assumes stability of equality, congruence and betweenness instead of excluded-middle for equality as we do, or to use even more constructive assumptions as in [12].

Third, it could be extended to some other versions of the parallel postulates, as the one recently proposed by Pambuccian [51].

Finally, it would be also interesting to complete this study by the formalization of the different independence properties that we mentioned.

8.1 Availability

The full Coq development is available here: http://geocoq.github.io/GeoCoq/.

Appendices

Summary of the 34 Postulates

• 1. (Tarski’s parallel postulate) Given a point D between the points B and C and a point T further away from A than D on the half line AD, one can build a line which goes through T and intersects the sides BA and BC of the angle $\angle ABC$ respectively further away from B than A and C.

• 2. (Playfair’s postulate) There is a unique parallel to a given line going through some point.

• 3. (Triangle postulate) The sum of the angles of any triangle is two right angles.

• 4. (Bachmann’s Lotschnittaxiom) Given the lines l, m, r and s, if l and r are perpendicular, r and s are perpendicular and s and m are perpendicular, then l and m must meet.

• 5. (Postulate of transitivity of parallelism) If two lines are parallel to the same line then these lines are also parallel.

• 6. (Midpoint converse postulate) The parallel line to one side of a triangle going through the midpoint of another side cut the third side in its midpoint.

• 7. (Alternate interior angles postulate) The line falling on parallel lines makes the alternate angles equal one to one another.

• 8. (Consecutive interior angles postulate) A line falling on parallel lines makes the sum of interior angles on the same side equal to two right angles.

• 9. (Perpendicular transversal postulate) Given two parallel lines, any line perpendicular to the first line is perpendicular to the second line.

• 10. (Postulate of parallelism of perpendicular transversals) Two lines, each perpendicular to one of a pair of parallel lines, are parallel.

• 11. (Universal Posidonius’ postulate) If two lines are parallel then they are everywhere equidistant.

• 12. (Alternative Playfair’s postulate) Any line parallel to line l passing through a point P is equal to the line that passes through P and shares a common perpendicular with l going through P.

• 13. (Proclus’ postulate) If a line intersects one of two parallel lines then it intersects the other.

• 14. (Alternative Proclus’ postulate) If a line intersects in P one of two parallel lines which share a common perpendicular going through P, then it intersects the other.

• 15. (Triangle circumscription principle) For any three non-collinear points there exists a point equidistant from them.

• 16. (Inverse projection postulate) For any given acute angle, any point together with its orthogonal projection on one side of the angle form a line which intersects the other side.

• 17. (Euclid 5) Given a non-degenerated parallelogram PRQS and a point U strictly inside the angle $\angle QPR$, there exists a point I such that Q and U are respectively strictly between S and I and strictly between P and I.

• 18. (Strong parallel postulate) Given a non-degenerated parallelogram PRQS and a point U not on line PR, the lines PU and QS intersect.

• 19. (Alternative strong parallel postulate) If a straight line falling on two straight lines make the sum of the interior angles on the same side different from two right angles, the two straight lines meet if produced indefinitely.

• 20. (Euclid’s parallel postulate) If a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if produced indefinitely, meet on that side on which are the angles less than the two right angles.

• 21. (Postulate of existence of a triangle whose angles sum to two rights) There exists a triangle whose angles sum to two rights.

• 22. (Posidonius’ postulate) There exists two lines which are everywhere equidistant.

• 23. (Postulate of existence of similar but non-congruent triangles) There exists two similar but non-congruent triangles.

• 24. (Thales’ postulate) If the circumcenter of a triangle is the midpoint of a side of a triangle, then the triangle is right.

• 25. (Thales’ converse postulate) In a right triangle, the midpoint of the hypotenuse is the circumcenter.

• 26. (Existential Thales’ postulate) There is a right triangle whose circumcenter is the midpoint of the hypotenuse.

• 27. (Postulate of right Saccheri quadrilaterals) The angles of any Saccheri quadrilateral are right.

• 28. (Postulate of existence of a right Saccheri quadrilateral) There is a Saccheri quadrilateral whose angles are right.

• 29. (Postulate of right Lambert quadrilaterals) The angles of any Lambert quadrilateral are right i.e. if in a quadrilateral three angles are right, so is the fourth.

• 30. (Postulate of existence of a right Lambert quadrilateral) There exists a Lambert quadrilateral whose angles are all right.

• 31. (Weak inverse projection postulate) For any angle, that, together with itself, make a right angle, any point together with its orthogonal projection on one side of the angle form a line which intersects the other side.

• 32. (Weak Tarski’s parallel postulate) For every right angle and every point T in the interior of the angle, there is a point on each side of the angle such that T is between these two points.

• 33. (Weak triangle circumscription principle) The perpendicular bisectors of the legs of a right triangle intersect.

• 34. (Legendre’s parallel postulate) There exists an acute angle such that, for every point T in the interior of the angle, there is a point on each side of the angle such that T is between these two points.

Definitions of the Geometric Predicates

Coq	Notation	Explanation
Bet A B C		B is between A and C
Cong A B C D	${AB} \mathbin {\equiv } {CD}$	The segments $\overline{AB}$ and $\overline{CD}$ are congruent
Col A B C	${{\mathrm{Col}}}\, {A} \, {B} \, {C}$	A, B and C are collinear
Coplanar A B C D	${{\mathrm{Cp}}}\, {A} \,{ B} \, {C} \, {D}$	A, B, C and D are coplanar
Par_strict A B C D	${A B}\mathbin {\parallel _s} {C D}$	The lines AB and CD are strictly parallel
Par A B C D	${A B}\mathbin {\parallel } {X Y}$	The lines AB and CD are parallel
CongA A B C D E F	${A} \, {B} \, {C} {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$	The angles $\angle ABC$ and $\angle DEF$ are congruent
TS A B P Q		P and Q are on opposite sides of line AB
OS A B P Q		P and Q are on the same side of line AB
SumA A B C D E F G H I	${A} \, {B} \, {C} {{\mathrm{\mathbin {\widehat{+}}}}}{D} \, {E} \, {F} {{\mathrm{\mathbin {\widehat{=}}}}}{G} \, {H} \, {I}$	The angles $\angle ABC$ and $\angle DEF$ sum to $\angle GHI$
TriSumA A B C D E F	${{\mathrm{\mathcal {S}}}}(\bigtriangleup {A}{B}{C}) {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$	The angle of the triangle ABC sum to $\angle DEF$
Le A B C D	$AB \le CD$	The segment $\overline{AB}$ is smaller or congruent to the segment $\overline{CD}$
Lt A B C D	$AB < CD$	The segment $\overline{AB}$ is smaller than the segment $\overline{CD}$
Midpoint M A B		M is the midpoint of the segment $\overline{AB}$
Per A B C		The triangle ABC is a right triangle with the right angle at vertex B
Out P A B		B belongs to the ray PA
InAngle P A B C	${P} {{\mathrm{\mathbin {\widehat{\in }}}}}{A} \, {B} \, {C}$	P belongs to the angle $\angle ABC$
LeA A B C D E F	${A} \, {B} \, {C} {{\mathrm{\mathbin {\widehat{\le }}}}}{D} \, {E} \, {F}$	The angle $\angle ABC$ is smaller or congruent to the angle $\angle DEF$

Coq	Notation	Explanation
LtA A B C D E F	${A} \, {B} \, {C} {{\mathrm{\mathbin {\widehat{<}}}}}{D} \, {E} \, {F}$	The angle $\angle ABC$ is smaller than the angle $\angle DEF$
Acute A B C		The angle $\angle ABC$ is acute
Perp_at X A B C D	${A B} \mathbin {\underset{X}{\perp }} {C D}$	The lines AB and CD meet at a right angle in X
Perp A B C D	${A B} \mathbin {\perp } {C D}$	The lines AB and CD are perpendicular
Perp2 A B C D P		The lines AB and CD have a common perpendicular which passes through P
BetS A B C		B is strictly between A and C
SAMS A B C D E F		The angles $\angle ABC$ and $\angle DEF$ do not make an over-obtuse angle
Saccheri A B C D		The quadrilateral ABCD is a Saccheri quadrilateral
Lambert A B C D		The quadrilateral ABCD is a Lambert quadrilateral
ReflectL P’ P A B		$P'$ is the image of P by the reflection with respect to the line AB
Perp_bisect P Q A B		The line PQ is the perpendicular bisector of the segment $\overline{AB}$
Defect A B C D E F	${{\mathrm{\mathcal {D}}}}(\bigtriangleup {A}{B}{C}) {{\mathrm{\mathbin {\widehat{=}}}}}{D} \, {E} \, {F}$	The angle $\angle DEF$ is the defect of the triangle ABC