Implementing Euclid’s straightedge and compass constructions in type theory. (English) Zbl 1479.03009

Kellison, Ariel; Bickford, Mark; Constable, Robert

Ann. Math. Artif. Intell. 85, No. 2-4, 175-192 (2019).

The article illustrates how to formalise Euclid’s constructions by straightedge and compass in a variant of constructive type theory. The core of the work presents a set of axioms implemented in the Nuprl proof assistant, to encode the fundamental constructions of Euclidean geometry in the plane.
The Euclidean plane is rendered by the type of points equipped with four relations: congruence, to express when two segments have the same length; betweenness to say when a point lies between two other points; apartness to model when two points are separated; and leftness to declare when a point is on the left of an oriented segment from a point to another one. Using these primitives, the three fundamental constructions can be readily expressed: given two segment suitably placed in the plane, they intersect and the point of intersection is identified as a term in type theory; given a segment and a circle suitably placed in the plane, the segment can be extended to a new one whose endpoints, identified as terms in type theory, intersect the circle; finally, given two circles suitably placed in the plane, their intersections are identified as terms in type theory. In addition, it is postulated that, fixed two separated points, every point \(P\) in the plane is separated from one of them: the postulate also identifies which point is separated from \(P\).
On this basis, the work shows how the initial propositions of Euclid’s Elements can be deduced. Finally, the paper discusses which kind of models are admissible for these axioms, considering the constructive nature of the system.
The contribution is well written and very clear. It also provides a brief but comprehensive set of references to other formalisations in the same line. The proper scientific content is accessible also to non experts with a little effort, while the paper still provides insights and ideas to the specialist.

Reviewer: Marco Benini (Buccinasco)

MSC:

03B35	Mechanization of proofs and logical operations
03F55	Intuitionistic mathematics
51M04	Elementary problems in Euclidean geometries
03B38	Type theory

Keywords:

constructive type theory; constructive geometry; foundations of geometry

Software:

Nuprl; OTTER

References:

[1]	Mäenpää, P.; von Plato, J., The logic of Euclidean construction procedures, Acta Philos. Fenn, 49, 275-293, (1990) · Zbl 0778.03020
[2]	Heyting, A., Axioms for intuitionistic plane affine geometry, Studies in Logic and the Foundations of Mathematics, 27, 160-173, (1959) · Zbl 0092.25002
[3]	Dalen, D., Outside as a primitive notion in constructive projective geometry, Geom. Dedicata., 60, 107-111, (1996) · Zbl 0846.51001
[4]	Dalen, D.V.: Extension problems in intuitionistic plane projective geometry. [Online]. Available: https://www.illc.uva.nl/Research/Publications/Dissertations/HDS-15-Dirk-van-Dalen.text.pdf
[5]	Mandelkern, M., A constructive real projective plane, J. Geom., 107, 19-60, (2016) · Zbl 1339.51001
[6]	von Plato, J., The axioms of constructive geometry, Ann. Pure Appl. Logic, 76, 169-200, (1995) · Zbl 0836.03034
[7]	von Plato, J., A constructive theory of ordered affine geometry, Indag. Math., 9, 549-562, (1998) · Zbl 0926.51014
[8]	Beeson, M.: Constructive geometry. In: Proceedings of the 10th Asian Logic Conference, pp. 19-84 (2009). [Online]. Available: http://www.worldscientific.com/doi/abs/10.1142/9789814293020_0002 · Zbl 1193.03021
[9]	Beeson, M., Brouwer and Euclid, Indag. Math., 29, 483-533, (2018) · Zbl 1437.03171
[10]	Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the nuprl proof development system. [Online]. Available: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.4216 (1985)
[11]	Constable, RL, Programs as proofs: a synopsis, Inf. Process. Lett., 16, 105-112, (1983) · Zbl 0514.68043
[12]	Vesley, R., Constructivity in geometry, History and Philosophy of Logic, 20, 291-294, (1999) · Zbl 1051.51500
[13]	Heyting, A., Zur intuitionistischen axiomatik der projektiven geometrie, Math. Ann., 98, 491-538, (1928) · JFM 53.0541.01
[14]	Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967) · Zbl 0183.01503
[15]	Knuth, D.E.: Axioms and Hulls. Springer, Berlin (1992). [Online]. Available: https://books.google.com/books/about/Axioms_and_hulls.html?id=vghRAAAAMAAJ · Zbl 0777.68012
[16]	Lombard M.; Vesley, R., A common axiom set for classical and intuitionistic plane geometry, Ann. Pure Appl. Logic, 95, 229-255, (1998) · Zbl 0922.03082
[17]	Beeson, M.: Logic of Ruler and Compass Constructions, pp. 46-55. Springer, Heidelberg (2012). [Online]. Available: http://link.springer.com/10.1007/978-3-642-30870-3_6 · Zbl 1357.03093
[18]	Beeson, M., A constructive version of Tarski’s geometry, Ann. Pure Appl. Logic, 166, 1199-1273, (2015) · Zbl 1392.03059
[19]	Sernaker, S., Constable, R.L.: Formal exploration of geometry. [Online]. Available: http://www.nuprl.org/MathLibrary/geometry/ (2016)
[20]	Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983). [Online]. Available: http://link.springer.com/10.1007/978-3-642-69418-9 · Zbl 0564.51001
[21]	Boutry, P., Gries, C., Narboux, J., Schreck, P.: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, pp. 1-68. [Online]. Available: http://link.springer.com/10.1007/s10817-017-9422-8 (2017) · Zbl 1441.03011
[22]	Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Automated Deduction in Geometry, pp. 139-156. Springer, Berlin (2006). [Online]. Available: http://link.springer.com/10.1007/978-3-540-77356-6_9 · Zbl 1195.03019
[23]	Beeson M., Wos, L.: OTTER proofs in Tarskian geometry. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning, pp. 495-510. Springer International Publishing, Cham (2014) · Zbl 1414.68099
[24]	Meikle L.I., Fleuriot, J.D.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. [Online]. Available: http://link.springer.com/10.1007/10930755_21 (2003) · Zbl 1279.68291
[25]	Calderón, G.: Formalizing constructive projective geometry in Agda. In: LSFA 2017: the 12th Workshop on Logical and Semantic Frameworks, with Applications, Brasília, pp. 150-165 (2017). [Online]. Available: http://lsfa2017.cic.unb.br/LSFA2017.pdf
[26]	Kahn, G.: Constructive geometry according to Jan von Plato. V5,10 (1995)
[27]	Constable, R.L.: The semantics of evidence. Cornell University, Ithaca, NY, Tech Rep. (1985)
[28]	Wadler, P., Propositions as types, Commun. ACM, 58, 75-84, (2015)
[29]	Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’ s elements. The Review of Symbolic Logic 2(4). [Online]. Available: http://repository.cmu.edu/philosophy (2009) · Zbl 1188.03008
[30]	Heath, T.: The Thirteen Books of Euclid’s Elements. Dover, New York (1956) · Zbl 0071.24203
[31]	Allen, S.; Bickford, M.; Constable, R.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E., Innovations in computational type theory using Nuprl, J. Appl. Log., 4, 428-469, (2006) · Zbl 1107.68090
[32]	Tarski, A.; Givant, S., Tarski’s system of geometry, Bull. Symb. Log., 5, 175-214, (1999) · Zbl 0932.01031
[33]	Bickford, M.: Constructive analysis and experimental mathematics using the Nuprl proof assistant. [Online]. Available: http://www.nuprl.org/documents/Bickford/reals.pdf (2016)