Can one design a geometry engine?

On the (un)decidability of certain affine Euclidean geometries
  • Johann A. MakowskyEmail author


We survey the status of decidability of the first order consequences in various axiomatizations of Hilbert-style Euclidean geometry. We draw attention to a widely overlooked result by Martin Ziegler from 1980, which proves Tarski’s conjecture on the undecidability of finitely axiomatizable theories of fields. We elaborate on how to use Ziegler’s theorem to show that the consequence relations for the first order theory of the Hilbert plane and the Euclidean plane are undecidable. As new results we add:


The first order consequence relations for Wu’s orthogonal and metric geometries (Wen-Tsün Wu, 1984), and for the axiomatization of Origami geometry (J. Justin 1986, H. Huzita 1991) are undecidable.

It was already known that the universal theory of Hilbert planes and Wu’s orthogonal geometry is decidable. We show here using elementary model theoretic tools that


the universal first order consequences of any geometric theory T of Pappian planes which is consistent with the analytic geometry of the reals is decidable.

The techniques used were all known to experts in mathematical logic and geometry in the past but no detailed proofs are easily accessible for practitioners of symbolic computation or automated theorem proving.


Euclidean geometry Automated theorem proving Undecidability 

Mathematics Subject Classification (2010)

0108 03B25 03D35 5102 5103 51M05 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.



This paper has its origin in my lecture notes on automated theorem proving [45], developed in the last 15 years. I was motivated to develop this material further, when I prepared a lecture on P. Bernays and the foundations of geometry, which I gave at the occasion of the unveiling in summer 2017 of a plaque at the house where P. Bernays used to live in Göttingen, before going into forced exile in 1933. P. Bernays edited Hilbert’s [35] from the 5th (1922) till the 10th edition (1967), see also [34, 36]. I am indebted to R. Kahle, who invited me to give this lecture. Without this invitation this paper would not have been written.

I was lucky enough to know P. Bernays personally, as well as some other pioneers of the modern foundations of geometry, among them R. Baer, H. Lenz, W. Rautenberg, W. Schwabhäuser, W. Szmielew and A. Tarski. I dedicate this paper to them, and to my wonderful teacher of descriptive geometry, M. Herter, at the Gymnasium Freudenberg during 1961-1967 in Zurich, Switzerland. Blessed be their memory.

