zbMATH — the first resource for mathematics

Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries. (English) Zbl 1439.03033
Written for “practitioners of symbolic computation or automated theorem proving,” this is a survey of undecidability results for elementary (first-order) geometries, with particular emphasis on “affine incidence geometry, Hilbert-style Euclidean geometry, Wu’s orthogonal geometry and Origami geometry.” The author shows
\(\bullet\) how the segment calculus allows for a transfer of the undecidability results known to hold for theories of fields to that of elementary geometries, \(\bullet\) how the result by M. Ziegler [Enseign. Math., II. Sér. 28, 269–280 (1982; Zbl 0519.12018)], which states that every finitely axiomatized field theory that has \(\mathbb{R}\) or \(\mathbb{C}\) as a model is hereditarily undecidable, can be used to prove the undecidability of a plethora of finitely axiomatized elementary geometries, and
\(\bullet\) that the consequences in the universal fragment of geometries over fields are decidable.
He also indicates that these results can be extended to projective, elliptic, hyperbolic, and higher-dimensional geometries.
03B25 Decidability of theories and sets of sentences
03D35 Undecidability and degrees of sets of sentences
51M05 Euclidean geometries (general) and generalizations
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] Alperin, RC, A mathematical theory of origami constructions and numbers, New York J. Math., 6, 133, (2000) · Zbl 1065.51501
[3] Artin, E.: Geometric Algebra, volume 3 of Interscience Tracts in Pure and Applied Mathematics. Interscience Publishers (1957) · Zbl 0077.02101
[4] Artin, E.: Coordinates in affine geometry. In: Collected Papers of E. Artin, pp. 505-510. Springer, 1965. Originally: Notre Dame Math. Coll (1940) · Zbl 0060.32501
[5] Tarski, A.; Givant, S., Tarski’s system of geometry, Bull. Symb. Log., 5, 175-214, (1999) · Zbl 0932.01031
[6] Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum I: Euclid-Hilbert. Philosophia Mathematicas (2017)
[7] Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum II: Archimedes-Descartes-Hilbert-Tarski Philosophia Mathematica (2017)
[8] Baldwin, J.T.: Model Theory and the Philosophy of Mathematical Practice. Cambridge University Press, Cambridge (2018) · Zbl 1393.03002
[9] Basu, S.: Algorithms in real algebraic geometry: a survey. arXiv:1409.1534 (2014)
[10] Boutry, P.; Braun, G.; Narboux, J., Formalization of the arithmetization of euclidean plane geometry and applications, J. Symb. Comput., 90, 149-168, (2019) · Zbl 1394.68349
[11] Blum, L., Cucker, F, Shub, M., Smale, S.: Complexity and Real Computation. Springer, Berlin (1998) · Zbl 0872.68036
[12] Beeson, M.: Some undecidable field theories. Translation of [78]. Available at www.michaelbeeson.com/research/papers/Ziegler.pdf
[13] Beeson, M.: Proof and computation in geometry. In: International Workshop on Automated Deduction in Geometry, 2012, vol. 7993 of LNAI, pp. 1-30. Springer (2013) · Zbl 1397.03018
[14] Beeson, M.: Proving Hilbert’S Axioms in Tarski Geometry, 2014. Manuscript Posted on pdfs.semanticscholar.org
[15] Beth, E.W.: The Foundations of Mathematics: A Study in the Philosophy of Science, 2nd edn. Elsevier, Amsterdam (1964)
[16] Balbiani, P., Goranko, V., Kellerman, R., Vakarelov, D.: Logical Theories for Fragments of Elementary Geometry. Handbook of Spatial Logics, pp. 343-428 (2007)
[17] Barrett, TW; Halvorson, H., Morita equivalence, Rev. Symb. Log., 9, 556-582, (2016) · Zbl 1397.03017
[18] Barrett, TW; Halvorson, H., From geometry to conceptual relativity, Erkenntnis, 82, 1043-1063, (2017) · Zbl 1417.03043
[19] Blumenthal, L.M.: A Modern View of Geometry. Courier Corporation (1980) · Zbl 0499.51001
[20] Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, volume 10 of Algorithms and Computation in Mathematics. Springer, Berlin (2003) · Zbl 1031.14028
[21] Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-order Logic, a Language Theoretic Approach. Cambridge University Press, Cambridge (2012) · Zbl 1257.68006
[22] Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Science & Business Media (2012)
[23] Carlson, J.A., Jaffe, A., Wiles, A.: The Millennium Prize Problems. American Mathematical Soc. (2006) · Zbl 1155.00001
[24] Descartes, R.: A discourse on the method of correctly conducting one’s reason and seeking truth in the sciences. Oxford University Press, 2006. Annotated new translation of the 1637 original by Ian Maclean
[25] Davenport, JH; Heintz, J., Real quantifier elimination is doubly exponential, J. Symb. Comput., 5, 29-35, (1988) · Zbl 0663.03015
[26] Enderton, H., Enderton, H.B.: A Mathematical Introduction to Logic. Elsevier, Amsterdam (2001). Reprint · Zbl 0992.03001
[27] Friedman, HM; Visser, A., When bi-interpretability implies synonymy, Logic Group Preprint Series, 320, 1-19, (2014)
[28] Gelernter, H.: Realization of a geometry theorem proving machine. In: IFIP Congress, pp. 273-281 (1959)
[29] Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers Presented at the May 3-5, 1960, Western Joint IRE-AIEE-ACM Computer Conference, pp. 143-149. ACM (1960)
[30] Ghourabi, F., Ida, T., Takahashi, H., Marin, M., Kasem, A.: Logical and algebraic view of Huzita’s origami axioms with applications to computational origami. In: Proceedings of the 2007 ACM Symposium on Applied Computing, pp. 767-772. ACM (2007)
[31] Hilbert, D., Ackermann, W.: Principles of Mathematical Logic. Chelsea Publishing company (1950) · Zbl 0040.00402
[32] Hall, M., Projective planes, Trans. Am. Math. Soc., 54, 229-277, (1943) · Zbl 0060.32209
[33] Hartshorne, R.: Geometry: Euclid and Beyond. Springer (2000) · Zbl 0954.51001
[34] Hilbert, D.: Grundlagen der geometrie. Latest reprint 2013: Springer-verlag, 1899 originally published in (1899)
[35] Hilbert, D.: The Foundations of Geometry. Open Court Publishing Company (1902) · JFM 33.0082.10
[36] Hilbert, D.: Foundations of Geometry Second Edition, translated from the Tenth Edition, revised and enlarged by Dr Paul Bernays. The Open Court Publishing Company, La Salle, Illinois (1971)
[37] Hodges, W.: Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1993)
[38] Hauschild, K.; Rautenberg, W., Rekursive unentscheidbarkeit der theorie der pythagoräischen körper, Fundam. Math., 82, 191-197, (1974) · Zbl 0299.02056
[39] Ivanov, N.V.: Affine planes, ternary rings, and examples of non-desarguesian planes. arXiv:1604.04945 (2016)
[40] Justin, J.: Résolution par le pliage de équation du troisieme degré et applications géométriques. In: Proceedings of the First International Meeting of Origami Science and Technology, pp. 251-261. Ferrara, Italy (1989)
[41] Kapur, D., A refutational approach to geometry theorem proving, Artif. Intell., 37, 61-93, (1988) · Zbl 0678.68094
[42] Koenigsmann, J., Defining \(\mathbb {Z}\)ℤ in \(\mathbb {Q}\)ℚ, Ann. Math., 183, 73-93, (2016) · Zbl 1390.03032
[43] Koenigsmann, J., On a question of Abraham Robinson, Israel J. Math., 214, 931-943, (2016) · Zbl 1402.12002
[44] Makowsky, JA, Algorithmic uses of the feferman-Vaught theorem, Ann. Pure Appl. Log., 126.1-3, 159-213, (2004) · Zbl 1099.03009
[45] Makowsky, J.A.: Topics in automated theorem proving, 1989-2015. Course 236 714, Faculty of Computer Science, Technion-Israel Institute of Technology, Haifa, Israel, available at http://www.cs.technion.ac.il/janos/COURSES/THPR-2015/
[46] Miller, N.: Euclid and his Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry. CSLI Publications Stanford (2007) · Zbl 1129.01001
[47] MacintyreAngus, A.; McKenna, K.; den Dries, LL, Elimination of quantifiers in algebraic structures, Adv. Math., 47, 74-87, (1983) · Zbl 0531.03016
[48] Pambuccian, V., Ternary operations as primitive notions for constructive plane geometry v, Math. Log. Q., 40, 455-477, (1994) · Zbl 0808.03045
[49] Pambuccian, V., Orthogonality as a single primitive notion for metric planes, Contributions to Algebra and Geometry, 49, 399-409, (2007) · Zbl 1161.51004
[50] Pambuccian, V., Axiomatizing geometric constructions, J. Appl. Log., 6, 24-46, (2008) · Zbl 1143.03007
[51] Pillay, A.: An Introduction to Stability Theory. Courier Corporation (2008) · Zbl 1227.03046
[52] Poizat, B.: Les Petits Cailloux: Une Approche Modèle-Théorique De L’algorithmie, Aléas, Paris (1995) · Zbl 0832.68044
[53] Prunescu, M.: Fast quantifier elimination means p= np. In: Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, Cie 2006, Swansea, UK, June 30-July 5, 2006, Proceedings, vol. 3988, pp. 459. Springer Science & Business Media (2006)
[54] Rabin, M.O.: A simple method for undecidability proofs and some applications. In: Bar-Hillel, Y. (ed.) Logic, Methodology and Philosophy of Science, pp. 58-68. North-Holland Publishing Company (1965)
[55] Rautenberg, W., Unentscheidbarkeit der Euklidischen Inzidenzgeometrie, Math. Log. Q., 7, 12-15, (1961) · Zbl 0166.26304
[56] Rautenberg, W., ÜBer metatheoretische Eigenschaften einiger geometrischer Theorien, Math. Log. Q., 8, 5-41, (1962) · Zbl 0112.24701
[57] Robinson, J., Definability and decision problems in arithmetic, J. Symb. Log., 14, 98-114, (1949) · Zbl 0034.00801
[58] Rooduijn, J.M.W.: Translating Theories. B.S. thesis, Universiteit Utrecht (2015)
[59] Solovay, RM; Arthan, RD; Harrison, J., Some new results on decidability for elementary algebra and geometry, Ann. Pure Appl. Log., 163, 1765-1802, (2012) · Zbl 1259.03020
[60] Schur, F.: Grundlagen der Geometrie. BG Teubner (1909) · JFM 40.0517.01
[61] Shoenfield, J.: Mathematical Logic Addison-Wesley Series in Logic. Addison-Wesley (1967)
[62] Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983) · Zbl 0564.51001
[63] Steinitz, E., Algebraische Theorie der Körper, Journal fúr reine und angewandte Mathematik, 137, 167-309, (1910) · JFM 41.0445.03
[64] Shlapentokh, A.; Videla, C., Definability and decidability in infinite algebraic extensions, Ann. Pure Appl. Log., 165, 1243-1262, (2014) · Zbl 1352.12006
[65] Szczerba, L.W.: Interpretability of elementary theories. In: Logic, Foundations of Mathematics, and Computability Theory, pp.129-145. Springer (1977) · Zbl 0375.02005
[66] Szmielew, W.: From Affine to Euclidean Geometry, an Axiomatic Approach. Polish Scientific Publishers (Warszawa-Poland) and D. Reidel Publishing Company, Dordrecht-Holland (1983) · Zbl 0516.51001
[67] Tarski, A., Sur les ensembles définissables de nombre réels, Fundam. Math., 17, 210-239, (1931) · JFM 57.0060.02
[68] Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951) · Zbl 0044.25102
[69] Tarski, A., Mostowski, A., Robinson, R.M.: Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North Holland (1953) · Zbl 0053.00401
[70] Visser, A.: Categories of theories and interpretations. Logic Group Preprint Series, 228 (2004)
[71] Visser, A.: Categories of Theories and Interpretations. In: Logic in Tehran. Proceedings of the workshop and conference on Logic, Algebra and Arithmetic, held October 18-22 (2006) · Zbl 1107.03066
[72] von Staudt, K.G.C.: Geometrie der lage. Bauer und Raspe (1847)
[73] von Staudt, K.G.C.: Beiträge zur Geometrie der Lage, vol. 2. F. Korn (1857)
[74] Wu, W.; Gao, X., Mathematics mechanization and applications after thirty years, Frontiers of Computer Science in China, 1, 1-8, (2007)
[75] Wikipedia: Huzita-Hatori axioms. Wikipedia entry: https://en.wikipedia.org/wiki/Huzita-Hatori_axioms
[76] Wu, W-T, Basic principles of mechanical theorem proving in elementary geometries, J. Autom. Reason., 2, 221-252, (1986) · Zbl 0642.68163
[77] Wu, W.-T.: Mechanical Theorem Proving in Geometries. Springer, Berlin (1994). (original in chinese 1984)
[78] Ziegler, M.: Einige unentscheidbare Körpertheorien. In: Strassen, V., Engeler, E. , Läuchli, H. (eds.) Logic and Algorithmic, An international Symposium Held in Honour of E. Specker, pp. 381-392. L’enseignement mathematiqué (1982)
[79] Zorn, M., Eleventh meeting of the association for symbolic logic, J. Symb. Log., 14, 73-80, (1949)
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.