mjhjmtu

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,
$$mathrmZFC 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?

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 $mathsfProv(lceilvarphi_nrceil)tovarphi_n$ for each $n$ then it would be indeed be inconsistent. This all holds for far weaker than ZFC as well.

As others have suggested, the key is to think about how we would actually go about writing down the predicate $psi(x)$ in the language of set theory. The "$n$" in $varphi_n$ is in the metatheory, so on its face, you really can't.

The best you could hope for is to write something equivalent to this, through formalization of syntax. You can certainly formalize and enumerate the one-variable formulas of $L_in$ in set theory, and formalize the substitution of a set parameter for a variable. Then you want to write something like "$kinomega$ and $varphi_k(k) $ holds."

It's the "$varphi_k(k)$ holds" part that is problematic. It requires we have a truth predicate that expresses the notion of a sentence holding. So another way of looking at what you've written is as a proof that a truth predicate does not exist. This is Tarski's theorem.