0
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ 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?) $\endgroup$ – Asaf Karagila Jun 2 '15 at 19:12
  • $\begingroup$ If it could be translated into ZFC by anybody who has existed since its invention, do you think we'd still be using ZFC? $\endgroup$ – Thomas Andrews Jun 2 '15 at 19:15
  • 2
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Jun 2 '15 at 20:10
  • 1
    $\begingroup$ Isn't $x \notin x$ the same as the axiom of foundation? $\endgroup$ – TokenToucan Jun 3 '15 at 4:45
  • 1
    $\begingroup$ It would be kind of weird if one of the paradoxes that motivated the creation of ZFC could be demonstrated in ZFC. $\endgroup$ – Jonathan Hebert Jun 3 '15 at 5:13
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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." $\endgroup$ – Dan Christensen Jun 3 '15 at 14:10
  • 1
    $\begingroup$ @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." $\endgroup$ – Mauro ALLEGRANZA Jun 3 '15 at 14:52
  • $\begingroup$ This distinction doesn't seem like anything the would concern most mathematicians, but your proof is just what I was looking for. Thanks. $\endgroup$ – Dan Christensen Jun 3 '15 at 19:16
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Dan Christensen Jun 3 '15 at 6:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.