Naive Set Theory Is Inconsistent

Russell's paradox shows that naive set theory is inconsistent. Not a good thing! This means you can derive contradictions, and of course from a contradiction you can derive anything, so that the system becomes completely worthless.

The text discusses a version of the paradox that involves the issue of whether a set can include its own powerset. But there are also simpler examples. The Axiom of Comprehension says that for any predicate formulable in first-order logic (plus the set membership relation $\in$), there is a set consisting of all the items that satisfy that formula. Well, here is a formula of first-order logic plus membership:

$$x \notin x$$

So we have, as an instance of the Comprehension Axiom,

$$\exists c \forall x(x \in c \leftrightarrow x \notin x)$$

But from this we can derive a contradiction. The above instance says that there is a set that is a member of itself if and only if it is not a member of itself. Call this set $pdox$ (since it's a paradoxical set!). (In effect we are setting up an existential elimination subproof.) Then we have $\forall x(x \in pdox \leftrightarrow x \notin x)$. If this is true of every object, then in particular it must be true of $pdox$ (by universal elimination). So now we have:

$$pdox \in pdox \leftrightarrow pdox \notin pdox$$

From here we can quickly derive a contradiction. We can prove that for any proposition $P$, $P \vee \neg P$. So in particular

$$pdox \in pdox \vee pdox \notin pdox$$

For disjunction elimination, assume that $pdox \in pdox$. Then by biconditional elimination, $pdox \notin pdox$. Now assume the other disjunct, $pdox \notin pdox$. A step of Reiteration allows us to write this down again as a conclusion inside our subproof. So we can complete the disjunction elimination step and conclude that $pdox \notin pdox$.

So far so good, but now we can use biconditional elimination again to conclude that $pdox \in pdox$. So we have derived both $pdox \in pdox$ and $pdox \notin pdox$ from our starting premises.

Recall that the sentence $pdox \notin pdox$ just abbreviates $\neg(pdox \in pdox)$. So, in Barwise and Etchemendy's system, we can derive $\perp$ by the $\perp$ Intro rule. This does not contain the constant $pdox$ that we used to instantiate the existential quantifier, so we can complete our existential elimination subproof and reach $\perp$ as our overall conclusion.

But this is clearly a disaster! After all, by $\perp$ Elim we can derive absolutely anything from $\perp$. So naive set theory is inconsistent.

Notice that the Axiom of Extensionality played no role in this derivation. We used only the rules of first-order logic plus the Comprehension Axiom. Since we know that first-order logic itself is sound, and therefore consistent, the source of the trouble appears to be the Comprehension Axiom.

(What if we restricted the predicates $P(x)$ in the Comprehension Axiom to properties expressible in first-order logic /emphwithout set membership? After all, the problem instance just discussed involves a property that includes the set membership relation. However, that would remove too much power. For instance, we need to be able to prove the existence of the powerset of a set, i.e. the set defined by the property $x \subseteq z$.)