Followup question on first-order formulas in first-order languages and open formulas. This is a followup question to my question here. I will reproduce the contents of my original question as follows.

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?

Noah Schweber gives the following answer here, which I will reproduce as follows.

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.

My new question is, does a similar statement hold for the language $\langle 0, \le\rangle$?
 A: No, it does not. The set $\{1\}$ is definable in that structure - it is the set of $x$ such that $$x\not=0\wedge \forall y(y\le x\implies [y=0 \vee y=x]).$$ However, it's not hard to show that it is not definable by a quantifier-free formula (there aren't very many sets which are definable by a quantifier-free formula in this structure; see if you can find them all, and prove that your list is exhaustive!). Roughly speaking, the reason is that this language does not have enough terms. 
Incidentally, note that the successor function is definable in this language ($S(x)=y$ iff $x\le y$ and $\neg y\le x$ and $\forall z[x\le z\wedge z\le y\implies x=z\vee z=y]$); combining this with the observation from the previous question that $(\mathbb{N}; 0, \le, S)$ does have quantifier elimination, we get two interesting facts:


*

*Definable expansions of theories without quantifier elimination might "gain" quantifier elimination. (By contrast, it's not hard to show that once you have quantifier elimination, you don't lose it by passing to a definable expansion.)

*Since the successor function is definable by a formula with one quantifier, every definable relation on $(\mathbb{N}; 0, \le)$ is definable by a Boolean combination of existential formulas; so, while we don't have full quantifier elimination, the quantifier hierarchy does collapse - just not right away.
