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?
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":
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.