{"docId":728,"paperId":728,"url":"https:\/\/lmcs.episciences.org\/728","doi":"10.2168\/LMCS-9(4:26)2013","journalName":"Logical Methods in Computer Science","issn":"","eissn":"1860-5974","volume":[{"vid":147,"name":"Volume 9, Issue 4"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"1310.8200","repositoryVersion":3,"repositoryLink":"https:\/\/arxiv.org\/abs\/1310.8200v3","dateSubmitted":"2013-01-18 00:00:00","dateAccepted":"2015-06-25 11:41:02","datePublished":"2013-12-30 00:00:00","titles":["Undecidable First-Order Theories of Affine Geometries"],"authors":["Kuusisto, Antti","Meyers, Jeremy","Virtema, Jonni"],"abstracts":["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.","Comment: 23 pages, 4 figures. arXiv admin note: substantial text overlap with arXiv:1208.4930"],"keywords":["Computer Science - Logic in Computer Science","Mathematics - Logic"]}