Implementation of mathematics in set theory: Difference between revisions

Revision as of 03:19, 21 December 2005

Revision as of 03:21, 21 December 2005

Line 146:

of functional predicates which are not sets makes it useful to allow the notation F(x)

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. ForIn any set A[[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(x)[A]</math>, xA has the same type as the expression <math>F(x)[A]</math>, and F is threetwo

types higher than <math>F(x)[A]</math>(onethe same 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"