The use of the member and subset subjects may be problematic, as it might not unify well with the usual "forall x: S123(x) => ..." technique of describing membership with the predicate. A182 was supposed to say "A subset of N which contains 1 and which always contains successor(n) when it contains n, must equal N. This is the first assertion which binds a set to a variable, and we don't really have a way to use a variable as a predicate the way we can use a subject like N.
The fact that we can create subjects like "member" and "subset" itself suggests that we might want to be able to deal with things this way, but I'm still not clear.
1 Comment on D9
The use of the member and subset subjects may be problematic, as it might not unify well with the usual "forall x: S123(x) => ..." technique of describing membership with the predicate. A182 was supposed to say "A subset of N which contains 1 and which always contains successor(n) when it contains n, must equal N. This is the first assertion which binds a set to a variable, and we don't really have a way to use a variable as a predicate the way we can use a subject like N.
The fact that we can create subjects like "member" and "subset" itself suggests that we might want to be able to deal with things this way, but I'm still not clear.
add a comment