Semënov definability

What fragments of Semënov arithmetic let us say what?

Hera Brown

Department of Computer Science, University of Oxford, UK

Semënov arithmetic, the extension of Presburger arithmetic by the exponentiation function $x \mapsto 2^{\abs{x}}$, is decidable. That gives us good reason to be interested in knowing what the theory can define and express; if we have a problem that only requires those sets to be defined, then we know that that problem is decidable as well. So we’re interested in knowing the sorts of sets that can be defined in Semënov arithmetic, and in particular the sorts of sets it can define that can’t be defined in just Presburger arithmetic.

So let’s look at the sorts of sets we can define in Semënov arithmetic and variegated fragments thereof.

Definability strength of Semënov arithmetic

What sets can we define using Semënov arithmetic? Well, given that it’s an extension of Presburger arithmetic, every set that’s definable in Presburger arithmetic is also definable in Semënov arithmetic. That’s a good start. We can also define the set of powers of two, namely $\set{1, 2, 4, 8, 16, \dots}$, by writing the formula $\phi(x) \defeq \exists y\ x = 2^y$. A number $x$ satisfies that formula just when $x$ is of the form $2^y$ for some $y$, and so $x$ satisfies that formula just when it’s a power of two.

Modifying the above formula $\phi(x)$, we can then define more restricted series of exponentials. For instance, we can define the set of what I’ll call the even powers of two, or $\set{2^0, 2^2, 2^4, \dots}$. We just need to modify $\phi(x)$ to express that $y$ is an even number, and we can do that easily by writing $\psi(x) \defeq \exists y\ ((\exists z\ y = 2z) \and x = 2^y)$. Similarly, we can define the set $\set{2^k, 2^{2k}, 2^{3k}, \dots}$ for any $k$ we like.

Now, this is analogous to defining the sets $\set{0,1,2,3, \dots}$ and $\set{0,2,4,6,\dots}$ in standard Presburger arithmetic. In essence what we’re doing is defining a set of naturals of which $y$ is a member, and then lifting that set to the powers of two. We know that Presburger arithmetic defines precisely the sets that are semi-linear [3]; that is, precisely the sets that are finite unions of linear sets of the form $kn + c$ for integer coefficient $k$ and constant $c$. So we know that we can lift these semi-linear sets to powers, and define these sets in Semënov arithmetic.

Of course, we can lift formulae many times, for instance writing $\phi(x) \defeq \exists y \exists z\ (x = 2^y \and y = 2^z)$ to define the set of powers of powers of two $\set{2^1, 2^2, 2^4, 2^8, \dots}$. We can lift formulae like this arbitrarily high, and by taking unions of definable sets we can have multiple heights of powers of two appear in a set (so we can have, say, the set $\set{2^0, \smash{2^{2^0}}, 2^1, \smash{2^{2^{1}}}, \dots}$ definable in Semënov arithmetic). We can add powers of different sorts together, and also define sets like $\set{0 + 2^0 + \smash{2^{2^0}}, 1 + 2^1 + \smash{2^{2^1}}, 2 + 2^2 + \smash{2^{2^2}}, \dots}$.

If anything Semënov arithmetic defines too much. We can define pairing functions in Semënov arithmetic—that is, injective functions from pairs of naturals to naturals—using for instance the formula $\phi(x, y, z) \defeq 2^{x+y} + x = z$ to define one such pairing function.

It’s a result given in [2] that any arithmetic theory that can define pairing functions has a non-elementary complexity, though; that means the time it takes to decide a formula of length $n$ grows faster than each of the functions $\set{2^n, \smash{2^{2^n}}, \smash{2^{2^{2^n}}}, \dots}$. The result comes from the fact that, in such a theory with a pairing function, we can effectively arithmetise the running of a Turing machine that takes a non-elementary amount of time to terminate. Since Semënov arithmetic defines pairing functions, its decision problem has a non-elementary complexity.

The upshot of this is that, in practice, it’s infeasible to decide any but the smallest formulae of Semënov arithmetic. Despite that, we can restrict Semënov arithmetic so that it still talks about powers of two, but doesn’t allow variables to appear both inside and outside a power (as was the case in the pairing function above). That fragment is elementary [1], and so let’s look at how much can be said in it.

