Implementation of mathematics in set theory: Difference between revisions

Revision as of 01:36, 24 January 2013

Revision as of 01:43, 24 January 2013

Line 56:

The '''[[inverse relation|converse]]''' of <math>R</math> is the relation <math>\left\{\left(y, x\right) : xRy\right\}</math>.

The '''___domain''' of <math>R</math> is the set <math>\left\{x : \exists y \in \left(xRy\right)\right\}</math>.

The '''range''' of <math>R</math> is the ___domain of the converse of <math>R</math>.

Line 70:

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) : a \in A \wedge b \in B\right\}</math> is a set (being a subclass of <math>P\!\left(mathcal{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 : xRy\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 ===