Antti Kuusisto ; Jeremy Meyers ; Jonni Virtema - Undecidable First-Order Theories of Affine Geometries

lmcs:728 - Logical Methods in Computer Science, December 30, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:26)2013
Undecidable First-Order Theories of Affine Geometries

Authors: Antti Kuusisto ; Jeremy Meyers ; Jonni Virtema ORCID-iD

    Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation \beta, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n>1, the FO-theory of the class of expansions of (R^2,\beta) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), and show that for each structure (T,\beta) in C, the FO-theory of the class of expansions of (T,\beta) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,\beta) with a restricted unary predicate, for example a finite predicate, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivities of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO.


    Volume: Volume 9, Issue 4
    Published on: December 30, 2013
    Accepted on: June 25, 2015
    Submitted on: January 18, 2013
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic

    Linked data

    Source : ScholeXplorer IsPartOf DOI 10.4230/lipics.csl.2012
    • 10.4230/lipics.csl.2012
    LIPIcs, Volume 16, CSL'12, Complete Volume
    Durand, Arnaud ;

    Share

    Consultation statistics

    This page has been seen 456 times.
    This article's PDF has been downloaded 308 times.