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?
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.
Francois has fully answered the question about the formulas phi(x) that PA proves to define a finite set, and I agree completely with what he said.
It is also natural, however, to consider which formulas phi(x) define a finite set in the standard model of arithmetic.
Here, the situation is even worse. The set of (codes for) formulas phi(x) that define a finite set in the standard model is not decidable, not enumerable, not co-enumerable, not computable from the halting problem nor computable even from finitely many iterations of the halting problem. This set is not definable by any arithmetic formula. To see this, suppose that it were. Suppose there were a formula F, such that F('phi(x)') was true iff phi(x) defined a finite set. Note that as a special case, when phi(x) is a sentence whose truth does not depend on x, then the set { n | phi(n) is true in N } is either everything or empty, depending on whether the sentence is true or false in N, the standard model. Thus, for a sentence phi, the formula ¬F('phi') is true if and only if phi is true. Thus, F provides a definable truth predicate, but this is exactly ruled out by Tarski's theorem on the non-definability of truth. The proof of this is to use the fixed-point lemma to find a sentence psi such that PA proves (F('psi') iff psi). Thus, psi asserts "I am not true", and this easily gives a contradiction.
