# Goedelizability and decidability of a property of Peano formulas

Sorry for not knowing the answers to these elementary questions:

Is the property of formulas of the first-order language of Peano arithmetic of "defining a finite set of natural numbers" goedelizable?

If so: Is the set of formulas with this property decidable, semidecidable or non-decidable?

-
By finite do you mean provably bounded, i.e. $PA \vdash \exists b\forall x(\phi(x) \to x \leq b)$? Or do you mean something stronger? –  François G. Dorais Feb 4 '10 at 23:46
By looking at your formula I am quite sure that I mean "provably bounded". But what might be stronger? –  Hans Stricker Feb 5 '10 at 0:03
"If this property was goedelizable and if there was a constructive proof that this property is decidable: one would not have to look for a specific proof for - e.g. - that there are infinitely many primes." Is this a correct line of reasoning? –  Hans Stricker Feb 5 '10 at 0:09
@Francois: Please forget about my last comment: you just showed that the property is NOT decidable, so what about infinite primes? –  Hans Stricker Feb 5 '10 at 0:50
Hans, this is the kind of focused and precise question that is good to make on MO. –  Joel David Hamkins Feb 5 '10 at 2:50
show 1 more comment

The set of (Gödel codes for) PA provably bounded formulas $\phi(x)$ is computably enumerable (c.e.). By provably bounded, I mean PA $\vdash \exists b\forall x(\phi(x)\to x \leq b)$. Indeed, you can enumerate all consequences of PA and when you find one of the shape $\exists b\forall x(\phi(x)\to x \leq b)$ then enumerate $\phi(x)$.

You can't do better than that since you can easily reduce the halting problem to the decision problem for the set of PA provably bounded formulas. Consider the formula $\phi_T(x)$ which says "the Turing machine $T$ (with blank input) has not halted after $x$ steps," with the usual arithmetic coding of Turing machines. Then PA proves that $\phi_T(x)$ is bounded if and only if $T$ truly halts in finite time.

Thus, the set of PA provably bounded formulas is a complete c.e. set.

-
Sorry, I do not understand the second part of your answer: on which input didn't the Turing machine T halt after x steps? –  Hans Stricker Feb 5 '10 at 0:16
It doesn't really matter, but I was assuming blank input. (If you prefer, you could also enumerate all possible combinations of machines and inputs.) –  François G. Dorais Feb 5 '10 at 0:22
While trying to understand your answer (second half of), I truly admire your ease of thinking this way! –  Hans Stricker Feb 5 '10 at 0:23
Do I understand correctly: The property of "defining a provably bounded set of natural numbers" is NOT decidable, but the set of such formulas is - almost trivially - enumerable? –  Hans Stricker Feb 5 '10 at 0:37
Yes, you understand correctly. In fact, I proved a stronger statement that the set of provably bounded formulas is a complete c.e. set, just like the halting set. –  François G. Dorais Feb 5 '10 at 0:40