Is the set of primes implicitly definable from successor?

Question

An earlier question by Joel David Hamkins asked whether multiplication is implicitly definable in the structure $(\mathbb{N},S)$ of the naturals with successor. Here $R$ is implicitly definable if there is a formula $\phi(\dot{R})$ that is satisfied only if $R = \dot{R}$. Joel's goal was to find a natural counterexample to implicit definability being transitive: $+$ is implicitly definable in terms of $S$, and $\cdot$ is implicitly definable in terms of $+$, and he hoped that $\cdot$ would not be implicitly definable in terms of $S$. Alas, it is, so we need an alternate example.

Question: Is the set of primes implicitly definable in $(\mathbb{N},S)$?

My guess is no, roughly because the set of primes has arbitrarily large gaps with pseudorandom behavior that cannot be captured by $S$ alone. In particular, I would conjecture that given any formula $\phi(P)$ on a predicate $P$ that is satisfied if $P = \textrm{Primes}$, there is some prime $p$ such that $\phi(P - \{p\})$ is true.

If primes is indeed not implicitly definable, it provides a nice counterexample to transitivity. From the earlier question $\cdot$ is implicitly definable from $S$, and primes is explicitly definable from $\cdot$.

Answer 1

The set of primes is not implicitly definable in $(\mathbb{N},S)$. This is immediately implied by following:

Theorem. A unary predicate $P$ on $\mathbb{N}$ is implicitly definable in $(\mathbb{N},S)$ iff $P$ is a finally periodic set of naturals.

Proof. Suppose $P$ is finally periodic, i.e. there are naturals $n$ and $m>0$ such that $\forall x(x\ge n \to x\in P\mathrel{\leftrightarrow} x+m\in P)$. Then $P$ is implicitly definable by the following formula $\varphi(X)$: $$\forall x\Big(X(x)\mathrel{\leftrightarrow}\exists y,z\big( S^{n+m}(z)=x\land S^m(y)=x\land X(y)\big) \lor \bigvee\limits_{k<n+m\text{ and }k\in P}x=S^k(0)\Big)$$

On the other hand if $P$ is implicitly definable in $(\mathbb{N},S)$, then it is definable in $(\mathbb{N},S)$ by a monadic second-order formula. And by the classical result of Büchi a set of naturals has a monadic second-order definition in $(\mathbb{N},S)$ iff it is finally periodic (combination of results from [1] and [2]).QED

[1]Büchi, J. Richard. "Symposium on Decision Problems: On a Decision Method in Restricted Second Order Arithmetic." Studies in Logic and the Foundations of Mathematics. Vol. 44. Elsevier, 1966. 1-11, doi:10.1016/S0049-237X(09)70564-6.

[2]Büchi, J. R. “Weak Second Order Arithmetic and Finite Automata”, Zeitschrift für Math. Log. und Grundl. der Math., 6 (1960), pp. 66–92, doi:10.1002/malq.19600060105.