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 ), there is a set consisting of all the items that satisfy that formula. Well, here is a formula of first-order logic plus membership:

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

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 (since it's a paradoxical set!). (In effect we are setting up an existential elimination subproof.) Then we have . If this is true of every object, then in particular it must be true of (by universal elimination). So now we have:

From here we can quickly derive a contradiction. We can prove that for any proposition , . So in particular

For disjunction elimination, assume that . Then by biconditional elimination, . Now assume the other disjunct, . 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 .

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

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

But this is clearly a disaster! After all, by Elim we can derive absolutely anything from . 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 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 .)