Content deleted Content added
Line 74:
with successive types (because x is considered as an element of y).
Where possible, a relation R (understood as a binary predicate) 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>). Where R is a set of ordered pairs, we read <math>x R y</math> as <math>(x,y)\in R</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. In [[NFU]], we need to bear in mind
that x and y are three types lower than R in <math>xRy</math> (this will drop to one type
when a type-level ordered pair is used).
Notice that here we do not support the distinction between range and codomain of a relation:
Line 84 ⟶ 86:
this necessary in our development. Note also that for the moment we do not consider relations
of arity greater than 2: all our relations are binary.
=== Operations on relations ===
All relations are here understood to be sets.
The <strong>converse</strong> of a relation R is the relation <math>\{(y,x) \mid x R y\}</math>.
The <strong>___domain</strong> of a relation R is the set <math>\{x \mid (\exists y.x R y)\}</math>.
The <strong>range</strong> of a relation R is the ___domain of the converse of R.
The <strong>relative product</strong> <math>R|S</math> is the relation <math>\{(x,z) \mid (\exists y.x R y \wedge y S z)\}</math>.
In [[ZFC]], all of these are sets by application of Union, Separation, and Power Set.
In [[NFU]], it is easy to see that these are stratified definitions.
=== Special kinds of relation ===
== Functions ==
A functional relation (where relation means binary predicate) is a binary predicate F such
that <math>(\forall xyz.x F y \wedge x F z \rightarrow y=z)</math>. Such a relation (predicate)
is implemented as a relation (set) exactly as in the previous section. So the predicate F is
implemented by the set <math>\{(x,y) \mid x F y\}</math>. We say that a set of ordered pairs F
is a function just in case <math>(\forall xyz.(x,y) \in F \wedge (x,z) \in F \rightarrow y=z)</math>.
We define F(x) as the unique object y such that <math>x F y</math> (if there is one) or
as the unique object y such that <math>(x,y) \in F</math>. The presence in both theories
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.
The function I defined by I(x) = x does not exist as a set in [[ZFC]] because it is "too large"
to be a set. It is a set in NFU. The function <math>S(x) = \{x\}</math> is not a function
in either theory (in ZFC because it is too large; in NFU because its definition is unstratified
and further it can be proved that there is no such function: see the resolution of
Cantor's paradox in the [[New Foundations]] article.
=== Special kinds of function ===
A function is an <strong>injection</strong> and is said to be <strong>one-to-one</strong> if
its converse is also a function.
If A and B are sets, a <strong>bijection from A to B</strong> is an injection whose range is
A and whose
| |||