Implementation of mathematics in set theory: Difference between revisions

Content deleted Content added
m Relations: wording
Line 45:
[[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>). When <math>R</math> is a relation, the notation <math>xRy</math> means <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>).
Line 57:
The '''___domain''' of <math>R</math> is the set <math>\left\{x : \exists y \left(xRy\right)\right\}</math>.
 
The '''range''' of <math>R</math> is the ___domain of the converse of <math>R</math>. That is, the set <math>\left\{y : \exists x \left(xRy\right)\right\}</math>.
 
The '''field''' of <math>R</math> is the [[union (set theory)|union]] of the ___domain and range of <math>R</math>.
Line 67:
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]], one proves that these notions all generate or apply to sets via the [[ZFC]] axioms of ''[[axiom of union|union]]Union'', ''[[axiom of separation|separation]]Separation'', and ''[[axiomAxiom of power set|powerPower set]]''. In [[New Foundations|NFU]], it is easy to check that these definitions give rise to stratified formulas.
 
Notice that with our formal definition of a binary relation, the range and codomain of a relation are not distinguished:. thisThis 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 [[cartesianCartesian 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>\mathcal{P}\!\left(A \cup B\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 ===
LetA <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>.
Line 82:
* '''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. A binary relation <math>R</math> is:
 
* An '''[[equivalence relation]]''' if <math>R</math> is reflexive, symmetric, and transitive.