# zbMATH — the first resource for mathematics

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. (English) Zbl 1441.03011
This is an important paper, which extends results obtained by M. Beeson [Bull. Symb. Log. 22, No. 1, 1–104 (2016; Zbl 1403.03130)], by showing which forms of Euclidean-like parallel postulates are equivalent within intuitionistic logic, with absolute geometry with decidable point equality as the background theory. While inside classical logic we know (see the reviewer and C. Schacht [Beitr. Algebra Geom. 60, No. 4, 733–748 (2019; Zbl 1429.51004)]) that, with Hilbert’s (or Tarski’s) absolute geometry as background, (*) $${\mathbf P}\rightarrow {\mathbf R}\rightarrow {\mathbf L}\rightarrow {\mathbf L}(\exists)$$, where $$\mathbf{P}$$ stands for the Eucidean parallel postulate, $$\mathbf{R}$$ stands for Clairaut’s axiom (“There is a rectangle”), $$\mathbf{L}$$ stands for Bachmann’s Lotschnittaxiom (“The perpendiculars raised to the legs of a right triangle intersect”), and $$\mathbf{L}(\exists)$$ for “There exists an angle, such that, through any point in its interior, there is a line intersecting both legs of the angle”. None of the arrows in (*) is reversible. The authors consider many more versions – 34 altogether – of axioms resembling the Euclidean parallel postulate, all of which are equivalent with the Euclidean parallel postulate in the presence of the Archimedean axiom, but not in its absence. In the intuitionistic setting, there is an additional axiom in the chain (*), namely between $${\mathbf P}$$ and $${\mathbf R}$$, where $$\mathbf{P}$$ stands for either Euclid’s version of the parallel postulate or for Tarski’s version thereof (“Through any point in the interior of an angle there is a line intersecting both legs”), there is $${\mathbf H}$$, Hilbert’s version of the parallel postulate, which states that through a point $$P$$ to a line $$g$$ not incident with $$P$$ there do not pass two parallels to $$g$$. The chain (*) thus becomes (each arrow cannot be reversed): ${\mathbf P}\rightarrow {\mathbf H}\rightarrow \mathbf{R}\rightarrow {\mathbf L}\rightarrow {\mathbf L}(\exists)$
Each of the 34 axioms turns out to be intuitionistically equivalent to one of the above five. The deductions are mechanically checked by Coq, a proof assistant,
The authors refer to $${\mathbf L}(\exists)$$ as “Legendre’s axiom,” but the reviewer is not aware of any place in Legendre’s Éléments de géométrie where such an axiom is stated. Legendre asks that any angle of measure $$\leq 60^{\circ}$$ should have the property that, through any point in its interior, there be a line intersecting both legs of the angle. It thus appears that this is the first instance in print where this axiom appears. The authors of the paper [Beitr. Algebra Geom. 60, No. 4, 733–748 (2019; Zbl 1429.51004)] were unaware of this precedent, and were under the impression of having been the first to stumble upon $${\mathbf L}(\exists)$$.

##### MSC:
 03B30 Foundations of classical theories (including reverse mathematics) 03B35 Mechanization of proofs and logical operations 51F05 Absolute planes in metric geometry 51M05 Euclidean geometries (general) and generalizations 03F55 Intuitionistic mathematics 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Coq; GeoCoq
