Undecidable First-Order Theories of Affine Geometries

DOI10.4230/LIPICS.CSL.2012.470MaRDI QIDQ4649566zbMATH OpenOpenAlexFDO

Authors Antti Kuusisto, Jeremy Meyers, Jonni Virtema

Publication date 22 November 2012

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

zbMATH Keywords

classical logicspatial logicTarski's geometryundecidability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Foundations of classical theories (including reverse mathematics) (03B30)

Abstract: Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (�eta) and a quaternary equidistance relation (equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,�eta,equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,�eta) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of monadic expansions of (R^2,�eta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,�eta), where T is a subset of R^2, and show that for each structure (T,�eta) in C, the FO-theory of the class of monadic expansions of (T,�eta) is undecidable. We then consider classes of expansions of structures (T,�eta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n,�eta). While the logics are incomparable in general, over expansions of (R^n,�eta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. This is an extended version of a publication in the proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012).

Recommendations

• Undecidable first-order theories of affine geometries
• Undecidability of the theory of projective planes
• scientific article; zbMATH DE number 1076941
• Algebraic geometry in first-order logic
• Geometrisation of first-order logic
• scientific article; zbMATH DE number 3901538
• The undecidability of orthogonal and origami geometries
• Undecidability of the first order theories of free noncommutative Lie algebras
• scientific article; zbMATH DE number 3150814
• Inaccessibility and undecidability in computation, geometry, and dynamical systems

Cited in

(1)

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

This page was built for publication: Undecidable First-Order Theories of Affine Geometries

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