This is a "proof" that ZFC is inconsistent, but I haven't found the mistake yet.
Let $\{\varphi_n \colon n <\omega\}$ be an enumeration of all formulas in $L_{\in}$ with exactly one free variable. Consider the formula
$$\psi(x) \equiv x \in \omega \land \lnot \varphi_x(x) \, .$$
Since $\psi$ is a formula with one free variable, then $\psi$ is $\varphi_k$ for some $k$. But then,
$$\mathrm{ZFC} \vdash \varphi_k(k) \leftrightarrow \psi(k) \leftrightarrow \lnot \varphi_k(k)$$
I have been giving this a lot of time, but I still cannot figure out the error on the fake proof here. Can anyone give me a clue?
Best Answer
The issue is there's no way to write $\varphi_n(x)$ uniformly in ZFC via a single formula $\phi(n,x)$. If you wanted a way to enumerate the unary formulas of $L_\in$ in ZFC then they won't be in the representation you want here, rather they'd be in the form of Godel numbering. Then if ZFC could prove the schema $\mathsf{Prov}(\lceil\varphi_n\rceil)\to\varphi_n$ for each $n$ then it would indeed be inconsistent. This all holds for far weaker than ZFC as well.