Can one design a geometry engine?
- 51 Downloads
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.
KeywordsEuclidean geometry Automated theorem proving Undecidability
Mathematics Subject Classification (2010)0108 03B25 03D35 5102 5103 51M05
Unable to display preview. Download preview PDF.
This paper has its origin in my lecture notes on automated theorem proving , 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  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.
- 3.Artin, E.: Geometric Algebra, volume 3 of Interscience Tracts in Pure and Applied Mathematics. Interscience Publishers (1957)Google Scholar
- 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
- 6.Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum I: Euclid-Hilbert. Philosophia Mathematicas (2017)Google Scholar
- 7.Baldwin, J.T.: Axiomatizing Changing Conceptions of the Geometric Continuum II: Archimedes-Descartes-Hilbert-Tarski Philosophia Mathematica (2017)Google Scholar
- 9.Basu, S.: Algorithms in real algebraic geometry: a survey. arXiv:1409.1534 (2014)
- 12.Beeson, M.: Some undecidable field theories. Translation of . 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)Google Scholar
- 14.Beeson, M.: Proving Hilbert’S Axioms in Tarski Geometry, 2014. Manuscript Posted on pdfs.semanticscholar.orgGoogle Scholar
- 15.Beth, E.W.: The Foundations of Mathematics: A Study in the Philosophy of Science, 2nd edn. Elsevier, Amsterdam (1964)Google Scholar
- 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
- 19.Blumenthal, L.M.: A Modern View of Geometry. Courier Corporation (1980)Google Scholar
- 22.Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Science & Business Media (2012)Google Scholar
- 23.Carlson, J.A., Jaffe, A., Wiles, A.: The Millennium Prize Problems. American Mathematical Soc. (2006)Google Scholar
- 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
- 27.Friedman, H.M., Visser, A.: When bi-interpretability implies synonymy. Logic Group Preprint Series 320, 1–19 (2014)Google Scholar
- 28.Gelernter, H.: Realization of a geometry theorem proving machine. In: IFIP Congress, pp. 273–281 (1959)Google Scholar
- 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.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.Hilbert, D., Ackermann, W.: Principles of Mathematical Logic. Chelsea Publishing company (1950)Google Scholar
- 33.Hartshorne, R.: Geometry: Euclid and Beyond. Springer (2000)Google Scholar
- 34.Hilbert, D.: Grundlagen der geometrie. Latest reprint 2013: Springer-verlag, 1899 originally published in (1899)Google Scholar
- 35.Hilbert, D.: The Foundations of Geometry. Open Court Publishing Company (1902)Google Scholar
- 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.Hodges, W.: Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1993)Google Scholar
- 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)Google Scholar
- 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)Google Scholar
- 51.Pillay, A.: An Introduction to Stability Theory. Courier Corporation (2008)Google Scholar
- 52.Poizat, B.: Les Petits Cailloux: Une Approche Modèle-Théorique De L’algorithmie, Aléas, Paris (1995)Google Scholar
- 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.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
- 58.Rooduijn, J.M.W.: Translating Theories. B.S. thesis, Universiteit Utrecht (2015)Google Scholar
- 60.Schur, F.: Grundlagen der Geometrie. BG Teubner (1909)Google Scholar
- 61.Shoenfield, J.: Mathematical Logic Addison-Wesley Series in Logic. Addison-Wesley (1967)Google Scholar
- 65.Szczerba, L.W.: Interpretability of elementary theories. In: Logic, Foundations of Mathematics, and Computability Theory, pp.129–145. Springer (1977)Google Scholar
- 68.Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)Google Scholar
- 69.Tarski, A., Mostowski, A., Robinson, R.M.: Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North Holland (1953)Google Scholar
- 70.Visser, A.: Categories of theories and interpretations. Logic Group Preprint Series, 228 (2004)Google Scholar
- 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.von Staudt, K.G.C.: Geometrie der lage. Bauer und Raspe (1847)Google Scholar
- 73.von Staudt, K.G.C.: Beiträge zur Geometrie der Lage, vol. 2. F. Korn (1857)Google Scholar
- 75.Wikipedia: Huzita-Hatori axioms. Wikipedia entry: https://en.wikipedia.org/wiki/Huzita-Hatori_axioms
- 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