Revision as of 18:06, 11 January 2013 edit RandomDSdevel (talk \| contribs) Extended confirmed users 762 edits →Empty set, singleton, unordered pairs and tuples: Replaced LaTeX "=_{\mathrm{def}}" with LaTeX "\overset{\mathrm{def.}}{=}" and fixed resulting spacing error ← Previous edit		Revision as of 18:21, 11 January 2013 edit undo RandomDSdevel (talk \| contribs) Extended confirmed users 762 edits m →Ordered pair: Replaced LaTeX "=_{\mathrm{def}}" with LaTeX "\overset{\mathrm{def.}}{=}" Next edit →
Line 50: 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 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.

Implementation of mathematics in set theory: Difference between revisions