Implementation of mathematics in set theory: Difference between revisions

Revision as of 07:25, 24 January 2013

Revision as of 23:10, 26 January 2013

Line 44:

== Relations ==

[[Relation (mathematics)|Relations]] are sets whose members are all [[ordered pair]]s. Where possible, a relation ''<math>R''</math> (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 ''<math>R''</math> is a set of ordered pairs, read ''<math>xRy''</math> as <math>\left(''x, y''\right)∈'' \in R''</math>.

In [[ZFC]], some relations (such as the general equality relation or subset relation on sets) are "'too large"'

to be sets (but may be harmlessly reified as [[proper class]]es). In [[New Foundations|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> '' <math>x''</math> and ''<math>y''</math> would

need to have the same type (because they appear as projections of the same pair), but also

successive types (because ''<math>x''</math> is considered as an element of ''<math>y''</math>).

=== Related definitions ===

Line 62:

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 : yRx\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</math> is the relation <math>\left\{\left(x, z\right) : \exists y\,\left(xRy \wedge ySz\right)\right\}</math>.

In [[ZFC]], provingone proves that these notions are all generate or apply to sets followsvia fromthe [[ZFC]] axioms of ''[[axiom of union|Unionunion]]'', ''[[axiom of separation|Separationseparation]]'', and ''[[axiom of power set|Powerpower Setset]]''. 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.

Line 75:

=== Properties and kinds of relations ===

Let ''<math>R''</math> be some [[binary relation]]. ''<math>R''</math> is:

*'''[[Reflexive relation|Reflexive]]''' if ''<math>xRx''</math> for every ''<math>x''</math> in the field of ''<math>R''</math>.

* '''[[Symmetric relation|Symmetric]]''' if <math>\forall x, y \,(xRy \to yRx)</math>.

* '''[[Transitive relation|Transitive]]''' if <math>\forall x, y, z \,(xRy \wedge yRz \rightarrow xRz)</math>.

* '''[[Antisymmetric relation|Antisymmetric]]''' if <math>\forall x, y \,(xRy \wedge yRx \rightarrow x=y)</math>.

* '''[[Well-founded relation|Well-founded]]''' if for every set ''<math>S''</math> which meets the field of ''<math>R''</math>, <math>\ \exists x \in S</math> whose preimage under ''<math>R''</math> does not meet ''<math>S''</math>.

* '''Extensional''' if for every ''<math>x, y''</math> in the field of ''<math>R''</math>, ''<math>x = y''</math> if and only if ''<math>x''</math> and ''<math>y''</math> have the same preimage under ''<math>R''</math>.

Relations having certain combinations of the above properties have standard names. ''<math>R''</math> is:

* An '''[[equivalence relation]]''' if ''<math>R''</math> is reflexive, symmetric, and transitive.

* A '''[[partial order]]''' if ''<math>R''</math> is reflexive, antisymmetric, and transitive.

* A '''[[linear order]]''' if ''<math>R''</math> is a partial order and for every ''<math>x, y''</math> in the field of ''<math>R''</math>, either ''<math>xRy''</math> or ''</math>yRx''</math>.

* A '''[[well-ordering]]''' if ''<math>R''</math> is a linear order and well-founded.

* A '''set picture''' if ''<math>R''</math> is well-founded and extensional, and the field of ''<math>R''</math> either equals the downward closure of one of its members (called its ''top element''), or is empty.

== Functions ==