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

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

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.

Review text

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 \textit{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.

Recommendations

Cites work

Cited in

(5)

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)