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)\).

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: DOI
[1] Avigad, J.; Dean, E.; Mumma, J., A formal system for Euclid’s elements, Rev. Symb. Log., 2, 700-768, (2009) · Zbl 1188.03008
[2] 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)
[3] Amira, D., Sur l’axiome de droites parallèles, L’Enseign. Math., 32, 52-57, (1933) · Zbl 0008.26904
[4] 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
[5] 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
[6] Bachmann, F.: Aufbau der Geometrie aus dem Spiegelungsbegriff. Grundlehren der mathematischen Wissenschaften. Springer, Berlin (1973) · Zbl 0254.50001
[7] Beeson, M.; Boutry, P.; Narboux, J., Herbrand’s theorem and non-Euclidean geometry, Bull. Symb. Log., 21, 111-122, (2015) · Zbl 1375.03079
[8] 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
[9] 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
[10] Beeson, M., A constructive version of Tarski’s geometry, Ann. Pure Appl. Log., 166, 1199-1273, (2015) · Zbl 1392.03059
[11] Beeson, M., Constructive geometry and the parallel postulate, Bull. Symb. Log., 22, 1-104, (2016) · Zbl 1403.03130
[12] Beeson, M.: Brouwer and Euclid. Indagationes Mathematicae. To appear in a special issue devoted to Brouwer (2017)
[13] Bell, JL, Hilbert’s \(\epsilon \)-operator in intuitionistic type theories, Math. Log. Q., 39, 323-337, (1993) · Zbl 0802.03005
[14] Birkhoff, GD, A set of postulates for plane geometry (based on scale and protractors), Ann. Math., 33, 329-345, (1932) · Zbl 0004.12602
[15] 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)
[16] Braun, G.; Narboux, J.; Ida, T. (ed.); Fleuriot, J. (ed.), From Tarski to Hilbert, No. 7993, 89-109, (2012), Edinburgh
[17] Braun, G.; Narboux, J., A synthetic proof of Pappus’ theorem in Tarski’s geometry, J. Autom. Reason., 58, 23, (2017) · Zbl 1405.03034
[18] 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)
[19] 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)
[20] Bonola, R.: Non-Euclidean Geometry: A Critical and Historical Study of Its Development. Courier Corporation, North Chelmsford (1955) · JFM 43.0557.02
[21] Borsuk, K., Szmielew, W.: Foundations of Geometry. North-Holland, Amsterdam (1960) · Zbl 0093.33301
[22] Cajori, F.: A History of Elementary Mathematics. Macmillan, London (1898) · JFM 46.1421.01
[23] 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
[24] Coxeter, H.S.M.: Non-Euclidean Geometry. Cambridge University Press, Cambridge (1998) · Zbl 0909.51003
[25] 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
[26] Dehn, M., Die Legendre’schen Sätze über die Winkelsumme im Dreieck, Math. Ann., 53, 404-439, (1900) · JFM 31.0471.01
[27] Duprat, J.: Fondements de géométrie euclidienne. https://hal.inria.fr/hal-00661537 (2010)
[28] 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
[29] Friedrich, C., Bolyai, F.: Briefwechsel zwischen Carl Friedrich Gauss und Wolfgang Bolyai. BG Teubner, Leipzig (1899)
[30] 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)
[31] 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)
[32] Greenberg, MJ, Aristotle’s axiom in the foundations of geometry, J. Geom., 33, 53-57, (1988) · Zbl 0655.51010
[33] Greenberg, M.J.: Euclidean and Non-Euclidean Geometries—Development and History. Macmillan, London (1993) · Zbl 0418.51001
[34] 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
[35] Gupta, H.N.: Contributions to the axiomatic foundations of geometry. PhD thesis, University of California, Berkley (1965)
[36] Hartshorne, R.: Geometry: Euclid and Beyond, Undergraduate Texts in Mathematics. Springer, Berlin (2000) · Zbl 0954.51001
[37] 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)
[38] Kline, M.: Mathematical Thought from Ancient to Modern Times, vol. 3. Oxford University Press, Oxford (1990) · Zbl 0784.01048
[39] 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
[40] 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)
[41] Lewis, FP, History of the parallel postulate, Am. Math. Mon., 27, 16-23, (1920)
[42] Laubenbacher, R., Pengelley, D.: Mathematical Expeditions: Chronicles by the Explorers. Springer, Berlin (2013) · Zbl 0919.01001
[43] Makarios, T.J.M.: A mechanical verification of the independence of Tarski’s Euclidean axiom. Master’s thesis, Victoria University of Wellington (2012)
[44] Martin, G.E.: The Foundations of Geometry and the Non-Euclidean Plane. Undergraduate Texts in Mathematics. Springer, Berlin (1998)
[45] Millman, R.S., Parker, G.D.: Geometry, A Metric Approach with Models. Springer, Berlin (1981) · Zbl 0484.51019
[46] Marić, F.; Petrović, D., Formalizing complex plane geometry, Ann. Math. Artif. Intell., 74, 271-308, (2014) · Zbl 1330.68264
[47] Narboux, J.; Botana, F. (ed.); Lozano, ER (ed.), Mechanical theorem proving in Tarski’s geometry, No. 4869, 139-156, (2007), Pontevedra · Zbl 1195.03019
[48] Pambuccian, V., Zum Stufenaufbau des Parallelenaxioms, J. Geom., 51, 79-88, (1994) · Zbl 0815.51012
[49] 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
[50] Pambuccian, V., On the equivalence of Lagrange’s axiom to the Lotschnittaxiom, J. Geom., 95, 165-171, (2009) · Zbl 1189.51010
[51] Pambuccian, V., Another equivalent of the Lotschnittaxiom, Beiträge zur Algebra und Geometrie/Contrib. Algebra Geom., 58, 167-170, (2017) · Zbl 1362.51004
[52] Papadopoulos, A.: Master Class in Geometry. Notes on Non-Euclidean Geometry, Chapter 1. European Mathematical Society, Zurich (2012)
[53] Pasch, M.: Vorlesungen über neuere Geometrie. Springer, Berlin (1976) · Zbl 0328.50001
[54] Pejas, W., Die Modelle des Hilbertschen Axiomensystems der absoluten Geometrie, Math. Ann., 143, 212-235, (1961) · Zbl 0109.39001
[55] 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
[56] Rothe, F.: Several Topics from Geometry (2014). http://math2.uncc.edu/ frothe/3181all.pdf
[57] Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983) · Zbl 0564.51001
[58] Szmielew, W., Some metamathematical problems concerning elementary hyperbolic geometry, Stud. Log. Found. Math., 27, 30-52, (1959) · Zbl 0092.38601
[59] Szmielew, W., A new analytic approach to hyperbolic geometry, Fundam. Math., 50, 129-158, (1961) · Zbl 0100.15701
[60] Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951) · Zbl 0044.25102
[61] Tarski, A.; Givant, S., Tarski’s system of geometry, Bull. Symb. Log., 5, 175-214, (1999) · Zbl 0932.01031
[62] 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.