{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article7173","name":"Undecidable First-Order Theories of Affine Geometries","abstract":"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 monadic expansions of (R^n,\\beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\\beta), where T is a subset of R^n, and show that for each structure (T,\\beta) in C, the FO-theory of the class of monadic expansions of (T,\\beta) is undecidable. We then consider classes of expansions of structures (T,\\beta) 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,\\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. An extended version of this article can be found on the ArXiv (arXiv:1208.4930v1).","keywords":["Tarski\u2019s geometry","undecidability","spatial logic","classical logic"],"author":[{"@type":"Person","name":"Kuusisto, Antti","givenName":"Antti","familyName":"Kuusisto"},{"@type":"Person","name":"Meyers, Jeremy","givenName":"Jeremy","familyName":"Meyers"},{"@type":"Person","name":"Virtema, Jonni","givenName":"Jonni","familyName":"Virtema"}],"position":36,"pageStart":470,"pageEnd":484,"dateCreated":"2012-09-03","datePublished":"2012-09-03","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Kuusisto, Antti","givenName":"Antti","familyName":"Kuusisto"},{"@type":"Person","name":"Meyers, Jeremy","givenName":"Jeremy","familyName":"Meyers"},{"@type":"Person","name":"Virtema, Jonni","givenName":"Jonni","familyName":"Virtema"}],"copyrightYear":"2012","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.470","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6219","volumeNumber":16,"name":"Computer Science Logic (CSL'12) - 26th International Workshop\/21st Annual Conference of the EACSL","dateCreated":"2012-09-03","datePublished":"2012-09-03","editor":[{"@type":"Person","name":"C\u00e9gielski, Patrick","givenName":"Patrick","familyName":"C\u00e9gielski"},{"@type":"Person","name":"Durand, Arnaud","givenName":"Arnaud","familyName":"Durand"}],"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article7173","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6219"}}}