FOL-Proof that "There is no set of all sets."

Question

There a many questions about this Theorem: There is no set of all sets. But I have not found a proof of it using first-order logic. I follow the Textbook Ciesielski, 1997, that has a proof with plain English.

My understanding: If we define $\varphi(x)=\neg(x\in x)$, and we apply the schema of separation: $\forall z\exists y\forall x[x\in y\Leftrightarrow (x\in z\land \varphi(x))]$, we should get some contradiction.

Is my understanding correct? Is the proof difficult?

I studied the rudiments of Propositional Logic (incl. Soundness and Completeness), but for FOL I just finished the syntax.

EDIT 1

Ciesielski introduce the Theorem above with the following words: An interesting consequence of the comprehension scheme [meaning the schema of separation as synonym] axiom is the following theorem. Is he wrong?

Answer 1

Here is a formal proof in Fitch:

Answer 2

This is just Russell's paradox. Suppose there were a set of all sets, $U$. By separation, we get $$R=\{x\in U: x\not\in x\}.$$ Since $U$ contains all sets, we have that the "$\in U$" can be omitted: $$R=\{x: x\not\in x\}.$$ That is, we have

$\forall x(x\in R\iff x\not\in x)$.

But now consider taking $x=R$: we get $R\in R\iff R\not\in R$, which is a contradiction.

---

To formalize this in first-order logic, here are the key things you'll need to prove:

• $\forall x\exists y\forall z(z\in y\iff z\in x\wedge z\not\in z)$. This is an instance of separation: "for each set $x$, the set $\{z\in x: z\not\in z\}$ is a set."

• $\forall x[\forall y(y\in x)\implies \forall y((\forall z(z\in y\iff z\in x\wedge z\not\in z))\implies (\forall z(z\in y\iff z\not\in z)))]$. Basically, if $x$ is the universal set then the set of elements of $x$ not containing themselves is in fact the set of all sets not containing themselves.

• $(\exists x\forall y(y\in x))\implies (\exists x\forall y(y\in x\iff y\not\in y))$. If there is a set of all sets, then there is a set of all sets not containing themselves.

• $\forall x[(\forall y(y\in x\iff y\not\in y))\implies (x\in x\iff x\not\in x)]$. If there is a set of all sets not containing themselves, we get a contradiction.

No particular step here is hard, but if you're really doing a completely formal deduction it will be a bit tedious. The key bulletpoint is the second one (the first is an immediate application of separation, the third follows from the first and second, and the fourth is just unwinding the definitions). The second bulletpoint is intuitively true since, if $x$ is a universal set, then the formulas "$z\not\in z$" and "$z\in x\wedge z\not\in z$" are equivalent; now you need to figure out how to put that equivalence "inside" some quantifiers in the appropriate way.