Editing Ordered pair (section)

===Quine–Rosser definition===
[[J. Barkley Rosser|Rosser]] (1953)<ref>[[J. Barkley Rosser]], 1953. ''Logic for Mathematicians''. McGraw–Hill.</ref> employed a definition of the ordered pair due to [[Willard van Orman Quine|Quine]] which requires a prior definition of the [[natural number]]s. Let <math>\N</math> be the set of natural numbers and define first
<math display="block">\sigma(x) := \begin{cases}
      x, & \text{if }x \notin \N, \\
      x+1, & \text{if }x \in \N.
    \end{cases}</math>
The function <math>\sigma</math> increments its argument if it is a natural number and leaves it as is otherwise; the number 0 does not appear in the range of <math>\sigma</math>.
As <math>x \setminus \N</math> is the set of the elements of <math>x</math> not in <math>\N</math> go on with
<math display="block">\varphi(x) := \sigma[x] = \{\sigma(\alpha)\mid\alpha \in x\} = (x \setminus \N) \cup \{n+1 : n \in (x \cap \N) \}.</math>
This is the [[Image (mathematics)#Image of a subset|set image]] of a set <math>x</math> under <math>\sigma</math>, [[Image (mathematics)#Other terminology|sometimes denoted]] by <math>\sigma''x</math> as well. Applying function <math>\varphi</math> to a set ''x'' simply increments every natural number in it. In particular, <math>\varphi(x)</math> never contains contain the number 0, so that for any sets ''x'' and ''y'',
<math display="block">\varphi(x) \neq \{0\} \cup \varphi(y).</math>
Further, define
<math display="block">\psi(x) := \sigma[x] \cup \{0\} = \varphi(x) \cup \{0\}.</math>
By this, <math>\psi(x)</math> does always contain the number 0.

Finally, define the ordered pair (''A'', ''B'') as the disjoint union
<math display="block">(A, B) := \varphi[A] \cup \psi[B] = \{\varphi(a) : a \in A\} \cup \{\varphi(b) \cup \{0\} : b \in B \}.</math>
(which is <math>\varphi''A \cup \psi''B</math> in alternate notation).

Extracting all the elements of the pair that do not contain 0 and undoing <math>\varphi</math> yields ''A''. Likewise, ''B'' can be recovered from the elements of the pair that do contain 0.<ref>[https://randall-holmes.github.io/ Holmes, M. Randall]: ''[https://web.archive.org/web/20180416202817/http://math.boisestate.edu/~best/best18/Talks/holmes_best18.pdf On Ordered Pairs]'', on: Boise State, March 29, 2009. The author uses <math>\sigma_1</math> for <math>\varphi</math> and <math>\sigma_2</math> for <math>\psi</math>.</ref>

For example, the pair <math>( \{\{a,0\},\{b,c,1\}\} , \{\{d,2\},\{e,f,3\}\} ) </math> is encoded as <math>\{\{a,1\},\{b,c,2\},\{d,3,0\},\{e,f,4,0\}\}</math> provided <math>a,b,c,d,e,f\notin \N</math>.

In [[type theory]] and in outgrowths thereof such as the axiomatic set theory [[New Foundations|NF]], the Quine–Rosser pair has the same type as its projections and hence is termed a "type-level" ordered pair. Hence this definition has the advantage of enabling a [[function (mathematics)|function]], defined as a set of ordered pairs, to have a type only 1 higher than the type of its arguments. This definition works only if the set of natural numbers is infinite. This is the case in [[New Foundations|NF]], but not in [[type theory]] or in [[New Foundations|NFU]]. [[J. Barkley Rosser]] showed that the existence of such a type-level ordered pair (or even a "type-raising by 1" ordered pair) implies the [[axiom of infinity]]. For an extensive discussion of the ordered pair in the context of Quinian set theories, see Holmes (1998).<ref>Holmes, M. Randall (1998) ''[http://math.boisestate.edu/~holmes/holmes/head.pdf  Elementary Set Theory with a Universal Set] {{Webarchive|url=https://web.archive.org/web/20110411041046/http://math.boisestate.edu/%7Eholmes/holmes/head.pdf |date=2011-04-11 }}''. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this monograph via the web.</ref>