Finite-variable fragments of $\Delta_0$-formulas

Consider sets definable in the usual structure of arithmetic $(\mathbb{N},0,1,+,\times)$ by $\Delta_0$-formulas, i.e., formulas with bounded quantifiers. The quantifier alternation hierarchy has been studied,* which stratifies $\Delta_0$ formulas by the number of nested alternations of bounded quantifiers they contain.

My question is, is anything known about the finite variable hierarchy, in which formulas are stratified by the number of (distinct) variables that occur? In particular,

• Does it collapse or is it strict? (Perhaps under some complexity-theoretic assumptions?)
• One expects that since syntactically one can write formulas with arbitrary high quantifier alternation using only finitely many variables, or arbitrarily many variables using only a finite amount of quantifier alternation, if we restrict ourselves to formulas from a finite level in either hierarchy, the other one still does not collapse (Assuming neither collapse absolutely.). Is this true?

*See, e.g., Keith Harrow, "The bounded arithmetic hierarchy," http://www.sciencedirect.com/science/article/pii/S0019995878902577

• Since there is a (term-)definable pairing function, I think the bounded variable hierarchy does collapse. – Emil Jeřábek Mar 4 '17 at 8:01
• Emil, if I understand you correctly, you are suggesting that I prove that for all $\Delta_0$-formulas $R(x_1,\dots,x_n)$, there is a 2-variable (say) $\Delta_0$-formula $A(z)$ such that $A(\langle x_1,\dots,x_n\rangle )=R(x_1,\dots,x_n)$. – Siddharth Mar 4 '17 at 17:01
• (continuation of the last comment) If I'm proving this by induction on the construction of $R$, the problem I run into is in the case when $R$ is defined by bounded quantification from some other formula. It seems like we get something like $A(z)=Qx_i \le z\ B(f(z))$, where $B$ is definable in 2-variables, but the graph of the function $f$ might not be. I'll have to think about this more. – Siddharth Mar 4 '17 at 17:07

The bounded variable hierarchy collapses to a fixed finite level, because of the existence of definable pairing functions.

In more detail, I will use the Cantor pairing function $$\def\p#1{\langle#1\rangle}\def\N{\mathbb N}\let\eq\leftrightarrow\p{x,y}=\frac{(x+y)(x+y+1)}2+x,$$ which is a bijection $\N^2\to\N$. Let $l(z)$, $r(z)$ denote the corresponding projections, so that $$l(\p{x,y})=x,\qquad r(\p{x,y})=y,\qquad\p{l(z),r(z)}=z.$$ Since $\p{x,y}$ is a polynomial with rational coefficients, $\p{x,y}=z$ is equivalent to a quantifier-free (hence $3$-variable) formula, namely $$\p{x,y}=z\eq z+z=(x+y)\cdot(x+y+1)+x,$$ and consequently the functions $l$ and $r$ are definable by $\Delta_0$ formulas using $3$ distinct variables: $$l(z)=x\eq\exists y\le z\,\p{x,y}=z,$$ and similarly for $r$.

Proposition: Every $\Delta_0$ formula in one free variable is equivalent to a $\Delta_0$ formula using only $3$ distinct variables.

Proof:

It will be convenient to preprocess the formulas first. Let us call a bounded quantifier $\exists y\le t(\vec x)\,\theta(\vec x,y)$ safe if $$\bigl(\exists y\le t(\vec x)\,\theta(\vec x,y)\bigr)\eq\bigl(\exists y\,\theta(\vec x,y)\bigr),$$ in which case we can replace the bound $t(\vec x)$ with any larger bound without affecting the truth of the formula. Similarly for universal quantifiers. By replacing $\exists y\le t(\vec x)\,\theta$ with $\exists y\le t(\vec x)\,(y\le t(\vec x)\land\theta)$, and unwinding terms with the help of extra existential quantifiers, it is easy to see that any $\Delta_0$ formula is equivalent to a $\Delta_0$ formula $\theta(\vec x)$ such that

• all quantifiers in $\theta$ are safe,

• the index $i$ of any variable $x_i$ quantified in any subformula $\xi$ of $\theta$ is higher than the indices of all free variables of $\xi$, and

• all atomic subformulas of $\theta$ (except quantifier bounds) are of the forms $x_i=x_j$, $x_i+x_j=x_k$, or $x_i\cdot x_j=x_k$.