I would also like to thank L. Kovacs and P. Schreck for their patience and flexibility concerning the deadline for submitting this paper to the special issue on Formalization of Geometry and Reasoning of the Annals of Mathematics and Artificial Intelligence. Special thanks are due to five anonymous referees and to J. Baldwin for critical remarks and suggestions, as well as for pointing out various imprecise statements, which I hope were all corrected.


  1. 1.
    Avigad, J., Dean, E., Mumma, J.: A formal system for Euclid’s elements. Rev. Symb. Log. 2(4), 700–768 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alperin, R.C.: A mathematical theory of origami constructions and numbers. New York J. Math. 6(119), 133 (2000)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Artin, E.: Geometric Algebra, volume 3 of Interscience Tracts in Pure and Applied Mathematics. Interscience Publishers (1957)Google Scholar
  4. 4.
    Artin, E.: Coordinates in affine geometry. In: Collected Papers of E. Artin, pp. 505–510. Springer, 1965. Originally: Notre Dame Math. Coll (1940)Google Scholar
  5. 5.
    Tarski, A., Givant, S.: Tarski’s system of geometry. Bull. Symb. Log. 5(2), 175–214 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum I: Euclid-Hilbert. Philosophia Mathematicas (2017)Google Scholar
  7. 7.
    Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum II: Archimedes-Descartes-Hilbert-Tarski Philosophia Mathematica (2017)Google Scholar
  8. 8.
    Baldwin, J.T.: Model Theory and the Philosophy of Mathematical Practice. Cambridge University Press, Cambridge (2018)CrossRefzbMATHGoogle Scholar
  9. 9.
    Basu, S.: Algorithms in real algebraic geometry: a survey. arXiv:1409.1534 (2014)
  10. 10.
    Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of euclidean plane geometry and applications. J. Symb. Comput. 90, 149–168 (2019)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Blum, L., Cucker, F, Shub, M., Smale, S.: Complexity and Real Computation. Springer, Berlin (1998)CrossRefzbMATHGoogle Scholar
  12. 12.
    Beeson, M.: Some undecidable field theories. Translation of [78]. Available at
  13. 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)Google Scholar
  14. 14.
    Beeson, M.: Proving Hilbert’S Axioms in Tarski Geometry, 2014. Manuscript Posted on pdfs.semanticscholar.orgGoogle Scholar
  15. 15.
    Beth, E.W.: The Foundations of Mathematics: A Study in the Philosophy of Science, 2nd edn. Elsevier, Amsterdam (1964)Google Scholar
  16. 16.
    Balbiani, P., Goranko, V., Kellerman, R., Vakarelov, D.: Logical Theories for Fragments of Elementary Geometry. Handbook of Spatial Logics, pp. 343–428 (2007)Google Scholar
  17. 17.
    Barrett, T.W., Halvorson, H.: Morita equivalence. Rev. Symb. Log. 9(3), 556–582 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Barrett, T.W., Halvorson, H.: From geometry to conceptual relativity. Erkenntnis 82(5), 1043–1063 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Blumenthal, L.M.: A Modern View of Geometry. Courier Corporation (1980)Google Scholar
  20. 20.
    Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry, volume 10 of Algorithms and Computation in Mathematics. Springer, Berlin (2003)CrossRefzbMATHGoogle Scholar
  21. 21.
    Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-order Logic, a Language Theoretic Approach. Cambridge University Press, Cambridge (2012)CrossRefzbMATHGoogle Scholar
  22. 22.
    Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Science & Business Media (2012)Google Scholar
  23. 23.
    Carlson, J.A., Jaffe, A., Wiles, A.: The Millennium Prize Problems. American Mathematical Soc. (2006)Google Scholar
  24. 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 MacleanGoogle Scholar
  25. 25.
    Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 29–35 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Enderton, H., Enderton, H.B.: A Mathematical Introduction to Logic. Elsevier, Amsterdam (2001). ReprintzbMATHGoogle Scholar
  27. 27.
    Friedman, H.M., Visser, A.: When bi-interpretability implies synonymy. Logic Group Preprint Series 320, 1–19 (2014)Google Scholar
  28. 28.
    Gelernter, H.: Realization of a geometry theorem proving machine. In: IFIP Congress, pp. 273–281 (1959)Google Scholar
  29. 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)Google Scholar
  30. 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)Google Scholar
  31. 31.
    Hilbert, D., Ackermann, W.: Principles of Mathematical Logic. Chelsea Publishing company (1950)Google Scholar
  32. 32.
    Hall, M.: Projective planes. Trans. Am. Math. Soc. 54(2), 229–277 (1943)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Hartshorne, R.: Geometry: Euclid and Beyond. Springer (2000)Google Scholar
  34. 34.
    Hilbert, D.: Grundlagen der geometrie. Latest reprint 2013: Springer-verlag, 1899 originally published in (1899)Google Scholar
  35. 35.
    Hilbert, D.: The Foundations of Geometry. Open Court Publishing Company (1902)Google Scholar
  36. 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)Google Scholar
  37. 37.
    Hodges, W.: Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1993)Google Scholar
  38. 38.
    Hauschild, K., Rautenberg, W.: Rekursive unentscheidbarkeit der theorie der pythagoräischen körper. Fundam. Math. 82(3), 191–197 (1974)CrossRefzbMATHGoogle Scholar
  39. 39.
    Ivanov, N.V.: Affine planes, ternary rings, and examples of non-desarguesian planes. arXiv:1604.04945 (2016)
  40. 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)Google Scholar
  41. 41.
    Kapur, D.: A refutational approach to geometry theorem proving. Artif. Intell. 37(1-3), 61–93 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Koenigsmann, J.: Defining \(\mathbb {Z}\) in \(\mathbb {Q}\). Ann. Math. 183(1), 73–93 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    Koenigsmann, J.: On a question of Abraham Robinson. Israel J. Math. 214(2), 931–943 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 44.
    Makowsky, J.A.: Algorithmic uses of the feferman-Vaught theorem. Ann. Pure Appl. Log. 126.1-3, 159–213 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 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
  46. 46.
    Miller, N.: Euclid and his Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry. CSLI Publications Stanford (2007)Google Scholar
  47. 47.
    MacintyreAngus, A., McKenna, K., Van den Dries, L.L.: Elimination of quantifiers in algebraic structures. Adv. Math. 47(1), 74–87 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Pambuccian, V.: Ternary operations as primitive notions for constructive plane geometry v. Math. Log. Q. 40(4), 455–477 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  49. 49.
    Pambuccian, V.: Orthogonality as a single primitive notion for metric planes. Contributions to Algebra and Geometry 49, 399–409 (2007)MathSciNetzbMATHGoogle Scholar
  50. 50.
    Pambuccian, V.: Axiomatizing geometric constructions. J. Appl. Log. 6(1), 24–46 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    Pillay, A.: An Introduction to Stability Theory. Courier Corporation (2008)Google Scholar
  52. 52.
    Poizat, B.: Les Petits Cailloux: Une Approche Modèle-Théorique De L’algorithmie, Aléas, Paris (1995)Google Scholar
  53. 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)Google Scholar
  54. 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)Google Scholar
  55. 55.
    Rautenberg, W.: Unentscheidbarkeit der Euklidischen Inzidenzgeometrie. Math. Log. Q. 7(1-5), 12–15 (1961)MathSciNetCrossRefzbMATHGoogle Scholar
  56. 56.
    Rautenberg, W.: ÜBer metatheoretische Eigenschaften einiger geometrischer Theorien. Math. Log. Q. 8(1-5), 5–41 (1962)CrossRefzbMATHGoogle Scholar
  57. 57.
    Robinson, J.: Definability and decision problems in arithmetic. J. Symb. Log. 14(2), 98–114 (1949)MathSciNetCrossRefzbMATHGoogle Scholar
  58. 58.
    Rooduijn, J.M.W.: Translating Theories. B.S. thesis, Universiteit Utrecht (2015)Google Scholar
  59. 59.
    Solovay, R.M., Arthan, R.D., Harrison, J.: Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Log. 163(12), 1765–1802 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  60. 60.
    Schur, F.: Grundlagen der Geometrie. BG Teubner (1909)Google Scholar
  61. 61.
    Shoenfield, J.: Mathematical Logic Addison-Wesley Series in Logic. Addison-Wesley (1967)Google Scholar
  62. 62.
    Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)CrossRefzbMATHGoogle Scholar
  63. 63.
    Steinitz, E.: Algebraische Theorie der Körper. Journal fúr reine und angewandte Mathematik 137, 167–309 (1910)MathSciNetzbMATHGoogle Scholar
  64. 64.
    Shlapentokh, A., Videla, C.: Definability and decidability in infinite algebraic extensions. Ann. Pure Appl. Log. 165(7), 1243–1262 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  65. 65.
    Szczerba, L.W.: Interpretability of elementary theories. In: Logic, Foundations of Mathematics, and Computability Theory, pp.129–145. Springer (1977)Google Scholar
  66. 66.
    Szmielew, W.: From Affine to Euclidean Geometry, an Axiomatic Approach. Polish Scientific Publishers (Warszawa-Poland) and D. Reidel Publishing Company, Dordrecht-Holland (1983)zbMATHGoogle Scholar
  67. 67.
    Tarski, A.: Sur les ensembles définissables de nombre réels. Fundam. Math. 17, 210–239 (1931)CrossRefzbMATHGoogle Scholar
  68. 68.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)Google Scholar
  69. 69.
    Tarski, A., Mostowski, A., Robinson, R.M.: Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North Holland (1953)Google Scholar
  70. 70.
    Visser, A.: Categories of theories and interpretations. Logic Group Preprint Series, 228 (2004)Google Scholar
  71. 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)Google Scholar
  72. 72.
    von Staudt, K.G.C.: Geometrie der lage. Bauer und Raspe (1847)Google Scholar
  73. 73.
    von Staudt, K.G.C.: Beiträge zur Geometrie der Lage, vol. 2. F. Korn (1857)Google Scholar
  74. 74.
    Wu, W., Gao, X.: Mathematics mechanization and applications after thirty years. Frontiers of Computer Science in China 1(1), 1–8 (2007)CrossRefGoogle Scholar
  75. 75.
    Wikipedia: Huzita-Hatori axioms. Wikipedia entry:
  76. 76.
    Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221–252 (1986)CrossRefzbMATHGoogle Scholar
  77. 77.
    Wu, W.-T.: Mechanical Theorem Proving in Geometries. Springer, Berlin (1994). (original in chinese 1984)CrossRefGoogle Scholar
  78. 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)Google Scholar
  79. 79.
    Zorn, M.: Eleventh meeting of the association for symbolic logic. J. Symb. Log. 14(1), 73–80 (1949). ASLCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Faculty of Computer ScienceTechnion–Israel Institute of TechnologyHaifaIsrael

Personalised recommendations