Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries

DOI10.1007/S10472-018-9610-1zbMATH Open1439.03033arXiv1712.07474OpenAlexW2778452107WikidataQ128785024 ScholiaQ128785024MaRDI QIDQ2631966FDOQ2631966

Authors: Johann A. Makowsky 

Publication date: 16 May 2019

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Abstract: We survey the status of decidabilty of the consequence relation in various axiomatizations of 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: (A) The first order consequence relations for Wu's orthogonal and metric geometries (Wen-Ts"un 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 (B) 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.

Full work available at URL: https://arxiv.org/abs/1712.07474

Recommendations

• The undecidability of orthogonal and origami geometries
• scientific article; zbMATH DE number 3926284
• Old and new results in the foundations of elementary plane Euclidean and non-Euclidean geometries
• Some new results on decidability for elementary algebra and geometry
• Undecidable First-Order Theories of Affine Geometries

zbMATH Keywords

Euclidean geometryundecidabilityautomated theorem proving

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Euclidean geometries (general) and generalizations (51M05) Undecidability and degrees of sets of sentences (03D35)

Cites Work

• Title not available (Why is that?)
• COMPLEXITY AND REAL COMPUTATION: A MANIFESTO
• Title not available (Why is that?)
• Undecidable theories
• A mathematical introduction to logic.
• Graph structure and monadic second-order logic. A language-theoretic approach
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Algorithms in real algebraic geometry
• Orthogonality as single primitive notion for metric planes
• Title not available (Why is that?)
• Projective Planes
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• On a question of Abraham Robinson
• Real quantifier elimination is doubly exponential
• Title not available (Why is that?)
• Basic principles of mechanical theorem proving in elementary geometries
• Title not available (Why is that?)
• Definability and decision problems in arithmetic
• Axiomatizing geometric constructions
• Euclid and his twentieth century rivals. Diagrams in the logic of Euclidean geometry
• Title not available (Why is that?)
• Tarski's System of Geometry
• Title not available (Why is that?)
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• Elimination of quantifiers in algebraic structures
• Algorithmic uses of the Feferman-Vaught theorem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof and computation in geometry
• A refutational approach to geometry theorem proving
• Axiomatizing Changing Conceptions of the Geometric Continuum I: Euclid-Hilbert†
• Ternary Operations as Primitive Notions for Constructive Plane Geometry V
• Title not available (Why is that?)
• Model Theory and the Philosophy of Mathematical Practice
• Title not available (Why is that?)
• A mathematical theory of origami constructions and numbers
• Some new results on decidability for elementary algebra and geometry
• Definability and decidability in infinite algebraic extensions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Defining \(\mathbb Z\) in \(\mathbb Q\)
• MORITA EQUIVALENCE
• From geometry to conceptual relativity
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Title not available (Why is that?)
• Über Metatheoretische Eigenschaften Einiger Geometrischer Theorien
• Title not available (Why is that?)
• Rekursive Unentscheidbarkeit der Theorie der pythagoräischen Körper
• Unentscheidbarkeit Der Euklidischen Inzidenzgeometrie
• Logical Approaches to Computational Barriers

Cited In (2)

• Axiomatizing origami planes
• STRONGLY MINIMAL STEINER SYSTEMS I: EXISTENCE

This page was built for publication: Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631966)