[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

naturaliff 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

couldbe 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$