Is this theory decidable?

Question

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.

Answer 1

Here are some comments and the start of a positive answer. I can prove three things:

• 1) If "$x$ has square dimension" is expressible in this language, then the theory is undecidable.

• 2) The binary predicate is not needed for the expressive power of the theory, and the theory is equally decidable or undecidable without it.

• 3) For $$\phi=(Q_1x_1)(Q_2x_2)...(Q_nx_n)P(x_1,\ldots,x_n)$$ with $P$ quantifier-free, let $$\phi^b = (Q_1x_1\le 2^n)(Q_2x_2\le 2^{n+1})...(Q_nx_n \le 2^{2n-1)})P(x_1,\ldots,x_n)$$ where each $Q_i$ is either $\forall$ or $\exists$, and $Qx\le n$ is restricted to $x$ of dimension $\le n$. Then the schema $$\phi \implies \phi^b$$ would show that the theory is decidable. I also have some ideas for why this might hold.

Proofs:

1) If the squares are definable, then we can define $x=y^2$ by "$x$ and $x+y+y+1$ are consecutive squares". Then we can also define $x=yz$ by $(y+z)^2=y^2+z^2+x+x$, which makes the theory undecidable.

2) The predicate $x\subseteq z$ is equivalent to $\forall y\ I(x,y,z) \rightarrow x=y$.

2a) If $x$ is contained in $z$ then obviously any isometry fixing $z$ can only take $x$ to itself.

2b) Suppose that any isometry fixing $z$ can only take $x$ to itself. Let $p$ be a point in $z$, with $x-p$ and $z-p$ being the spaces of vectors from $p$ to $x$ and $z$. Construct an orthonormal basis $v_i$ for the ambient vector space such that $\{v_1\ldots v_n\}$ is a basis for $z-p$, and $\{v_1\ldots v_{n+k}\}$ spans both $z-p$ and $x-p$. Then consider an isometry of the space that:

• fixes $p$ and $p+v_i$ for $i\le n$
• switches $p+v_i$ with $p+v_{i+k}$ for $n+1\le i\le n+k$
• fixes $p+v_i$ for $i>n+2k$.

This isometry fixes $z$. So by hypothesis, it must take $x$ to itself. So it must not switch any basis vectors. So $k=0$ and $x$ must be contained in $z$.

3) If the schema holds, then we can decide the truth of a sentence $\phi_0$ by putting it into prenex normal form $\phi$, and evaluating the truth of $\phi^b$ using the standard Tarski decision procedure. The combination of $\phi \implies \phi^b$ and $\psi \implies \psi^b$, where $\psi$ is the prenex form of $\neg \phi$, is enough to show that $\phi$ and $\phi^b$ are equivalent.

Why we should expect that $\phi \implies \phi^b$?

A good test case is $$\phi = \forall w\, \exists x\, \forall y \,\exists z\, P(w,x,y,z)$$ with $P$ quantifier-free. If $\phi$ holds then there are Skolem functions $f_2$ and $f_4$ such that $$\forall w\, \forall y\, P( w, f_2(w), y, f_4( w, y )).$$ Then we can show $\phi^b$ by showing that other Skolem functions $g_2$ and $g_4$, whose ranges have dimensions at most $32$ and $128$, satisfy $$\forall w \le 16\, \forall y\le 64\, P( w, g_2(w), y, g_4( w, y )).$$ The idea is to get rid of unneeded dimensions from the images of $f_2$ and $f_4$, since no configuration describable by this many quantifiers will need more than these dimensions. This seems easy enough to prove for any particular true $\phi$, and perhaps someone will see how to articulate the argument that we can do it generally.

Which bounds should we use?

Suppose we want bounds $$\phi^b = (Qx_1 \le a_1) \cdots (Qx_n \le a_n) P(x_1, \ldots x_n)$$ with the $a$'s depending on $n$ but independent of the $Q$'s and $P$. Consider the examples $$\phi_j = \forall x_1 \cdots \forall x_{j-1} \exists x_j \cdots \exists x_n \bigwedge_{i<j} x_i \subset x_j \wedge \bigwedge_{i\ge j} x_{i+1} \subset x_i$$

Then $\phi_1$ can only be satisfied with $x_1$ of dimension at least $n-1$.

So the lowest possibility for $\phi_1^b$ is $a_1= n-1$.

The lowest simultaneous possibility for $\phi_1^b$ and $\phi_2^b$ is $a_1 = n-1,\, a_2 = n$.

The lowest simultaneous possibility for $\phi_1^b, \ldots \phi_4^b$ is $a_1 = n-1,\, a_2 = n,\, a_3 = 2n,\, a_4 = 4n$.

Since these $a_i$ grow exponentially, the statement of claim 3 seemed easiest using only powers of 2, and that seems like a convenient form in which to try to prove the decidability.