# Need help with formal proofs of two simple theorems in the language of ZFC?

EDIT: Starting Over

I would like to see a formal proof in the language of ZFC of:

1. $\neg\exists S: \forall x:[x\in S \iff x\notin x]$

2. $\forall S: \exists x: x\notin S$ (added later)

Can someone list the formal proof here if it is not too long, or give me a reference, preferably online?

• What do you mean by a "formal ZFC proof"? (And why do I have the feeling that you're going to post a link to your blog here?) – Asaf Karagila Jun 2 '15 at 19:12
• If it could be translated into ZFC by anybody who has existed since its invention, do you think we'd still be using ZFC? – Thomas Andrews Jun 2 '15 at 19:15
• You have forgotten the leading existential quantifier; thus the proof must conclude with : $\lnot \exists y \forall x ( x \in y \leftrightarrow x \notin x)$. As you have showed it is provable in f-o logic with the binary predicate $\in$. Per se it is not "paradoxical" att all... unless you consider the "naive" Comprehension principle as an axiom. – Mauro ALLEGRANZA Jun 2 '15 at 20:10
• Isn't $x \notin x$ the same as the axiom of foundation? – TokenToucan Jun 3 '15 at 4:45
• It would be kind of weird if one of the paradoxes that motivated the creation of ZFC could be demonstrated in ZFC. – Jonathan Hebert Jun 3 '15 at 5:13

For 1, this is a derivation with Natural Deduction.

Consider a first-order language with a binary predicate $E(x,y)$ :

1) $(∃y)(∀x)(E(x,y) ↔ ¬E(x,x))$ --- assumed [b]

2) $(∀x)(E(x,s) ↔ ¬E(x,x))$ --- assumed [a] for $\exists$-elimination

3) $E(s,s) ↔ ¬E(s,s)$ --- from 2) by $\forall$-elimination

The formula in 3) is a contradiction, since $E(s,s) ↔ E(s,s)$. Thus, we have :

4) $\bot$ --- from 3)

5) $\bot$ --- from 4) by $\exists$-elimination, discharging [a] : $s$ does not occur in 5)

6) $(∃y)(∀x)(E(x,y) ↔ ¬E(x,x)) \to \bot$ --- from 1) and 5) by $\to$-introduction, discharging [a]

$\vdash \lnot (∃y)(∀x)(E(x,y) ↔ ¬E(x,x))$ --- from 6) by abbreviation : $\lnot p := p \to \bot$.

We have used no $\mathsf {ZFC}$ axioms.

Ref to :

Regarding 2, this formula is not valid.

Consider again the formula of first-order language with the binary predicate $E(x,y)$ :

$∀y∃x\lnot E(x,y)$.

If we interpret it into the domain $\mathbb N$ of natural numbers with $E$ interpreted as $\ge$, we have :

$∀y∃x(x < y)$

that is clearly not satisfied for $y=0$.

Thus, being not valid, it is not provable by rules of logic alone, i.e. :

$\nvdash ∀y∃x\lnot E(x,y)$.

In presence of the Axiom Schema of Separation, we can use the Russell's paradox argument to prove that the assumption :

$\exists y \forall x(x \in y)$

produces a contradiction. Simplifying a little :

1) $\exists y \forall x(x \in y)$ --- assumed [a]

2) $\forall x(x \in V)$ --- assumed [b] for $\exists$-elimination

3) $x \in V$ --- from 3) by $\forall$-elimination

4) $\mathsf {ZFC} \vdash \exists z \forall x (x \in z \leftrightarrow x \in V \land x \notin x)$ --- Axiom of Separation

5) $(x \in z \leftrightarrow x \in V \land x \notin x)$ --- from 4), assuming [c] : $\forall x (x \in z \leftrightarrow x \in V \land x \notin x)$ for $\exists$-introduction and by $\forall$-elimination

6) $(x \in z \leftrightarrow x \notin x)$ --- from 3) and 5) by tautological implication

7) $\exists z \forall x (x \in z \leftrightarrow x \notin x)$ --- from 6) by $\forall$-introduction : $x$ not free in assumptions [a], [b] or [c] and from 4) and 5) by $\exists$-elimination : $z$ not free in 7), discharging [c]

8) $\vdash \lnot \exists z \forall x (x \in z \leftrightarrow x \notin x)$ --- proved above

9) $\bot$ --- from 7) and 8)

10) $\bot$ --- from 1) and 2) by $\exists$-elimination : $V$ not free in 10), discharging [b]

11) $\exists y \forall x(x \in y) \to \bot$ --- from 1) and 10) by $\to$-introduction, discharging [a]

$\mathsf {ZFC} \vdash \lnot \exists y \forall x(x \in y)$ --- from 11) by abbreviation.

Thus, we have concluded with :

$\mathsf {ZFC} \vdash\forall y \exists x(x \notin y)$.

• Looks good. This is roughly how I did it my own system. I'm just wondering what you meant by "not a first-order theorem." – Dan Christensen Jun 3 '15 at 14:10
• @DanChristensen - you can read any good textbook of Math Log... For example, Tourlakis, page 37 for I.3.16 Definition ($\Gamma$-Theorems) and the "special case with $\Gamma= \emptyset$ : "We often say in this case [$\vdash A$] that $A$ is provable with no nonlogical axioms." – Mauro ALLEGRANZA Jun 3 '15 at 14:52
• This distinction doesn't seem like anything the would concern most mathematicians, but your proof is just what I was looking for. Thanks. – Dan Christensen Jun 3 '15 at 19:16

Two Proofs in ZFC that the Russell Set" is not a set.

(1) The axiom of regularity states: $\forall x ( x \neq \emptyset \rightarrow \exists y \in x\ ( x \cap y = \emptyset) )$. If we had a set $R = \{x: x \notin x\}$ then consider now $\{R\}$. We see that there must be an element of $\{R\}$ which is disjoint from $\{R\}$. Since the only element of $\{R\}$ is R, it must be that $R \cap \{R\} = \emptyset$. So, since $R \in \{R\}$, we cannot have $R \in R$ (by the definition of disjoint).

(2) If we had a set $R = \{x: x \notin x\}$ then $R \in R$ $\leftrightarrow$ $R \notin R$. By the bi-valence of 1st-order classical logic, we must have either $R \in R$ or $R \notin R$. Since in either we case we have contradictions, and contradictions are not coherent in 1st-order classical-logic, since they would entail the truth of every sentence in the language of ZFC, we reject the existence of $R$.

• Thanks, but while these look like quite rigorous proofs, I was looking for a purely formal proof, e.g. just a numbered list of formal statements citing the one axiom used to generate each statement. Something that could be verified by a computer. Is this not how formal proofs are written in the literature? – Dan Christensen Jun 3 '15 at 6:01