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.