Is the set of formulas equivalent to a bounded formula decidable

171 Views Asked by At

In C. Papdimitriou, Computational Complexity a bounded (first order) formula over the signature of the natural numbers with addition and multiplication is defined the following way:

We use the notation $(\forall x < t)\phi$, where $t$ is a term, as an abbreviation for $\forall x((x < t) \Rightarrow \phi)$; similary for $(\exists x < t)\phi$. We call these bounded quantifiers. When all quantifiers (bounded and unbounded) precede the rest of the expression, we say that the expression is in bounded prenex form. So, sentence $(\forall x < 9)\exists y(\forall z < 2\times y(x + z + 10 < 4\times y)$ is in bounded prenex form (although it is not in prenex form if we expand the abbreviation $\forall x < 9$). We call a sentence bounded if all of its universal quantifiers are bounded, and the sentence is in bounded prenex form.

He then goes on to show that:

Suppose that $\phi$ is a bounded sentence. Then $\mathbb N \models \phi$ if and only if $\{ NT \} \vdash \phi$

Where $NT$ stands for a finite set of axioms regarding addition and multiplication.

Now my question. For a given formula, is it decidable if it is equivalent to a bounded formula? I would say yes, building up some prenex normal form, and then checking the expression should be managable, otherwise, regarding the Theorem I would suspect this not to be the case, as then the bounded sentences satisfied by $\mathbb N$ would be decidable.

1

There are 1 best solutions below

0
On BEST ANSWER

I suppose "equivalence" here means "$T$-provable equivalence" for some appropriate background theory $T$ of arithmetic (like $PA$). If so, then - as long as $T$ is reasonably strong - the answer to the question is no.

$PA$ has a weak completeness property: if $\sigma$ is a bounded-quantifier sentence in the language of arithmetic, then $PA$ decides $\sigma$. (In fact much more is true - $NT$ is enough to decide $\sigma$, as you state.) Conversely, any sentence which $PA$ decides is either $PA$-equivalent to $0=0$ or is $PA$-equivalent to $0=1$. So we have:

A sentence $\varphi$ in the language of arithmetic is $PA$-equivalent to a bounded-quantifier sentence iff it is decidable in $PA$.

Since the set of sentences decidable in $PA$ is incomputable (indeed, has Turing degree $0'$), this implies that the answer to your question is "no."


Note that the above is really about sentences (and $PA$-decidability) as opposed to formulas. We can also ask what happens if we talk about equivalence over the structure $\mathbb{N}$ itself. The answer is the same in this situation - in fact, the problem of telling whether a formula is equivalent to one with bounded quantifiers gets even harder.

Say that two formulas are $\mathbb{N}$-equivalent if they hold of the same tuples of natural numbers (that is, define the same subset of the appropriate Cartesian power of $\mathbb{N}$). Note that every sentence (thought of as a $0$-ary formula) is $\mathbb{N}$-equivalent to either $0=0$ or $0=1$, so the situation is uninteresting there. We now ask:

What formulas are $\mathbb{N}$-equivalent to bounded-quantifier formulas?

The key observation is that bounded-quantifier formulas define computable (in fact, better than computable) sets. So any formula which defines a non-computable set can't be equivalent over $\mathbb{N}$ to a bounded-quantifier formula.

Now consider the standard formula $\eta(x)$ defining the halting problem: $\eta$ holds of $n\in\mathbb{N}$ iff the $n$th Turing machine halts on input $n$. For an arbitrary sentence $\varphi$ in the language of arithmetic, consider the formulas $\varphi^+(x)=\eta(x)\wedge\varphi$ and $\varphi^-(x)=\eta(x)\vee\varphi$.

  • If $\varphi$ is true in $\mathbb{N}$, then $\varphi^-(x)$ is $\mathbb{N}$-equivalent to $x=x$ and $\varphi^-(x)$ is $\mathbb{N}$-equivalent to $\eta(x)$; so if $\varphi$ is true, $\varphi^-(x)$ is $\mathbb{N}$-equivalent to a bounded-quantifier formula and $\varphi^+(x)$ isn't.

  • If $\varphi$ is false in $\mathbb{N}$, the situation is reversed: $\varphi^+(x)$ is $\mathbb{N}$-equivalent to a bounded-quantifier formula and $\varphi^-(x)$ isn't.

So the set of formulas which are $\mathbb{N}$-equivalent to a bounded-quantifier formula computes the true theory of arithmetic! (And it's not hard to show that in fact it's Turing-equivalent to the true theory of arithmetic.)