Naturally definable sets of natural numbers (3)

Question

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

Answer 1

I think my answer here to your first question along this line seems largely to apply to this version as well. Since you have the word "equivalent" in the latter part of your definition of natural, I find it ambiguous unless you state precisely what you mean there. I think that you mean provably-equivalent-in-PA, as you used that concept in the earlier part of your definition, although another natural interpretation would be equivalent-in-the-standard-model.

If you mean provably-equivalent-in-PA, then I had pointed out that you will not be able to prove in PA that any particular formula is natural, including the example that you gave(!). The reason is that on this interpretation, the naturalness of a formula implies Con(PA). For the same reason, if PA is consistent, it will be consistent with PA, by the Incompleteness Theorem, that there are no natural formulas.

In any case, even if you assume PA is consistent in your meta-theory (while not allowing this assumption to be used in your equivalences), then the question of whether a given formula is equivalent to a finite set is not computable. So you will not in general be able to decide whether a given formula is natural, as Francois and I explaned in your recent question on that point. It is not even computably enumerable, but rather co-enumerable, since it will be the unnatural formulas that are enumerable.

If you mean equivalent in the sense of equivalent-in-the-standard-model, then the question of whether a given formula defines a finite set is not computable, nor even arithmetically expressible, as I mentioned in my answer to another of your questions here. Thus, the question of naturality here will be even worse than non-computable.