Models of ZF + Reinhardt (Final part to series of questions) So, in the previous question, I got an answer to what the minimum requirement for an inner model of the existence of a Reinhardt is due to Andrés E. Caicedo. However, I did not get an answer to the first question I asked, most likely because I didn't show the information required to complete it.
So, here is my "proof" that $0^{\#}$ can't exist:
Let $j:L\rightarrow L$ be a nontrivial elementary embedding.
It is said that the existence of a nontrivial elementary embedding from $V$ to itself can be expressed as a first-order theory with an added constant symbol $j$. However, I could not find this theory. So, I attempted to create my own. I believe this is why the proof fails.
I asserted that $M$ a standard transitive model of ZF satisfies the existence of such an embedding iff there is some $f:M\rightarrow M$ such $\langle M;\in, f\rangle$ satisfies the following schema:


*

*$\exists x(f(x)\neq x)$

*For every formula $\varphi$ which does not contain a function symbol:


*

*$\forall x(\varphi(x)\Leftrightarrow\varphi(f(x)))$

*$\forall x_0,x_1(\varphi(x_0,x_1)\Leftrightarrow\varphi(f(x_0),f(x_1)))$

*...

*$\forall x_0,x_1...x_n(\varphi(x_0,x_1...x_n)\Leftrightarrow\varphi(f(x_0),f(x_1),...f(x_n)))$

*... 



So, let's check if this holds for $\langle L;\in,j\rangle$:


*

*$j$ is nontrivial, so $\exists x\in L(j(x)\neq x)$ by definition of nontriviality. Of course, this is equivalent to $\langle L;\in,j\rangle\models\exists x(f(x)\neq x)$. So, $\langle L;\in,j\rangle$ satisfies this.

*Let $\varphi$ be a formula which does not contain a function symbol.


*

*Because $j$ is elementary: $$\forall x\in L(L\models\varphi[x]\Leftrightarrow L\models\varphi[j(x)])$$ 
$$\forall x\in L(L\models(\varphi[x]\Leftrightarrow \varphi[j(x)]))$$
$$\forall x\in L(\langle L;\in,j\rangle\models(\varphi(x)\Leftrightarrow \varphi(f(x))))\text{ because }f\text{ is interpreted as }j $$
$$\langle L;\in,j\rangle\models\forall x\in L(\varphi(x)\Leftrightarrow\varphi(f(x)))$$

*This could be shown to hold for more quantification with the same method.



Therefore, it seems as though $L$ satisfies the existence of a nontrivial elementary embedding, which is obviously false. Where am I wrong? If I am wrong because I stated the scheme incorrectly, why?
 A: You are quite right: the problem is when you define the theory in question. You show that $(L; \in, j)$ is a (fine, proper class) model of a certain theory, and then claim that that is the theory Kunen showed was inconsistent; but the problem is that the theory Kunen showed was inconsistent was not just "ZFC + $j$ is an elementary embedding."
The actual first-order theory (call it "ZFC$_{elem}$," I don't know if it actually has a name) that Kunen showed is inconsistent is much stronger than what you've written, the difference being the extension of the separation/replacement schemes to include formulas in the new language (that is, including the added function symbol). Going back to the usual Kunen inconsistency, we see that we can't have $\{j(\xi): \xi<\lambda\}$ (where $\lambda=j^{(\omega)}(crit(j))$ is the first $j$-fixed point above the critical point) be an element of $L$, so $(L; \in, j)$ does not satisfy the separation scheme for formulas with $j$ as a parameter.
Note that this is exactly the amenability issue raised in your previous question, I'm just phrasing it here in terms of the axioms of the theory involved since I think that might be clearer.
Here's the precise definition of ZFC$_{elem}$ and statement of the "first-order Kunen inconsistency":

Let $\Sigma=\{\in, f\}$ be a language gotten by adding a unary function symbol to the language of set theory. Let ZFC$^f$ be the theory in this language consisting of: (i) the usual ZFC axioms, (ii) a scheme (as you've written) asserting that $f$ is an elementary embedding from the universe to itself, and (iii) expanded replacement/separation schemes covering all formulas in the expanded language. Then ZFC$_{elem}$ is inconsistent.

So if you could get a model of ZFC$_{elem}$ from the assumption that $0^\sharp$ exists, then you would indeed have disproved the existence of $0^\sharp$; however, the structure $(L;\in, j)$ is not a  model of ZFC$_{elem}$ since it doesn't satisfy the expanded separation/replacement schemes (part (iii)).

As an aside, what I've written above is overkill; Kunen needed much less than the full separation/replacement schema extended to the new language. But there's no reason to go into that at the moment.
