Notes - Logic and Proof MT24, Lower bounds for deciding real arithmetic

It is $\mathbf{NEXPTIME}$-hard, i.e. it is at least as hard as deciding whether a non-deterministic Turing machine will halt in at most $2^n$ steps.

Given a non-deterministic Turing machine $M$ and $n$ in unary, we can find a sentence $\varphi _ M$ that is true iff $M$ halts in at most $2^n$ steps. To do this, we:

• Find a formula $\text{Mult} _ n(x, y, z)$ that encodes the statement $x = yz$ and $0 \le z \le 2^{2^n} - 1$ (why $2^{2^n}$? intuitively, deciding $\mathbf{EXP}$ corresponds to an exponential factor, and then since it’s nondeterministic, it’s $2^{2^n}$). This formula should have length $O(n)$.
• Use this to create a formula $\text{Pow} _ n(x)$ which encodes that $x$ is a power of two and $0 \le x \le 2^{2^n} - 1$.
• Use this to then define $\text{Bit} _ n(x, y)$ that is true when $x = 2^k$ and the $k$-th bit of $y$ is $1$ (and $0 \le x, y \le 2^{2^n} - 1$).
• Use this to encode the valid transitions of the Turing machine starting from an empty tape.

Induct on $n$. The base case is straightforward, since the following will suffice:

\[\text{Mult}_0(x, y, z) := (z = 0 \land x = 0) \lor (z = 1 \land x = y)\]

For the inductive step, suppose we have an $O(n)$-size formula for $\text{Mult} _ n(x, y, z)$.

Note that any integer $z \in I _ {n+1}$ can be written in the form

\[\begin{aligned} z &= 2^{2^n} q + r \\\\ &= (2^{2^n} - 1)q + q + r \end{aligned}\]

where $q, r \in I _ n$. This means that every $z \in I _ {n+1}$ can be written $z = z _ 1 z _ 2 + z _ 2 + z _ 3$ for some $z _ 1, z _ 2, z _ 3 \in I _ n$. Therefore $\text{Mult} _ {n+1}(x, y, z)$ iff

\[\exists z_1 \exists z_2 \exists z_3 \left( \bigwedge^3_{i = 1} (z_i \in I_n) \land (z = z_1 z_2 + z_2 + z_3) \land z = (yz_1)z_2 + yz_2 + yz_3 \right)\]

which leads to the following definition:

\[\begin{aligned} \text{Mu}&\text{lt}_{n+1}(x, y, z) := \exists z_1 \exists z_2 \exists z_3 \exists y_1 \exists y_2 \exists y_3 \exists y_4( \\\\ & (z = y_1 + z_2 + z_3) \land (x = y_3 + y_2 + y_4) \\\\ & \land(\text{Mult}_n(y_1, z_1, z_2) \land \text{Mult}_n(y_2, y, z_2) \land \text{Mult}_n(y_3, y_2, z_1) \land \text{Mult}_n(y_4, y, z_3)) \\\\ ) \end{aligned}\]

The only problem is that the four occurrences of $\text{Mult} _ n$ would mean that the above definition grows in length exponentially. However, we can apply the Fisher-Rabin trick and instead introduce new universally quantified variables to replace them with just one occurrence of $\text{Mult} _ n$.

\[\forall z ((z = x \lor z = y) \to \varphi(z))\]