The predicate shaves(X,X) is very different from the predicate member-of(X,X).
To find values of X that satisfy the first, you simply enumerate all of your facts about
shaves(al, fred)
shaves(al, joe)
shaves(al, al)
and look for one that unifies with shaves(X,X).
You aren’t going to find the X that satisfy member(X,X) by unification. It isn’t even ever true for finite sets, except by convention for the empty set.
It isn’t even ever true for finite sets, except by convention for the empty set.
I think that you’re confusing the element-of relation with the subset-of relation. Or something. But then, all sets are subsets of themselves, including finite ones, so I’m not sure what you were thinking.
At any rate, the empty set is not an element of itself according to any convention that I’ve ever seen.
You aren’t going to find the X that satisfy member(X,X) by unification.
I’m not sure how to respond to this until you answer my question in this comment.
The predicate shaves(X,X) is very different from the predicate member-of(X,X). To find values of X that satisfy the first, you simply enumerate all of your facts about
shaves(al, fred) shaves(al, joe) shaves(al, al)
and look for one that unifies with shaves(X,X).
You aren’t going to find the X that satisfy member(X,X) by unification. It isn’t even ever true for finite sets, except by convention for the empty set.
I think that you’re confusing the element-of relation with the subset-of relation. Or something. But then, all sets are subsets of themselves, including finite ones, so I’m not sure what you were thinking.
At any rate, the empty set is not an element of itself according to any convention that I’ve ever seen.
I’m not sure how to respond to this until you answer my question in this comment.
You’re right; I was mis-remembering. It can’t be, or 1 := 0 u {0} wouldn’t work.