Sufficient Condition for Defining $\in$

Question

Consider the first order language $\mathcal{L}=\{\in,\in'\}$ with two binary relational symbols $\in , \in'$ and $ZFC$ as a $\{\in\}$-theory. If we define $\in'$ using $\{\in\}$-formula $\varphi(x,y)$ it is clear if there is an elementary embedding $j:\langle V,\in'\rangle\longrightarrow \langle V,\in'\rangle$ which doesn't preserve $\in$ then there is no definition for $\in$ using a $\{\in'\}$-formula like $\psi(x,y)$ within $ZFC$ otherwise for all $x,y\in V$ we have:

$x\in y\leftrightarrow \psi(x,y)\leftrightarrow \psi(j(x),j(y))\leftrightarrow j(x)\in j(y)$

that means the $\in'$-elementary embedding $j$ preserves $\in$ too. A contradiction. Thus:

If $\in$ is definable using $\in'$ then all $\in'$-elementary embeddings of the universe preserve $\in$.

Question. Is the above condition sufficient for defining $\in$ using $\in'$? Precisely, is the following true?

For all $\{\in\}$-formula $\varphi(x,y)$, if the binary relation $\in'$ is defined by $\varphi(x,y)$ and all elementary embeddings $j:\langle V,\in'\rangle\leftrightarrow \langle V,\in'\rangle$ preserve $\in$ then there is $\{\in'\}$-formula $\psi(x,y)$ such that

$ZFC\cup\{\forall x\forall y~(x\in' y\leftrightarrow \varphi (x,y))\}\vdash \forall x\forall y~(x\in y\leftrightarrow \psi (x,y))$

Answer 1

The answer is basically "No". Consider the universe $\omega=\{0,1,2,\dots\}$ with $\in=<$. Let us define $$x\in' y\leftrightarrow x\in y\wedge \neg\exists z(x\in z\wedge z\in y).$$ Then any embedding preserving $\in'$ preserves $\in$. In fact $j$ would have to be given by $j(x)=x+c$ for some constant $c$. However, $x\in' y\leftrightarrow y=x+1$, and $<$ on $\omega$ is not first-order definable from successor.

The underlying idea is that, under your assumptions, $\in$ should be definable from $\in'$ in some very powerful language, but not necessarily in first-order logic.

It is a little harder to consider models of set theory rather than just $(\omega,<)$, since models of set theory cannot be described as explicitly, but the main idea is the same.

Answer 2

$ \newcommand\ZFC{\text{ZFC}} \newcommand\HOD{\text{HOD}} \newcommand\Ord{\text{Ord}} $

I like this question. Here are some set-theoretic counterexamples, which may be closer to what you are thinking about than Bjorn's nice example.

Theorem. Assume ZFC + V=HOD plus $V\neq L$ plus $0^\sharp$ does not exist; that is, in $\langle V,\in\rangle$. Then there is a definable relation $\in'$ on $V$ such that $\langle V,\in'\rangle$ has no nontrivial elementary embeddings, yet $\in$ is not definable from $\in'$.

Proof. Since V=HOD, it follows that there is a definable bijection of $V$ with $\Ord$, and also of $\Ord$ with $L$. Thus, we get a definable bijection $\pi:V\to L$. Define $x\in' y\leftrightarrow \pi(x)\in \pi(y)$, so that $\pi$ is a definable isomorphism of $\langle V,\in'\rangle$ with $\langle L,\in\rangle$. Since $0^\sharp$ does not exist, it follows that there are no nontrivial $\in'$-elementary embeddings $j:V\to V$, since there are no nontrivial $\in$-embeddings $j:L\to L$. But meanwhile, $\in$ is not definable from $\in'$ in $V$, since if it were, we could run the definition inside $\langle L,\in\rangle$ to recover a copy of $V$, which is impossible as this would give us access in $L$ to sets in $V$ that are not in $L$. QED

The argument can be generalized to other inner models $K$ rather than $L$, using the appropriate sharps, and indeed, we can avoid the sharp issue entirely with the following:

Theorem. Every model $V$ of ZFC has a class forcing extension $V[G]$ in which there is a definable relation $\in'$, such that $\langle V[G],\in'\rangle$ admits no nontrivial self-embeddings and $\in^{V[G]}$ is not definable from $\in'$ from parameters.

Proof. Let $V[G]$ be a nontrivial extension of $V$ satisfying $V=\HOD$, obtained by the usual progressively closed iteration. It follows that $V$ is a definable class in $V[G]$, and we may actually arrange that this definition does not require parameters. Thus, the extension has a definable bijection $\pi:V[G]\to V$, and we may define $x\in' y\iff \pi(x)\in \pi(y)$. Thus, $\pi$ is an isomorphism of $\langle V[G],\in'\rangle$ with $\langle V,\in\rangle$. This forcing extension $V[G]$ can have no nontrivial elementary embedding $\langle V,\in\rangle\to\langle V,\in\rangle$, and hence no nontrivial elementary self embedding of $\langle V[G],\in'\rangle$. Yet, $\in^{V[G]}$ is not definable from $\in'$, even with parameters, since if it were, we could run the definition inside $\langle V,\in\rangle$, with $\pi$ of the parameters, and thereby get access to the sets of $V[G]$ from $V$ itself, which is impossible. QED