lo.logic - Naturally definable sets of natural numbers (3)

[This shall be the last of a series of questions, see Naturally definable sets of natural numbers (2)]

I cannot explain why I have been so stubborn not to see the most straight-forward definition for naturalness, sorry for the confusion I have caused. (In any case I guess I have learned a lot from previous answers!)

Let $Phi(x)$ be a formula of the first-order language of Peano arithmetic (PA).

Definition: A formula $Phi(x)$ is
natural iff it is provably-equivalent-in-PA to a formula $phi(x)$ in prenex disjunctive normal form with its matrix not containing clauses of which the disjunction is
equivalent [corrected:] provably-equivalent-in-PA to some $p(x) = q(x)$ with
$p(x), q(x)$ polynomials in $x$ with
natural coefficients.

The last condition means "clauses of which the disjunction defines a finite set", thus "adding" an arbirtrary finite set. There must by the way be an analogue condition on the matrix of the prenex conjunctive normal form, which must not contain conjunctive clauses that are equivalent to some $p(x) neq q(x)$, thus "excluding" an arbitrary finite set.

There definitely are natural formulas, e.g. $(exists y) x = 2 cdot y$.

Consider a formula that is not in this form, i.e. its matrix in prenex disjunctive normal form does contain clauses of which the disjunction is equivalent to some $p(x) = q(x)$, e.g. $(exists y) x = 2 cdot y vee x = 17$ Then it is in general not possible to make these clauses disappear by applying logical axioms only. But nevertheless the formula might be natural.

Do you agree

...that the set of natural
formulas is not decidable (but maybe enumerable)?

(Like the set of formulas that define finite sets, see Francois' answer to another question.)

... that nevertheless every formula
which defines an infinite set could be
natural?

Or is there one explicit example of a formula that is provably not natural? I suspect that if (big if) every formula is natural, the formula in the "correct" form (without any clauses equivalent to $p(x)=q(x)$) can be arbitrarily weird.

... that every finite set might be
definable by some natural formula $Phi(x)$ in the form
$lbrace x | Phi(x) wedge bigvee_{k_1 < k_2} n_{k_1} leq x leq n_{k_2} rbrace$