= 27d567bc2d48d9f40e9ccc20ea370b15)
MrMind comments on No coinductive datatype of integers - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (138)
Yes, but Subsets(x,y) is a primitive relationship in ZFC. I don't really know what cousin_it means by an explanation, but assuming it's something like a first-order definition formula, nothing like that exists in ZFC that doesn't subsume the concept in the first place.
No, it isn't. The only primitive relations in ZFC are set membership and possibly equality (depending on how you prefer it). "x is a subset of y" is defined to mean "for all z, z in x implies z in y".
Can I downvote myself? Somehow my mind switched "subset" and "membership", and by the virtue of ZFC being a one-sorted theory, lo and behold, I wrote the above absurdity. Anyway, to rewrite the sentence and make it less wrong: subsets(x,y) is defined by the means of a first-order formula through the membership relation, which in a one-sorted theory already pertains the idea of 'subsetting'. x E y --> {x} <= y. So subsetting can be seen as a transfinite extension of the membership relation, and in ZFC we get no more clarity or computational intuition from the first than from the second.