Kuusisto, Antti ;
Meyers, Jeremy ;
Virtema, Jonni
Undecidable FirstOrder Theories of Affine Geometries
Abstract
Tarski initiated a logicbased approach to formal geometry that studies firstorder structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the firstorder (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FOtheory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FOtheory of monadic expansions of (R^n,\beta) is Pi^1_1hard 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 FOtheory 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).
BibTeX  Entry
@InProceedings{kuusisto_et_al:LIPIcs:2012:3691,
author = {Antti Kuusisto and Jeremy Meyers and Jonni Virtema},
title = {{Undecidable FirstOrder Theories of Affine Geometries}},
booktitle = {Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL},
pages = {470484},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897422},
ISSN = {18688969},
year = {2012},
volume = {16},
editor = {Patrick C{\'e}gielski and Arnaud Durand},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3691},
URN = {urn:nbn:de:0030drops36910},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2012.470},
annote = {Keywords: Tarski’s geometry, undecidability, spatial logic, classical logic}
}
Keywords: 

Tarski’s geometry, undecidability, spatial logic, classical logic 
Seminar: 

Computer Science Logic (CSL'12)  26th International Workshop/21st Annual Conference of the EACSL

Issue date: 

2012 
Date of publication: 

2012 