Implementation of mathematics in set theory: Difference between revisions

Revision as of 23:25, 18 March 2016

Revision as of 01:22, 9 April 2016

Line 38:

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, thethese Kuratowskitwo pairdefinitions hashave a technical disadvantage: itthe 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 things that matter are that it satisfy the defining condition:

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