# Is the set of bounded quantified sentences decidable in PA

In the first order theory of $\mathbb N$ with $+$ and $\cdot$ is the set of formulas with bounded quantifiers (universal and existential) decidable, i.e. can we decide for a given such sentence if it is true in the natural numbers or not?

I guess yes: For these sentences are closed under negation, and it is easy to see if an arbitrary expression has this form (syntactically, by giving an appropriate inductive definition of these formulas). So, just enumerate all derivations form the axioms, and as we have $$\mathbb N \models \varphi \mbox{ iff } PA \vdash \varphi$$ for bounded sentences, and $\mathbb N \not\models \varphi$ iff $\mathbb N \models \neg\varphi$, we just look for a given bounded quantifier sentence if it, or its negation occurs among the derived sentences, which will certainly happen at some point.

Is this correct?

• Your reasoning is correct, assuming you already know that '$\mathbb{N} \vDash \varphi$ iff $PA \vdash \varphi$'. Apr 15, 2018 at 22:09
• It is common to refer to such expressions as "strongly representable". plato.stanford.edu/entries/goedel-incompleteness contains some mentions of it, searching through the article for "strongly representable" and "bounded". It is the basis of defining things like $\Sigma_1$ statements. Apr 17, 2018 at 8:55

However, there is an easier way to see that the set of sentences with bounded quantifiers is decidable. It is pretty straightforward to imagine writing a computer program that decides the truth of such a sentence. The bounded quantifiers just become bounded loops (i.e. 'for loops'), which of course always terminate. And then the rest is just that propositional formulae and atomic sentences are decidable. In fact, this was probably the upshot of how you showed that $\mathbb N\models \phi$ iff $PA\vdash \phi.$