Definability strength of the predicate fragment

The predicate fragment of Semënov arithemtic is defined as the extension of Presburger arithmetic with a predicate $P$ that holds of just the powers of two (and we can define this $P$ in Semënov arithemtic as $P(x) \defeq \exists y\ 2^y = x$). That is, the domain of $P$ is the set $\set{1, 2, 4, 8, 16, \dots}$. At first glance it may seem that this is just as powerful as Semënov arithmetic generally, but that’s not actually the case. In particular, we don’t have access to the exponents of any powers of two that we define, and so we can’t say things like $\forall x \exists y\ 2^{x+y} > 2^x + y$. We can’t even define the powers of the powers of two; we only have access to the set $\set{1, 2, 4, 8, 16 \dots}$ and can’t filter out for powers of powers of two. So the predicate fragment of Semënov is strictly weaker than Semënov arithmetic more generally.

That being said, we aren’t restricted to defining just the set $\set{1, 2, 4, 8, 16, \dots}$ and nothing else; we can take the intersection of this set with certain semi-linear sets and use this to define more interesting sets of powers of two. For instance, on the face of it, it seems that the set of powers of four $\set{1, 4, 16, 64, \dots}$ isn’t definable in the predicate fragment. But we can define this set, using some number-theoretic properties of the powers of $4$.

In particular, notice that in the set of powers of four, all elements (apart from $1$) end in either a $4$ or a $6$. Likewise, for all the powers of two that aren’t powers of $4$ (namely the numbers $2, 8, 32, 128, \dots$, notice that all of those end in either a $2$ or an $8$. So, if we take the intersection of the powers of two with the set of numbers that end in a $4$ or $6$ (and then take the union of this with $\set{1}$), we get the set containing precisely the even powers of $4$.

Further, we can define the set of numbers that end in a $4$ or a $6$; that’s just the semi-linear set formed by the union of the linear sets generated by $10n + 4$ and $10n + 6$, which we can define with the Presburger formula $\phi(x) \defeq \exists y\ (x = 10y + 4 \or x = 10y + 6)$. Taking the conjunction of this formula with $P(x)$ (and so taking the intersection of the sets defined by each) we end up with a formula in the predicate fragment that defines precisely the powers of four. So we’re done.

This applies more generally, though. If we want to define the set $\set{2^{0n}, 2^{1n}, 2^{2n}, \dots}$ in the predicate fragment, it suffices to notice that $2^{kn}$ is congruent to $1$ mod $2^n -1$ for any value of $k$. We can express this sort of modular constraint in Presburger arithmetic, since everything here is finitely bounded, and so we can take the intersection of the set of all numbers congruent to $1$ mod $2^n -1$ with the set of powers of two, both definable in the predicate fragment, and so define the set $\set{2^{0n}, 2^{1n}, 2^{2n}, \dots}$ in the predicate fragment.

Generalising even further, we can see that the set of all powers of two whose exponents form a linear set, namely the set $\set{2^{0n + k}, 2^{1n + k}, 2^{2n + k}, \dots}$, contains precisely those powers of two congruent to $2^k$ mod $2^n - 1$. We can again define this modular constraint in Presburger arithmetic, take the intersection of the set thus defined with the set of powers of two, and so define the set of powers of two whose exponents form a linear set, all in the predicate fragment.

Taking unions of the sets defined above gets us the sets of powers of two whose exponents form a semi-linear set. Since Presburger arithmetic defines precisely the semi-linear sets, we end up with a neat result: the predicate fragment allows us to define all sets of powers whose exponents form a Presburger-definable set.

Conclusion

We’ve seen what sorts of sets can be defined in Semënov arithmetic generally, as well as the predicate fragment of Semënov arithmetic where we can only talk about variables appearing only in powers or only linearly. Complexity is tied to the sorts of sets that we can defined—generally more complex theories let us define more complex sets—but there’s still a decent amount we can do in the elementary predicate fragment as well, using a bit of number theory.

Bibliography