It is well-known that both Presburger arithmetic (by contrast with Peano arithmetic) and Tarski geometry are decidable. I was in the shower this morning and wondered whether there exists an elegant mutual generalisation of these theories that is also decidable. In particular, I settled on the following system:

- The objects are the finite-dimensional affine subspaces of your favourite infinite-dimensional real Hilbert space (let's say $L^2$ for concreteness).
- We have a binary predicate, $x \subseteq y$, which inherits its usual meaning.
- We have a ternary predicate, $I(x, y; z)$, which means there is an isometry of the ambient space which fixes $z$ and maps $x$ bijectively onto $y$.

I'll show that this does indeed generalise both Presburger arithmetic and Tarski geometry.

Firstly, note that we can encode the concept of a point:

$$ x \textrm{ is a point } \iff \forall y . (y \subseteq x) \implies (y = x) $$

(It's rather cute that this is precisely how Euclid described a point, namely 'a point is that which has no part'.)

Similarly for lines:

$$ x \textrm{ is a line } \iff x \textrm{ is not a point and } \forall y . (y \subseteq x) \implies ((y = x) \textrm{ or } y \textrm{ is a point}) $$

We can continue inductively to define planes and so on.

We describe two lines $x, y$ as *parallel* if there is a plane which contains both $x$ and $y$, and there is no $z$ such that $z \subseteq x$ and $z \subseteq y$. This allows one to define \emph{parallelogram}, and emulate vector addition with respect to some origin $o$. That allows one to take Minkowski sums of affine subspaces with respect to $o$.

So far we haven't touched the ternary predicate $I(x, y; z)$. One rudimentary application is to equate distances between points:

$$ |a - b| = |d - c| \iff \exists e . (b + c = a + e) \textrm{ and } I(d, e; c) $$

Here we're using $(b + c = a + e)$ as shorthand for $e$ being a point and satisfying the vector addition property mentioned earlier. We can also compare distances: $|x - y| \geq |a - b|$ if and only if we can find points $c, d$ such that $b + b = c + d$ and $|x - y| = |a - c| = |a - d|$. Together with collinearity, this allows us to define Tarski's 'betweenness' predicate, so we can encode all of Tarskian geometry.

Another application of this predicate is to equate dimension:

$$ \dim(x) = \dim(y) \iff \exists z . I(x, y; z) $$

We can also add dimensions. Specifically, $\dim(x) + \dim(y) = \dim(z)$ if and only if we can find a point $o$ and spaces $a, b$ such that $\dim(a) = \dim(x)$, $\dim(b) = \dim(y)$, the intersection of $a$ and $b$ is $o$, and every point in $z$ can be expressed uniquely as a sum (as vectors relative to $o$) of a point in $a$ and a point in $b$.

This endows us with the ability to perform Presburger arithmetic on the dimensions of spaces.

Anyway, this prompts the question: is this theory (together with a suitable finite set of axioms) decidable? With 'bounded quantifiers' (i.e. bounded dimension), this reduces to $n$-dimensional Tarski geometry (and therefore is decidable). However, I feel this theory is much stronger since you can make first-order statements about arbitrary finite-dimensional vector spaces.