🚀 go-pugleaf

In article <24780@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>This (or so I claim) is the single, simple, obvious cause of Russel's
>paradox.  In particular, R = {x : x not elem x} is a definition of
>type (2) that contains an implicit reference to R because x quantifies
>over a set that contains R.  (Or you could show the recursion in the
>definition of elem as I did before).  Also, although I am glossing
>over the fact that the paradox exists without the "R =" part of the
>above, it should be clear that the same points could be made by
>viewing set abstractions as self-defining names of sets.

It appears to me that you are complaining not about elementhood being a
proposition, but about the unrestricted range of the quantification in the
axiom of comprehension.  Note that your complaint about the implicit
reference to R is just as applicable to R = {x : x = x}, which gives the
universal set without using elementhood.

And, in fact, it is exactly this analysis which led to ZF set theory.  In
that theory, comprehension is limited to the form {x : x \in S and P(x)},
where S is a set (implicitly already known to exist) and P is a predicate.

Proper classes arose because it is hard to talk about sets in general
without them.  I think it is safe to say that most mathematicians are a bit
uncomfortable dealing with proper classes, but their use is at least
demonstrably consistent (at least if the underlying set theory is
consistent).

BTW
>]The source of the paradox is sometimes mistakenly traced to the idea
>]of self-membership, but that's a mistake, as, e.g., Peter Aczel's
>]recent work on nonwellfounded sets shows.
>
>Is this generally acknowledged now or still controversial?

It is certainly acknowledged that set theories with self-membership can be
consistent and sufficiently powerful.  I think it is clear that
self-membership is not in itself the problem; however, many of the analyses
of what the problem is (yours included) do exclude self-membership.