Editing New Foundations (section)

=== Ordered pairs ===
[[Relation (mathematics)|Relations]] and [[function (mathematics)|functions]] are defined in TST (and in NF and NFU) as sets of [[ordered pair]]s in the usual way. For purposes of stratification, it is desirable that a relation or function is merely one type higher than the type of the members of its field. This requires defining the ordered pair so that its type is the same as that of its arguments (resulting in a '''type-level''' ordered pair). The usual definition of the ordered pair, namely <math>(a, \ b)_K \; := \  \{ \{ a \}, \ \{ a, \ b \} \}</math>, results in a type two higher than the type of its arguments ''a'' and ''b''. Hence for purposes of determining stratification, a function is three types higher than the members of its field. NF and related theories usually employ [[Ordered pair#Quine–Rosser definition|Quine's set-theoretic definition]] of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements ''a'' and ''b'', and therefore does not directly work in NFU. 

As an alternative approach, Holmes{{sfn|Holmes|1998}} takes the ordered pair ''(a, b)'' as a [[primitive notion]], as well as its left and right [[projection (mathematics)|projection]]s <math>\pi_1</math> and <math>\pi_2</math>, i.e., functions such that <math>\pi_1((a, b)) = a</math> and <math>\pi_2((a, b)) = b</math> (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of <math>\{x \mid \phi \}</math> for any stratified formula <math>\phi</math> is considered a theorem and only proved later, so expressions like <math>\pi_1 = \{((a, b), a) \mid a, b \in V\}</math> are not considered proper definitions). Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter.