|
=== Related definitions ===
Let ''<math>R''</math> and ''<math>S''</math> be given [[binary relation]]s. Then the following concepts are useful:
The '''[[inverse relation|converse]]''' of ''<math>R''</math> is the relation <math>\left\{\left(y, x\right) \mid: x R yxRy\right\}</math>.
The '''___domain''' of ''<math>R''</math> is the set <math>\left\{x \mid: \exists y \,(xin R y\left(xRy\right)\}</math>.
The '''range''' of ''<math>R''</math> is the ___domain of the converse of ''<math>R''</math>.
The '''field''' of ''<math>R''</math> is the [[union (set theory)|union]] of the ___domain and range of ''<math>R''</math>.
The '''[[preimage]]''' of a member ''<math>x''</math> of the field of ''<math>R''</math> is the set <math>\left\{y \mid y: RxyRx\right\}</math> (used in the definition of "'well-founded"' below).
The '''downward closure''' of a member ''<math>x''</math> of the field of ''<math>R''</math> is the smallest set ''<math>D''</math> containing ''<math>x''</math>, and containing each ''<math>zRy''</math> for each ''<math>y''∈'' \in D''</math> (i.e., including the preimage of each of its elements with respect to ''<math>R''</math> as a subset).
The '''[[relation composition|relative product]]''' <math>R|S</math> of ''<math>R''</math> and ''<math>S'', ''R|S'',</math> is the relation <math>\left\{\left(x, z\right) \mid: \exists y\,\left(xRy \wedge ySz\right)\right\}</math>.
In [[ZFC]], proving that these notions are all sets follows from ''[[axiom of union|Union]]'', ''[[axiom of separation|Separation]]'', and ''[[axiom of power set|Power Set]]''. In [[New Foundations|NFU]], it is easy to check that these definitions give rise to stratified formulas.
Notice that the range and codomain of a relation are not distinguished: this could be done by representing a relation ''<math>R''</math> with codomain ''<math>B''</math> as ''<math>\left(R, B\right)''<\math>, but our development will not require this.
In [[ZFC]], any relation whose ___domain is a subset of a set ''<math>A''</math> and whose range is a subset of a set ''<math>B''</math> will be a set, since the [[cartesian product]] <math>A \times B = \left\{\left(a, b\right) \mid: a \in A \wedge b \in B\right\}</math> is a set (being a subclass of <math>P\!\left(P\!\left(A \cup B\right)\right)</math>), and ''Separation'' provides for the existence of <math>\left\{\left(x, y\right) \in A \times B \mid: x R yxRy\right\}</math>. In [[New Foundations|NFU]], some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that ''<math>x''</math> and ''<math>y''</math> are three types lower than ''<math>R''</math> in <math>xRy</math> (one type lower if a type-level ordered pair is used).
=== Properties and kinds of relations ===
| 