Where is the mistake in this "proof" of the inconsistency of ZFC?

Solution 1:

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.

Solution 2:

As others have suggested, the key is to think about how we would actually go about writing down the predicate $\psi(x)$ in $L_\in$. It is not as straightforward as you make it out to be. For instance, if $\varphi_0$ is $x=x$ and $\varphi_1$ is $\forall y(y\in x),$ we would want $\varphi_0(0)$ to be $0=0$ and $\varphi_1(1)$ to be $\forall y(y\in 1).$ It is clear that these aren't just two instances of some formula $\psi(x)$ with $0$ and $1$ plugged in for $x$, respectively. You have confused the "$n$" in $\varphi_n$ with the integer in the formal theory. Really, this $n$ is from an enumeration we have created on the outside (i.e. in the metatheory), talking about the language, not in it.

So the best you can hope for is to write something equivalent within $L_\in,$ through formalization of syntax (i.e. coding formulas as sets). You can certainly formalize and enumerate the one-variable formulas of $L_\in,$ and you can also formalize the operation of substituting of a set parameter for a variable. So far so good, but to finish, you need to write down a sentence that means "$k\in\omega$ and $\varphi_k(k) $ does not hold."

It's the "$\varphi_k(k)$ does not hold" part that is problematic. It requires that you have a truth predicate that will take a code for a sentence and tell you if it holds or not. In fact, another way of looking at what you've written is as a proof that this truth predicate cannot be expressed in $L_\in$. This is a version of Tarski's theorem.

Edit: In line with what others have pointed out, Tarski’s theorem is not particular to set theory. In fact, your fake proof only uses one small aspect of ZFC: that it can represent numbers. So it could just as well be a fake proof of the inconsistency of PA. Turning this fake inconsistency proof into a real proof of Tarski’s theorem just requires some formalization of syntax, as I outlined, and a closer look will show you that you don’t need to express or prove very much about arithmetic to make it work.

Solution 3:

"ZFC" is a red herring. $ \def\eq{\Leftrightarrow} \def\nn{\mathbb{N}} $

Take any first-order theory $S$, and any $2$-parameter sentence $P$ over $S$. Let $Q(x) :\equiv \neg P(x,x)$. Then $Q$ is a $1$-parameter sentence and $S$ trivially proves "$\forall y \exists z ( \neg Q(z) \eq P(y,z) )$". Now observe that if $S$ has a countable language and also has a countable set $T$ of provably distinct terms, then all $1$-parameter sentences over $S$ can be enumerated and put in bijection with the interpretation of $T$ in any model of $S$. However, the above fact shows that no $2$-parameter sentence over $S$ can capture any such enumeration, despite $T$ appearing to provide sufficiently many objects!

For example, no $2$-parameter sentence $P$ over PA represents (in the above sense) an enumeration of all $1$-parameter sentences $X$ over PA, despite there being a concrete bijection between the terms $N = \{``$1$", ``$1+1$", ``$1+1+1$", \cdots \}$ and $X$. Furthermore, there is a computable bijection $r$ from $N$ to $X$, and hence we can in fact explicitly construct a $2$-parameter sentence $R$ over PA such that for every $t \in N$ and $Q \in X$ we have that $\text{PA} \vdash R(c(t),c(Q))$ if $r(t) = Q$ and $\text{PA} \vdash \neg R(c(t),c(Q))$ if $r(t) \ne Q$. What we do not have is a $2$-parameter sentence over PA that attains the truth values of an enumeration of $X$.

I call this phenomenon a syntactic version of Cantor's theorem, because Cantor's theorem says there is no countable enumeration of functions from $\nn$ to booleans, and here we have proven that there is no 'syntactic' enumeration of predicates over $S$.