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 β, and a quaternary equidistance relation \equiv. Tarski established, inter alia, that the first-order (FO) theory of (R^2,β,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,β) 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,β) with just one unary predicate is not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,β), and show that for each structure (T,β) in C, the FO-theory of the class of expansions of (T,β) with a single unary predicate is undecidable. We then consider classes of expansions of structures (T,β) 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,β). While the logics are incomparable in general, over expansions of (R^n,β), formulae of weak universal MSO translate into equivalent formulae of universal MSO.