First-order formula in first-order language, another open language where equivalence true on the naturals?

Question

For any first-order formula $X$ in the first-order language $\langle 0, S, \le\rangle$ (possibly with free variables) does there necessarily exist another open formula $Y$ such that the equivalence $X \equiv Y$ is true on the set of all nonnegative integer numbers?

Answer 1

Yes, this is true. The structure $(\mathbb{N}; 0, S, \le)$ admits quantifier elimination, and the proof of this is via induction on the complexity of $X$. For an example of such a proof, see this, which goes through the proof of quantifier elimination for a version of Presburger arithmetic.