Implementation of mathematics in set theory: Difference between revisions

Revision as of 16:21, 2 June 2022

Revision as of 16:31, 2 June 2022

Line 97:

In NFU, <math>x</math> has the same type as <math>F\!\left(x\right)</math>, and <math>F</math> is three types higher than <math>F\!\left(x\right)</math> (one type higher, if a type-level ordered pair is used). To solve this problem, one could define <math>F\left[A\right]</math> as <math>\left\{y : \exists x\,\left(x \in A \wedge y = F\!\left(x\right)\right)\right\}</math> for any set <math>A</math>, but this is more conveniently written as <math>\left\{F\!\left(x\right) : x \in A\right\}</math>. Then, if <math>A</math> is a set and <math>F</math> is any functional relation, the [[Axiom of replacement|Axiom of Replacement]] assures that <math>F\left[A\right]</math> is a set in [[ZFC]]. In NFU, <math>F\left[A\right]</math> and <math>A</math> now have the same type, and <math>F</math> is two types higher than <math>F\left[A\right]</math> (the same type, if a type-level ordered pair is used).

The function <math>I</math> such that <math>I\!\left(x\right) = x</math> is not a set in ZFC because it is "too large". <math>I\!\left(x\right)</math> is however a set in NFU. The function (predicate) <math>S</math> such that <math>S\!\left(x\right) = \left\{x\right\}</math> is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be [[Stratified formula#In set theory|stratified]]. Moreover, <math>S\!\left(x\right)</math> can be proved not to exist in NFU (see the resolution of [[Cantor's paradox]] in [[New Foundations]].)

=== Operations on functions ===