Definition and decidability of bounded quantifiers

Question

Consider quantifier-free formulas $P(x,y) = Q(x,y)$ of Peano arithmetic.

Consider $P(x,y),Q(x,y)$ to be terms composed of variables $x,y, \operatorname{succ}, +, \times$.

Note that these are equivalent with polynomials $P(x,y),Q(x,y) \in \mathbb{Z}_+[x,y]$.

Let $R(x)$ be correspondingly a term, resp. a polynomial in $\mathbb{Z}_+[x]$.

The quantifier of a formula $(\exists y)\ P(x,y) = Q(x,y)$ is bounded if there is a polynomial $R(y)$ such that

$$(\forall x)\Big(\big( (\exists y)\ P(x,y) = Q(x,y) \big) \rightarrow \big( y \leq R(x) \big)\Big)$$

which is equivalent with

$$(\forall x)\Big(\big( (\exists y)\ P(x,y) = Q(x,y) \big) \rightarrow \big((\exists z)\ y + z = R(x)\big)\Big)$$

which is a pure PA sentence again.

(Note that the righthand side of $\rightarrow$ is a only a shorthand!)

I wonder:

• Is this the correct definition of a bounded quantifier?

• Has the defining sentence to be true or provable?

• Is the property of a sentence to have a bounded quantifier decidable?

Answer 1

Is this the correct definition of a bounded quantifier?

I would say you are talking about "boundable" existential quantifiers, rather than bounded quantifiers.

It is true that terms in Peano arithmetic are polynomials, so in the language of Peano arithmetic if we have a bounded quantifier $(\exists x < t(y)) R(x,y)$ then $t(y)$ is a polynomial in $y$.

You have defined what it means to be able to replace the existential quantifier in $(\forall y)(\exists x)R(x,y)$ with a bounded quantifier.

Has the defining sentence to be true or provable?

You will get two different notions depending whether you want to defining sentence to be true or provable. This follows from the next answer.

Is the property of a sentence to have a bounded quantifier decidable?

No. Let $P(y)$ be any formula with one free variable $y$. Let $S(x,y)$ be a formula such that it is satisfied only when $x = 2^y$. Let $R(x,y)$ be $$[x = 0 \land (\forall z < y) P(z)] \lor [S(x,y) \land (\exists z < y)\lnot P(z)].$$

Note that $(\forall y)(\exists x)R(x,y)$ holds, provably in PA. But the quantifier is boundable (by a polynomial) if and only if $(\forall y)P(y)$ holds. And the quantifier is provably boundable if and only if $(\forall y)P(y)$ is provable. In general, the latter two are not equivalent.

Answer 2

In general, a bounded quantifier is the abbreviation of a "standard" first-order formula like :

$\forall x (Px \rightarrow Qx)$

which we can abbreviate in slightly different forms according to the contexts :

• set theory : $\forall x \in P : Qx$, which is : $\forall x(x \in P \rightarrow Qx)$;

• (formal) arithmetic : $\forall x \le n : Qx$, which is : $\forall x (x \le n \rightarrow Qx)$.

Thus, if we consider the second case, we can "unwind" it as :

$\forall x (\exists y (n = x +y)\rightarrow Qx)$.