Let us call such formulas special.

Claim: For any special formula $\theta(x_0,\dots,x_n)$, there is a formula $\xi(z)$ using only $3$ distinct variables such that $$\xi(z)\eq\theta\bigl(r(l^n(z)),\dots,r(l(z)),r(z)\bigr).$$

Note that the Claim implies the Proposition: if $\xi(z)\eq\theta(r(z))$ can be written using $3$ variables, then so can $$\theta(x)\eq\exists z\le x^2\,\bigl(z=\p{0,x}\land\xi(z)\bigr).$$

We will prove the Claim by induction on the complexity of $\theta$.

The induction steps for Boolean connectives are trivial. The step for bounded quantifiers is also easy: if $\theta(x_0,\dots,x_n)$ is $\exists x_{n+1}\le t(\vec x)\,\theta'(x_0,\dots,x_{n+1})$, where the quantifier is safe, and $\xi'$ is a $3$-variable formula equivalent to $\theta'(r(l^{n+1}(z)),\dots,r(l(z)),r(z))$, then \begin{align*} \theta(r(l^n(z)),\dots,r(z))&\eq\exists x_{n+1}\,\xi'(\p{z,x_{n+1}})\\ &\eq\exists w\,(l(w)=z\land\xi'(w))\\ &\eq\exists w\le s(z)\,(l(w)=z\land\xi'(w)) \end{align*} for a suitable term $s(z)$.

It remains to prove the Claim for special atomic formulas. First, notice that since $l$ and $r$ are definable using $3$ variables, the same holds for any finite composition of these functions: for example, $$x=l^{n+1}(z)\eq\exists y\le z\,(x=l(y)\land y=l^n(z)),$$ where we proceed to expand the inner formulas. This immediately takes care of atomic formulas $x_i=x_j$, as $$r(l^i(z))=r(l^j(z))\eq\exists x\le z\,(x=r(l^i(z))\land x=r(l^j(z))).$$ For the formulas $x_i+x_j=x_k$ (and similarly $x_i\cdot x_j=x_k$), we can proceed as follows: $$r(l^i(z))+r(l^j(z))=r(l^k(z))\eq\exists w\le t(z)\,(l(l(w))=r(l^i(z))\land r(l(w))=r(l^j(z))\land r(w)=r(l^k(z))\land\exists x,z\le w\,(w=\p{\p{x,z},x+z})).$$ (Note that we recycled the $z$ variable.) Here, $l(l(w))=r(l^i(z))$ can be written as $\exists x\le w\,(x=l(l(w))\land x=r(l^i(z)))$, which we know how to handle, and similarly for the other two conjuncts. Finally, $$w=\p{\p{x,z},x+z}$$ can be written as an identity using no further variables, as $\p{\p{x,z},x+z}$ is a polynomial with rational coefficients in $x$ and $z$ (and $x+z$). QED

Corollary: Every $\Delta_0$ formula in $n$ free variables is equivalent to a $\Delta_0$ formula using $\max\{3,n+1\}$ distinct variables.

• We only used elementary properties of the pairing function, hence the equivalence is not just true in $\N$, it is provable in a very weak theory: IOpen is certainly enough (probably $\mathrm{PA}^-$ will suffice with a little care).
• The result still holds for bounded formulas in a richer language with extra binary functions or relations. Even more generally, if we expand the language with $k$-ary functions and relations with $k>2$, the result holds with $k+1$ in place of $3$.
• The transformation more-or-less preserves quantifier complexity: for any $i\ge1$, an $E_i$ formula in $n$ free variables is equivalent to an $E_i$ formula using $\max\{3,n+1\}$ distinct variables, and similarly for $U_i$. However, we need to make sure the $E_i$ and $U_i$ classes are defined in such a way as to explicitly allow conjunctions and disjunctions; of course, we cannot reduce the number of distinct variables in prenex formulas.
• @EmilJeřábek, really nice, thank you! Sorry for the delay in getting to read this--I still need to go through it carefully. Here's what I'm currently wondering: it seems like the bounds on the bounded quantifiers can in general be polynomials. If we insist that they are single variables (e.g., allow $\exists x \le z$ but forbid $\exists x \le z^2$), does the proof still go through? – Siddharth Mar 19 '17 at 2:35