Consider the usual language $\mathcal{L}=(\in, \mathrm{st})$ of Nelson's Internal Set Theory, and a unary $\mathcal{L}$-predicate $P$. For an $\mathcal{L}$-formula $\varphi$, let $\varphi^P$ denote the formula obtained from $\varphi$ by replacing each occurrence of $\mathrm{st(-)}$ with $P(-)$.
Call the predicate $P$ a pseudo-standard predicate if for any IST axiom $\varphi$ we have $IST \vdash \varphi^P$ as well. Basically, a pseudo-standard $P$ satisfies all the same axioms as the predicate $\mathrm{st}$, as far as the theory IST is concerned.
Question
Can we define a pseudo-standard $\mathcal{L}$-predicate $P$ such that
- I. $\forall x. \mathrm{st}(x) \rightarrow P(x)$ is not provable in IST;
- II. $\forall x. P(x) \rightarrow \mathrm{st}(x)$ is not provable in IST;
- III. neither of the above are provable in IST?
Motivation
This question arises from an interest in how well the IST axioms characterize the standardness predicate $\mathrm{st}$. Between 2016 and 2019, I posed this general question to various audiences, including after my thesis viva, but if anyone has worked out an answer, that answer hasn't reached me yet. Given that the question is related to a discussion under a recent answer of Joel David Hamkins, the timing feels right to ask it again. I hope that this particular concretization of the general question is sufficient to avoid trivial solutions (such as solutions of the form $\mathrm{st}(x) \wedge Q$ for some $\in$-sentence $Q$), but I'll be grateful for refinements in case it does not fully succeed in doing so.
