Russell's Paradox

*A*:Type, *Q*:(*A**A*Prop). *P*:(*A*Prop). *p*:*A*. *x*:*A*. *Q*(*x*,*p*) *P*(*x*))

Often Russell's Paradox is phrased in terms of sets and the membership relation between sets.

Let *x* *y*"

P:(SetProp).p:Set.x:Set. (xp)P(x)

which is sometimes called "unlimited comprehension", and may seem quite plausible.

Notice that unlimited comprehension is an instance of the body of the above theorem, using *Set**A**x* *p*"*Q*(*x*,*p*)

p:Set.x:Set. (xp) (xx)

by letting *P*(*x*)*x* *x*)

, p:Set. (pp) (pp)

(see lemma *P* *P*)

This contradiction does not depend essentially on the fact that we are talking about sets and trying to represent each property of sets as the set of all sets with that property.

Abstracting away from these details, we get the theorem that there is NO class of objects all of whose properties can be represented by the objects themselves no matter what representation method, *Q*(*x*,*p*)

(Think of *Q*(*x*,*p*)*x**p*

Here is a trivial variation of the theorem using the variable *Set*"*A*"*Q*"*x* *p*"*Q*(*x*,*p*)"

*Set*:Type, :(*Set**Set*Prop).

Thm* (*P*:(*Set*Prop). *p*:*Set*. *x*:*Set*. (*x* *p*) *P*(*x*))

About: