Undecidable First-Order Theories of Affine Geometries

TL;DR

This paper investigates the logical complexity of affine geometries, proving that the first-order theories of many geometric structures with added unary predicates are undecidable, thus refuting previous conjectures about their decidability.

Contribution

It demonstrates that for all n>1, the FO-theory of monadic expansions of affine geometries is _1-hard, and introduces a broad class of structures with undecidable theories, challenging prior assumptions.

Findings

Monadic expansions of affine geometries are _1-hard.

The FO-theory of a broad class of geometric structures is undecidable.

Weak universal MSO logic over expansions can be translated into universal MSO.

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^2,\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^2, 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. This is an extended version of a publication in the proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL 2012).