Content deleted Content added
Line 148:
over functions in the latter sense, all such uses are in principle eliminable. In [[NFU]],
notice that in <math>F(x)</math>, x has the same type as the expression <math>F(x)</math>, and F is three
types higher than <math>F(x)</math> (one type higher if a type-level pair is used). For any set A,
we define <math>F[A]</math> as <math>\{y \mid (\exists x.x \in A \wedge y=F(x))\}</math>,
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[A]</math> is a set in [[ZFC]] by Replacement. In [[NFU]],
notice that in <math>F[A]</math>, A has the same type as the expression <math>F[A]</math>, and F is two
types higher than <math>F[A]</math> (the same type 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"
| |||