Let $\Gamma$ and $\Delta$ be theories in the language of set theory (LST), and let $M = \{x: \phi(x)\}$ be a class, where $\phi(x)$ is some formula of LST. Let us say that $M$ is a (standard) class model of $\Gamma$ in $\Delta$ if and only if $\Gamma \vdash \psi$ implies $\Delta \vdash \psi^M$ for all sentences $\psi$ of LST, where $\psi^M$ denotes the relativization of $\psi$ to the class $M$. I'm curious about what can be said of proper class models $M$ of ZF in ZF such that $\mbox{ZF} \vdash \forall x (x \in M \rightarrow \phi^M(x)$), i.e., $\mbox{ZF} \vdash \forall x (\phi(x) \rightarrow \phi^M(x))$.


A class $M = \{x: \phi(x)\}$ satisfying $\forall x (\phi(x) \rightarrow \phi^M(x))$ could be said to be "contained in its self-relativization." Using Definition I.16.5 from Kunen's set theory book (2013), the statement $\forall x (\phi(x) \rightarrow \phi^M(x))$ (i.e., $(\forall x \, \phi(x))^\phi)$) holds if and only if $\phi$ is absolute for $\{x:\phi(x)\}$, written $\{x: \phi(x)\} \preceq\_\phi V$.


Examples of such proper class models of ZF satisfying this self-relativization property are $V$ and $L$ (and both satisfy the stronger condition $\mbox{ZF} \vdash \forall x (\phi(x) \leftrightarrow \phi^M(x)$). Note also that the canonical inner models $L[0^\sharp]$, $L[\mu]$, etc., are transitive class models of ZF that satisfy the self-relativization property, but their consistency strength is well beyond that of ZF.


My questions are as follows. What are some other interesting examples and non-examples? Am I correct in thinking that HOD is a non-example? Are there examples besides $V$ and $L$ whose existence is equiconsistent with ZF? And is there an example that is non-transitive?


One interesting thing about such class models $M$ of ZF in ZF is that ZF does not refute $V = M$ if ZF is consistent, for if $\mbox{ZF} \vdash \neg \forall x (\phi(x))$, then $\mbox{ZF} \vdash \neg \forall x (x\in M \rightarrow \phi^M(x))$, and therefore $\mbox{ZF} \nvdash \forall x (x \in M \rightarrow \phi^M(x))$, assuming ZF is consistent. This is what piqued my interest in the question. Also, one of the comments points out that, if ZF proves that $M$ is non-transitive, then ZF refutes $V = M$. Thus, if there is a non-transitive example, then ZF cannot prove that it is non-transitive. But could there be one that isn't transitive according to a theory stronger than ZF? (Maybe no such theory would be very natural or attractive.)



What are some further examples of proper class models of ZF that are contained in their own "self-relativization"?
Let $AC$ stand for the axiom of choice, let $L$ denote the constructible universe and let $L^\*$ the universe of constructible sets transitively containing $\emptyset$ as an element.
Although $L^\*$ is a proper subclass of $L$, it collapses to $L$, so it is isomorphic to $L$.


Let $\phi(x)$ be the formula


* $(AC\rightarrow x\in L)\wedge(\neg AC\rightarrow x\in L^\*)$.


I claim that the corresponding class $M$ is a model of $ZFC$ in $ZF$. In fact, $M$ is either $L$ or $L^\*$, so it is a model of $ZFC$ in any case.
(This argument can be made precise: $ZF\vdash AC\rightarrow (\psi^M\leftrightarrow \psi^L)$ and $ZF\vdash \neg AC\rightarrow (\psi^M\leftrightarrow \psi^{L^\*})$, for any $\psi$. Therefore $\psi^M$ holds for all $ZFC$ axioms).


Now, I claim that $M$ is self-relativizing. Indeed, $ZF\vdash AC^M$, so $ZF\vdash \phi(x)^M\leftrightarrow (x\in L)^M$. But $L^M$ is $M$ in both cases, because $M$ is either $L$ or $L^\*$, and $L^\*$ is isomorphic to $L$. Therefore, $ZF\vdash \phi(x)^M\leftrightarrow \phi(x)$.


Finally, $ZF$ cannot prove that $L\subseteq M$, and $ZF+\neg AC$ proves that $M$ is a proper sublass of $L$.


