The “member” predicate is not a predicate like “shaves”; it is a primitive predicate, like “and”, with special semantics. If you want to generate the set of X for which member(X,Y) is true, you need Y to be bound. To generate the set of Y for which member(X,Y) is true, you need X to be bound. That’s what I meant.
Asking for the set of all for which member(X,Y) is true is going to get stuck in an infinite loop without ever generating any results. There is some connection between Russell’s paradox, and queries that generate a useless infinite loop in a query language. You can look at a statement of the paradox and feel that it leads to two contradictory proofs; but if you define set theory and the algorithms used to answer queries, I think (but am not sure) you will find that you can prove what the algorithm will produce when run.
Thanks for the pointer. I was saying that my guess is that Russell’s paradox reduces to something like the Kleene-Rosser paradox, which is resolved when you spell out the order of execution; and that we shouldn’t worry about paradoxes that are resolved when you spell out the order of execution, because a “formal logic” without the details for performing computations spelled out is not sufficiently formal.
The “member” predicate is not a predicate like “shaves”; it is a primitive predicate, like “and”, with special semantics. If you want to generate the set of X for which member(X,Y) is true, you need Y to be bound. To generate the set of Y for which member(X,Y) is true, you need X to be bound. That’s what I meant.
That’s not a problem, because, like I said, both arguments of member(X,X) are bound in Russell’s paradox. They are both bound by the phrase “The set of all X such that. . .” that precedes them.
Asking for the set of all for which member(X,Y) is true is going to get stuck in an infinite loop without ever generating any results.
Again, I need to know how you are encoding sets before I can answer any question about what an algorithm would do on given input.
but if you define set theory and the algorithms used to answer queries, I think (but am not sure) you will find that you can prove what the algorithm will produce when run.
My talk of “primitive predicates” makes sense only if you’re talking about a computational implementation.
In a truly formal logic, you do determine the definitions of the predicates purely by the axioms they are found in, including a set of axioms that are production rules, which therefore spell out execution (although order of execution is still usually ambiguous). ZF set theory is like that.
But I’ve never seen a presentation of Russell’s paradox which defined what “not” and “member-of” mean in an axiomatic way. I don’t think that had even been done for set theory at the time Russell proposed his paradox. The presentations I’ve seen always rely on your intuition about what “not” and “member of” mean.
The “member” predicate is not a predicate like “shaves”; it is a primitive predicate, like “and”, with special semantics. If you want to generate the set of X for which member(X,Y) is true, you need Y to be bound. To generate the set of Y for which member(X,Y) is true, you need X to be bound. That’s what I meant.
Asking for the set of all for which member(X,Y) is true is going to get stuck in an infinite loop without ever generating any results. There is some connection between Russell’s paradox, and queries that generate a useless infinite loop in a query language. You can look at a statement of the paradox and feel that it leads to two contradictory proofs; but if you define set theory and the algorithms used to answer queries, I think (but am not sure) you will find that you can prove what the algorithm will produce when run.
It looks like you’re using a computational model to understand Russell’s paradox. Should you be thinking of Kleene-Rosser?
Thanks for the pointer. I was saying that my guess is that Russell’s paradox reduces to something like the Kleene-Rosser paradox, which is resolved when you spell out the order of execution; and that we shouldn’t worry about paradoxes that are resolved when you spell out the order of execution, because a “formal logic” without the details for performing computations spelled out is not sufficiently formal.
That’s not a problem, because, like I said, both arguments of member(X,X) are bound in Russell’s paradox. They are both bound by the phrase “The set of all X such that. . .” that precedes them.
Again, I need to know how you are encoding sets before I can answer any question about what an algorithm would do on given input.
One wouldn’t want all queries within set theory to be decidable by some algorithm. If that were the case, then set theory would not be able to capture enough of arithmetic.
I’m aware of that. This particular paradox, though, is one where the question seems to be decidable both ways, not one where it’s undecidable.
My talk of “primitive predicates” makes sense only if you’re talking about a computational implementation.
In a truly formal logic, you do determine the definitions of the predicates purely by the axioms they are found in, including a set of axioms that are production rules, which therefore spell out execution (although order of execution is still usually ambiguous). ZF set theory is like that.
But I’ve never seen a presentation of Russell’s paradox which defined what “not” and “member-of” mean in an axiomatic way. I don’t think that had even been done for set theory at the time Russell proposed his paradox. The presentations I’ve seen always rely on your intuition about what “not” and “member of” mean.