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?

  • 2
    $\begingroup$ $\psi$ is not a single formula. The term $\neg \phi_x(x)$ is effectively a different formula for every $x$. I suspect this has something to do with it - in particular I think some form of diagonalization-like reasoning will show that $\psi(x)$ is not such a $\phi_k$. $\endgroup$ Oct 30, 2018 at 0:49
  • $\begingroup$ What is your definition of 'formula'? Since you're talking about a formal logical result, a naive definition that a formula is just a string of symbols isn't sufficient here... $\endgroup$ Oct 30, 2018 at 0:50
  • 3
    $\begingroup$ There's a language/metalanguage mixup going on here. The you're using a variable of your metalanguage (the $x$ that ranges over natural numbers) as a variable of your object language, which is just plain mischief. $\endgroup$ Oct 30, 2018 at 0:55
  • 1
    $\begingroup$ Suppose $\varphi$ was a lexicographical enumeration of unary formulas. What would $\psi$ look like? How many symbols long would it be? $\endgroup$
    – DanielV
    Oct 30, 2018 at 1:06
  • 2
    $\begingroup$ This is pretty close to Richard's paradox -- in fact arguably it is Richard's paradox, given the usual set-theoretic convention that identifies "real number" with "subset of $\omega$" -- at least as long as you're not giving a specific argument for how "$\varphi_x(y)$" is supposed to be a concrete formula in the language of set theory with free variables $x$ and $y$. $\endgroup$ Oct 30, 2018 at 1:19

3 Answers 3


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.


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.

  • $\begingroup$ Not done yet. He appears to have k∈ω and (φk(k) holds or φk(k) doesn't hold) which is just as bad. $\endgroup$
    – Joshua
    Oct 30, 2018 at 15:50
  • $\begingroup$ @Joshua They just need the “doesn’t hold” part to express $\psi,$ but in any event I got that backwards. Fixed it, thanks. $\endgroup$ Oct 30, 2018 at 16:51

"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$.

  • 2
    $\begingroup$ The first line is really on the nose. So many people find "inconsistency proofs" (whether seriously, or just to see if they understood some concept), which are in fact proofs about the inconsistency of some weak arithmetic theory. The proof that $\omega=\omega+1$ can be usually adapted to prove that $n=n+1$ for some $n<\omega$. But people forget to look closely as to how much of ZFC they actually used in the proof. $\endgroup$
    – Asaf Karagila
    Oct 30, 2018 at 7:12
  • $\begingroup$ @AsafKaragila: Thanks! The 'proof' that $ω=ω+1$ is a new one for me. Do you have a recent example of such a 'proof' that isn't just a crank post? =) $\endgroup$
    – user21820
    Oct 30, 2018 at 15:22
  • 1
    $\begingroup$ Of course not. But it's a story I heard from a colleague who was an editor of a prominent logic journal. He received a submission of a paper claiming that they proved that $\omega=\omega+1$, and therefore transfinite ordinals are poppycock. The editor then replied that the methods of the proof can be used to show that for some finite $n$, in fact, $n=n+1$ and the result should be submitted to a number theory journal as they would be very interested in such result. :-) $\endgroup$
    – Asaf Karagila
    Oct 30, 2018 at 15:24
  • $\begingroup$ Hahaha! Very nice. Edward Nelson would be pleased. =) $\endgroup$
    – user21820
    Oct 30, 2018 at 15:25
  • 1
    $\begingroup$ @AsafKaragila That's evil, I love it. (My favorite bunk proof was showing that the Riemann Hypothesis held by (1) giving a ZFC proof of a zero off the line, (2) establishing a contradiction in ZFC, and then (3) concluding that this means RH does hold. It was glorious. And, needless to say, the technique was under-utilized. :P) $\endgroup$ Oct 30, 2018 at 17:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .