Implementation of mathematics in set theory: Difference between revisions

Revision as of 18:52, 25 October 2019

Revision as of 18:55, 25 October 2019

Line 35:

{{main article|Ordered pair}}

First, consider the '''ordered pair'''. The reason that this comes first is technical: ordered pairs are needed to implement [[Relation (mathematics)|relations]] and [[Function (mathematics)|functions]], which are needed to implement other concepts which may seem to be prior.

The first definition of the ordered pair was the definition <math>(x,y) \overset{\mathrm{def}}{=} \{\{\{x\},\emptyset\},\{\{y\}\}\}</math> proposed by [[Norbert Wiener]] in 1914 in the context of the type theory of [[Principia Mathematica]]. Wiener observed that this allowed the elimination of types of ''n''-ary relations for <math>''n'' > 1</math> from the system of that work.

It is more usual now to use the definition <math>(x,y) \overset{\mathrm{def.}}{=} \{\{x\},\{x,y\}\}</math>, due to [[Kazimierz Kuratowski|Kuratowski]].

Either of these definitions works in either [[ZFC]] or [[New Foundations|NFU]]. In NFU, these two definitions have a technical disadvantage: the Kuratowski ordered pair is two types higher than its projections, while the Wiener ordered pair is three types higher. It is common to postulate the existence of a type-level ordered pair (a pair <math>(x,y)</math> which is the same type as its [[Projection (mathematics)|projections]]) in NFU. It is convenient to use the Kuratowski pair in both systems until the use of type-level pairs can be formally justified.

The internal details of these definitions have nothing to do with their actual mathematical function. For any notion <math>(x,y)</math> of ordered pair, the thingsthing that mattermatters areis that it satisfysatisfies the defining condition:

* :<math>(x,y)=(z,w) \ \equiv \ x=z \wedge y=w</math>

…and that it be reasonably easy to collect ordered pairs into sets.