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?



Goedelizability and decidability of a property of Peano formulas
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.


