When you have "predicate types" in practice you need restrictions on what kind of predicates are allowed. If you allow anything at all, that's when you get Russ

When you have "predicate types" in practice you need restrictions on what kind of predicates are allowed. If you allow anything at all, that's when you get Russell's paradox. That tells us the general comprehension principle is invalid, that is, you cannot allow the construction of a set from an arbitrary predicate (or definite condition). > Predicate types only have a notion of "cardinality" anyway when you restrict the possible values to some finite universe. It is much more subtle than that. Regular set theory allows cardinalities far bigger than the least infinite cardinal, aleph-zero. But of course it's computers that we are talking about. Even then it's wrong. What if I define a predicate that's returns true for every natural number? Then it's infinite. But what if I define a complicated enough predicate that it does not halt for some numbers? Then we get back a recursively enumerable set that may or may not be infinite. In essence, when you introduce predicates, you no longer really care about cardinalities you start to care about the complexity of the predicates. For your purpose, your predicate has to be sufficiently simple that it denotes a recursive set (not a recursively enumerable set).