Content deleted Content added
No edit summary |
No edit summary |
||
Line 41:
== Ordered pair ==
The first substantial mathematical construction we consider is the <strong>ordered pair</strong>. The reason
that this comes first is technical: we will need it to implement notions of [[relation (mathematics) | relation]] and
[[function (mathematics) | function]] which are needed for implementations of other concepts which may seem to be prior.
Line 64:
and that it be reasonably easy to collect ordered pairs into sets.
== Relations ==
A relation is implemented as a set of ordered pairs, in either [[ZFC]] or [[NFU]]. In [[ZFC]],
some relations (such as the general equality relation or subset relation on sets) are too large
to be sets, and so cannot be implemented as sets (but may harmlessly be reified as [[proper classes]]). In [[NFU]], some relations (such as the membership relation) are not sets because
their definitions are not stratified: in <math>\{(x,y) \mid x \in y\}</math> x and y would
need to have the same type (because they appear as projections of the same pair, but also
with successive types (because x is considered as an element of y).
Where possible, a relation R is implemented as <math>\{(x,y) \mid x R y\}</math> (which may
be written as <math>\{z \mid \pi_1(z) R \pi_2(z)\}</math>). In [[ZFC]], any relation which
has ___domain a subset of a set A and range a subset of a set B will be a set, since the cartesian product <math>A \times B = \{(a,b) \mid a \in A wedge b \in B\}</math> is a set (being a
subclass of <math>P(P(A \cup B))</math>) and Separation provides for the existence of <math>\{(x,y)\in A \times B \mid x R y\}</math>. In [[NFU]], some relations with global scope
(such as equality and subset) are implemented as sets.
| |||