Full Text:
##### References:
  Avigad, J.; Dean, E.; Mumma, J., A formal system for Euclid’s elements, Rev. Symb. Log., 2, 700-768, (2009) · Zbl 1188.03008  Amiot, A.: Eléments de géométrie [texte imprimé]: rédigés d’après le nouveau programme de l’enseignement scientifique des lycées; suivis d’un complément à l’usage des élèves de mathématiques spéciales (1870)  Amira, D., Sur l’axiome de droites parallèles, L’Enseign. Math., 32, 52-57, (1933) · Zbl 0008.26904  Alama, J.; Pambuccian, V., From absolute to affine geometry in terms of point-reflections, midpoints, and collinearity, Note di Mat., 36, 11-24, (2016) · Zbl 1414.51002  Bachmann, F.: Zur Parallelenfrage. In: Cortés, V., Richter, B. (eds.) Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, vol. 27, pp. 173-192. Springer, Berlin (1964) · Zbl 0123.38002  Bachmann, F.: Aufbau der Geometrie aus dem Spiegelungsbegriff. Grundlehren der mathematischen Wissenschaften. Springer, Berlin (1973) · Zbl 0254.50001  Beeson, M.; Boutry, P.; Narboux, J., Herbrand’s theorem and non-Euclidean geometry, Bull. Symb. Log., 21, 111-122, (2015) · Zbl 1375.03079  Boutry, P., Braun, G., Narboux, J.: From Tarski to Descartes: formalization of the arithmetization of Euclidean geometry. In: The 7th International Symposium on Symbolic Computation in Software (SCSS 2016), EasyChair Proceedings in Computing, Tokyo, Japan, pp. 15 (March 2016) · Zbl 1394.68349  Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, Strasbourg, France, p. 19 (2016) · Zbl 1397.03019  Beeson, M., A constructive version of Tarski’s geometry, Ann. Pure Appl. Log., 166, 1199-1273, (2015) · Zbl 1392.03059  Beeson, M., Constructive geometry and the parallel postulate, Bull. Symb. Log., 22, 1-104, (2016) · Zbl 1403.03130  Beeson, M.: Brouwer and Euclid. Indagationes Mathematicae. To appear in a special issue devoted to Brouwer (2017)  Bell, JL, Hilbert’s $$\epsilon$$-operator in intuitionistic type theories, Math. Log. Q., 39, 323-337, (1993) · Zbl 0802.03005  Birkhoff, GD, A set of postulates for plane geometry (based on scale and protractors), Ann. Math., 33, 329-345, (1932) · Zbl 0004.12602  Braun, D., Magaud, N.: Des preuves formelles en Coq du théorème de Thalès pour les cercles. In: Baelde, D., Alglave, J. (eds.) Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Le Val d’Ajol, France (2015)  Braun, G.; Narboux, J.; Ida, T. (ed.); Fleuriot, J. (ed.), From Tarski to Hilbert, No. 7993, 89-109, (2012), Edinburgh  Braun, G.; Narboux, J., A synthetic proof of Pappus’ theorem in Tarski’s geometry, J. Autom. Reason., 58, 23, (2017) · Zbl 1405.03034  Boutry, P., Narboux, J., Schreck, P., Braun, G.: A short note about case distinctions in Tarski’s geometry. In: Botana, F., Quaresma, P. (eds.) Proceedings of the 10th International Workshop on Automated Deduction in Geometry, Volume TR 2014/01 of Proceedings of ADG 2014, pp. 51-65. University of Coimbra, Coimbra (2014)  Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility and readability of formal proofs in geometry. In: Botana, F., Quaresma, P. (eds.) Proceedings of the 10th International Workshop on Automated Deduction in Geometry, Volume TR 2014/01 of Proceedings of ADG 2014, pp. 31-49. University of Coimbra, Coimbra (2014)  Bonola, R.: Non-Euclidean Geometry: A Critical and Historical Study of Its Development. Courier Corporation, North Chelmsford (1955) · JFM 43.0557.02  Borsuk, K., Szmielew, W.: Foundations of Geometry. North-Holland, Amsterdam (1960) · Zbl 0093.33301  Cajori, F.: A History of Elementary Mathematics. Macmillan, London (1898) · JFM 46.1421.01  Cohen, C.; Mahboubi, A., Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Log. Methods Comput. Sci., 8, 1-40, (2012) · Zbl 1241.68096  Coxeter, H.S.M.: Non-Euclidean Geometry. Cambridge University Press, Cambridge (1998) · Zbl 0909.51003  Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Richter-Gebe, J., Wang, D. (eds.) Automated Deduction in Geometry, Lectures Notes in Computer Science, vol. 2061, pp. 306-324 (2001) · Zbl 0985.68078  Dehn, M., Die Legendre’schen Sätze über die Winkelsumme im Dreieck, Math. Ann., 53, 404-439, (1900) · JFM 31.0471.01  Duprat, J.: Fondements de géométrie euclidienne. https://hal.inria.fr/hal-00661537 (2010)  Euclid, Heath, T.L., Densmore, D.: Euclid’s Elements: All Thirteen Books Complete in One Volume: The Thomas L. Heath Translation. Green Lion Press, Santa Fe (2002) · Zbl 1026.01024  Friedrich, C., Bolyai, F.: Briefwechsel zwischen Carl Friedrich Gauss und Wolfgang Bolyai. BG Teubner, Leipzig (1899)  Gries, C., Boutry, P., Narboux, J.: Somme des angles d’un triangle et unicité de la parallèle: une preuve d’équivalence formalisée en Coq. In: Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016)  Grégoire, B, Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) Post-proceedings of Automated Deduction in Geometry (ADG 2008). Number 6701 in Lecture Notes in Artificial Intelligence (2011)  Greenberg, MJ, Aristotle’s axiom in the foundations of geometry, J. Geom., 33, 53-57, (1988) · Zbl 0655.51010  Greenberg, M.J.: Euclidean and Non-Euclidean Geometries—Development and History. Macmillan, London (1993) · Zbl 0418.51001  Greenberg, MJ, Old and new results in the foundations of elementary plane Euclidean and non-Euclidean geometries, Am. Math. Mon., 117, 198-219, (2010) · Zbl 1206.51015  Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)  Hartshorne, R.: Geometry: Euclid and Beyond, Undergraduate Texts in Mathematics. Springer, Berlin (2000) · Zbl 0954.51001  Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois, 1960. Second English edition, translated from the tenth German edition by Leo Unger. Original publication date (1899)  Kline, M.: Mathematical Thought from Ancient to Modern Times, vol. 3. Oxford University Press, Oxford (1990) · Zbl 0784.01048  Klugel, G.S.: Conatuum praecipuorum theoriam parallelarum demonstrandi recensio. PhD thesis, Schultz, Göttingen (1763). German translation available http://www2.math.uni-wuppertal.de/ volkert/versuch.html  Legendre, A.M.: Réflexions sur différentes manières de démontrer la théorie des parallèles ou le théorème sur la somme des trois angles du triangle. Mémoires de l’Académie royale des sciences de l’Institut de France, XII: pp. 367-410 (1833)  Lewis, FP, History of the parallel postulate, Am. Math. Mon., 27, 16-23, (1920)  Laubenbacher, R., Pengelley, D.: Mathematical Expeditions: Chronicles by the Explorers. Springer, Berlin (2013) · Zbl 0919.01001  Makarios, T.J.M.: A mechanical verification of the independence of Tarski’s Euclidean axiom. Master’s thesis, Victoria University of Wellington (2012)  Martin, G.E.: The Foundations of Geometry and the Non-Euclidean Plane. Undergraduate Texts in Mathematics. Springer, Berlin (1998)  Millman, R.S., Parker, G.D.: Geometry, A Metric Approach with Models. Springer, Berlin (1981) · Zbl 0484.51019  Marić, F.; Petrović, D., Formalizing complex plane geometry, Ann. Math. Artif. Intell., 74, 271-308, (2014) · Zbl 1330.68264  Narboux, J.; Botana, F. (ed.); Lozano, ER (ed.), Mechanical theorem proving in Tarski’s geometry, No. 4869, 139-156, (2007), Pontevedra · Zbl 1195.03019  Pambuccian, V., Zum Stufenaufbau des Parallelenaxioms, J. Geom., 51, 79-88, (1994) · Zbl 0815.51012  Pambuccian, V.: Axiomatizations of hyperbolic and absolute geometries. In: Prékopa, A., Molnár, E. (eds.) Non-Euclidean Geometries, vol. 581, pp. 119-153. Springer, Berlin (2006). doi:10.1007/0-387-29555-0 · Zbl 1106.51008  Pambuccian, V., On the equivalence of Lagrange’s axiom to the Lotschnittaxiom, J. Geom., 95, 165-171, (2009) · Zbl 1189.51010  Pambuccian, V., Another equivalent of the Lotschnittaxiom, Beiträge zur Algebra und Geometrie/Contrib. Algebra Geom., 58, 167-170, (2017) · Zbl 1362.51004  Papadopoulos, A.: Master Class in Geometry. Notes on Non-Euclidean Geometry, Chapter 1. European Mathematical Society, Zurich (2012)  Pasch, M.: Vorlesungen über neuere Geometrie. Springer, Berlin (1976) · Zbl 0328.50001  Pejas, W., Die Modelle des Hilbertschen Axiomensystems der absoluten Geometrie, Math. Ann., 143, 212-235, (1961) · Zbl 0109.39001  Piesyk, Z., The existential and universal statements on parallels, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 9, 761-764, (1961) · Zbl 0104.14801  Rothe, F.: Several Topics from Geometry (2014). http://math2.uncc.edu/ frothe/3181all.pdf  Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983) · Zbl 0564.51001  Szmielew, W., Some metamathematical problems concerning elementary hyperbolic geometry, Stud. Log. Found. Math., 27, 30-52, (1959) · Zbl 0092.38601  Szmielew, W., A new analytic approach to hyperbolic geometry, Fundam. Math., 50, 129-158, (1961) · Zbl 0100.15701  Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951) · Zbl 0044.25102  Tarski, A.; Givant, S., Tarski’s system of geometry, Bull. Symb. Log., 5, 175-214, (1999) · Zbl 0932.01031  Trudeau, R.J.: The Non-Euclidean Revolution. Springer, Berlin (1986) · Zbl 0899.51015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.