Content deleted Content added
→Empty set, singleton, unordered pairs and tuples: Clarified abbreviation of 'defined' to 'def' by reinstating periods ('.'s) afterwards, giving 'def.' over equals signs |
m →Ordered pair: Clarified abbreviation of 'defined' to 'def' by reinstating periods ('.'s) afterwards, giving 'def.' over equals signs |
||
Line 37:
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 implementat 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, the Kuratowski pair has a technical disadvantage: it is two types higher than its projections. 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 things that matter are that it satisfy the defining condition:
|