Original form of Russell’s paradox: Let A be the set of all sets and let P(A) be the powerset of A. By Cantor, |P(A)| > |A|. But, P(A) is a subset of A, so |P(A)|<=|A|. That’s a contradiction.
Cantor’s theorem breaks down in my system when applied to the set of all sets, because its proof essentially relies on Russell’s paradox to reach the contradiction.
Hmm, that almost seems to be cutting off the nose to spite the cliche. Cantor’s construction is a very natural construction. A set theory where you can’t prove that would be seen by many as unacceptably weak. I’m a bit fuzzy on the details of your system, but let me ask, can you prove in this system that there’s any uncountable set at all? For example, can we prove |R| > |N| ?
Yes. The proof that |R| > |N| stays working because predicates over N aren’t themselves members of N, so the issue of “complete definedness” doesn’t come up.
Hmm, this make work then and not kill off too much of set theory. You may want to talk to a professional set theorist or logician about this (my specialty is number theory so all I can do is glance at this and say that it looks plausible). The only remaining issue then becomes that I’m not sure that this is inherently better than standard set theory. In particular, this approach seems much less counterintuitive than ZFC. But that may be due to the fact that I’m more used to working with ZF-like objects.
Ok, I’ve read up on Cantor’s theorem now, and I think the trick is in the types of A and P(A), and the solution to the paradox is to borrow a trick from type theory. A is defined as the set of all sets, so the obvious question is, sets of what key type? Let that key type be t. Then
A: t=>bool
P(A): (t=>bool)=>bool
We defined P(A) to be in A, so a t=>bool is also a t. Let all other possible types for t be T. t=(t=>bool)+T. Now, one common way to deal with recursive types like this is to treat them as the limit of a sequence of types:
t[i] = t[i-1]=>bool + T
A[i]: t[i]=>bool
P(A[i]) = A[i+1]
Then when we take the limit,
t = lim i->inf t[i]
A = lim i->inf A[i]
P(A) = lim i->inf P(A[i])
Then suddenly, paradoxes based on the cardinality of A and P(A) go away, because those cardinalities diverge!
I’m not sure I know enough about type theory to evaluate this. Although I do know that Russell’s original attempts to repair the defect involved type theory (Principia Mathematica uses a form of type theory however in that form one still can’t form the set of all sets). I don’t think the above works but I don’t quite see what’s wrong with it. Maybe Sniffnoy or someone else more versed in these matters can comment.
I don’t know anything about type theory; when I wrote that I heard it has philosophical problems when applied to set theory, I meant I heard that from you. What the problems might actually be was my own guess...
I can’t seem to work out for myself what you mean. Can you spell it out in more detail?
Original form of Russell’s paradox: Let A be the set of all sets and let P(A) be the powerset of A. By Cantor, |P(A)| > |A|. But, P(A) is a subset of A, so |P(A)|<=|A|. That’s a contradiction.
Cantor’s theorem breaks down in my system when applied to the set of all sets, because its proof essentially relies on Russell’s paradox to reach the contradiction.
Hmm, that almost seems to be cutting off the nose to spite the cliche. Cantor’s construction is a very natural construction. A set theory where you can’t prove that would be seen by many as unacceptably weak. I’m a bit fuzzy on the details of your system, but let me ask, can you prove in this system that there’s any uncountable set at all? For example, can we prove |R| > |N| ?
Yes. The proof that |R| > |N| stays working because predicates over N aren’t themselves members of N, so the issue of “complete definedness” doesn’t come up.
Hmm, this make work then and not kill off too much of set theory. You may want to talk to a professional set theorist or logician about this (my specialty is number theory so all I can do is glance at this and say that it looks plausible). The only remaining issue then becomes that I’m not sure that this is inherently better than standard set theory. In particular, this approach seems much less counterintuitive than ZFC. But that may be due to the fact that I’m more used to working with ZF-like objects.
The original form of Russell’s (Zermelo’s in fact) paradox is not this. The original form is {x|x not member of x}.
That leads to both
x is a member of x
and
x is not a member of x
And that is the original form of the paradox.
No. See for example This discussion. The form you give where it is described as a simple predicate recursion was not the original form of the paradox.
Ok, I’ve read up on Cantor’s theorem now, and I think the trick is in the types of A and P(A), and the solution to the paradox is to borrow a trick from type theory. A is defined as the set of all sets, so the obvious question is, sets of what key type? Let that key type be t. Then
We defined P(A) to be in A, so a t=>bool is also a t. Let all other possible types for t be T. t=(t=>bool)+T. Now, one common way to deal with recursive types like this is to treat them as the limit of a sequence of types:
Then when we take the limit,
Then suddenly, paradoxes based on the cardinality of A and P(A) go away, because those cardinalities diverge!
I’m not sure I know enough about type theory to evaluate this. Although I do know that Russell’s original attempts to repair the defect involved type theory (Principia Mathematica uses a form of type theory however in that form one still can’t form the set of all sets). I don’t think the above works but I don’t quite see what’s wrong with it. Maybe Sniffnoy or someone else more versed in these matters can comment.
I don’t know anything about type theory; when I wrote that I heard it has philosophical problems when applied to set theory, I meant I heard that from you. What the problems might actually be was my own guess...
Huh. Did I say that? I don’t know almost anything about type theory. When did I say that?