Formalizing Russel’s Paradox in FOL.

elementary-set-theorypredicate-logicpropositional-calculus

I think I understand Russel's Paradox and can describe it in natural language, but I'm having a hard time formalizing it in logic. Here's the tiny bit I came up with so far:

$($The set $A = \{X: X \notin X\}$ exists. $) \rightarrow (A \in A \leftrightarrow A \notin A)$

Since $A \in A \leftrightarrow A \notin A$ is a contradiction, the above statement can never be true if the set $A$ exists. This is the paradox and why they came up with axioms that ensure there are not sets containing themselves.

But this seems like it's just the final conclusion (if it even is formalized correctly?). How do I get there? How do I formalize for instance "Assuming $A$ contains itself, its defining property $A \notin X$ is not satisfied, therefore it doesn't contain itself" and how do I get to the contradiction $A \in A \leftrightarrow A \notin A $? How do I do the whole thing step by step?

I'm not familiar with axiomatic set theory, so if it is possible to formalize it just using propositional or predicate logic and naive set theory that would be the best.

I'd greatly appreciate some pointers in the right direction.

Best Answer

The following is a theorem of FOL (first order logic) in any standard system, where $\mathsf{L}$ is any binary predicate:

$$\mathsf{\neg\exists x\forall y(Lxy \leftrightarrow \neg Lyy)}$$

So, first step, just prove this in your favourite system!

Now suppose that we interpret the predicate '$\mathsf{L}$' as ... shaves ---, and take the domain to be the men in some particular village. Then our theorem tells us that there is no man in the village who shaves all and only those who do not shave themselves. Sometimes this is called the Barber Paradox -- but there is no genuine paradox here, just a logical theorem that there can be no such person!

Suppose instead that we interpret '$\mathsf{L}$' as .. is a member of ---, and take the domain to be the universe of sets. Then our theorem tells us that there is no set which has as its members just those sets which are not members of themselves. Think of a set which doesn't contain itself as a normal set: then we have shown that there is no set of all normal sets. This is, famously, Russell's Paradox. And this time the label 'paradox' is perhaps a bit more appropriate.

(Why? Because, assuming we can understand the mathematicians' usual idea of a set as an object over and above its members, ... is a normal set --- seems a perfectly sensible unary predicate. And it is a rather plausible principle that, given a sensible unary predicate, we can gather together the things that satisfy the predicate into a set. So it is a bit of a surprise to find, purely as a matter of logic, that there can be no set of normal sets -- our plausible principle can't be applied across the board.)

[That's borrowed from P-t-r Sm-th's freely downloadable Intro to Formal Logic -- which proves the theorem on p. 312.]