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.

| cite | improve this question | | | | |
  • $\begingroup$ first-order statements about arbitrary finite-dimensional vector spaces aren't usually considered undecidable $\endgroup$ – JMP Nov 27 '15 at 13:59
  • $\begingroup$ @JonMarkPerry He's not saying they are, he's just saying that this is evidence that the theory described is much stronger than $n$-dimensional Tarski geometry. $\endgroup$ – Noah Schweber Nov 29 '15 at 8:15
  • $\begingroup$ @NoahSchweber Let $\varphi$ be the statement "for all x, there exists y with dim(y) > dim(x)". That is true in my theory, but false in every $T_n$. $\endgroup$ – Adam P. Goucher Nov 29 '15 at 12:10
  • 1
    $\begingroup$ This is a great question! Is there a statement in Tarski geometry that is true in $n$ dimensions if and only if $n$ is prime, say? $\endgroup$ – Will Sawin Dec 2 '15 at 13:54
  • 1
    $\begingroup$ Another question along the lines of Will Sawin's is: can we express "this subspace has square dimension" in this language? I suspect not. But if so, then multiplication is definable also (because $x=y^2$ iff $x$ and $x+y+y+1$ are consecutive squares, and because $x=yz$ iff $(y+z)^2=y^2+z^2+x+x$), and then the theory would be undecidable. $\endgroup$ – Matt F. Dec 4 '15 at 21:25

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.


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.

| cite | improve this answer | | | | |
  • $\begingroup$ Given what you've done, you should be able to encode (fixing an origin $o$) "$z = x\oplus y$" and then "$w \subset x\oplus y$ is the graph of a linear map $x\to y$" and finally "$z$ is isomorphic to $x\otimes y$" at which point $\dim y = (\dim x)^2 \Leftrightarrow y \cong x\otimes x$. $\endgroup$ – Lior Silberman Dec 6 '15 at 17:39
  • $\begingroup$ @LiorSilberman, I see how to express the first two statements there with first-order formulas, but not the third. The definition for "$z$ is isomorphic to $x \otimes y$" might start with "for every graph $w$ of a linear map there is a unique element of $z$ such that....", but then I don't see how to finish the definition. If it works it probably fits in a comment. $\endgroup$ – Matt F. Dec 6 '15 at 18:34
  • $\begingroup$ Ah -- I see the problem. The graph of a bilinear map is not a subspace. $\endgroup$ – Lior Silberman Dec 6 '15 at 18:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.