Content deleted Content added
Line 147:
both for sets F and for important functional predicates. As long as one does not quantify
over functions in the latter sense, all such uses are in principle eliminable. For any set A,
we define <math>F
more conveniently written as <math>\{F(x) \mid x \in A\}</math>. If A is a set and F
is any functional relation, <math>F
notice that in <math
types higher than <math>F(x)</math>(one type higher if a type-level pair is used).
The function I defined by I(x) = x does not exist as a set in [[ZFC]] because it is "too large"
|