Implementation of mathematics in set theory

<h2 id="preliminaries">Preliminaries</h2>
The following sections carry out certain constructions in the two theories <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> and compare the resulting implementations of certain mathematical structures (such as the <a href="/facts/Natural_numbers/u65og8JE">natural numbers</a>).
Mathematical theories prove theorems (and nothing else). So saying that a theory allows the construction of a certain object means that it is a theorem of that theory that that object exists. This is a statement about a definition of the form "the x such that 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
 exists", where 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
 is a <a href="/facts/Well-formed_formula/YpTVlzuj">formula</a> of our <a href="/facts/Formal_language/crDTyP8q">language</a>: the theory proves the existence of "the x such that 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
" just in case it is a theorem that "there is one and only one x such that 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
". (See <a href="/facts/Bertrand_Russell/SRpwNX2U">Bertrand Russell's</a> <a href="/facts/Theory_of_descriptions/dNpuBrr6">theory of descriptions</a>.) Loosely, the theory "defines" or "constructs" this object in this case. If the statement is not a theorem, the theory cannot show that the object exists; if the statement is provably false in the theory, it proves that the object cannot exist; loosely, the object cannot be constructed.
ZFC and NFU share the language of set theory, so the same formal definitions "the x such that 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
" can be contemplated in the two theories. A specific form of definition in the language of set theory is <a href="/facts/Set-builder_notation/0nVHQF6E">set-builder notation</a>: 
 
 
 
 {
 x
 ∣
 ϕ
 }
 
 
 {\displaystyle \{x\mid \phi \}}
 
 means "the set A such that for all x, 
 
 
 
 x
 ∈
 A
 ↔
 ϕ
 
 
 {\displaystyle x\in A\leftrightarrow \phi }
 
" (A cannot be <a href="/facts/Free_variables_and_bound_variables/ndWnXXYs">free</a> in 
 
 
 
 ϕ
 
 
 {\displaystyle \phi }
 
). This notation admits certain conventional extensions: 
 
 
 
 {
 x
 ∈
 B
 ∣
 ϕ
 }
 
 
 {\displaystyle \{x\in B\mid \phi \}}
 
 is synonymous with 
 
 
 
 {
 x
 ∣
 x
 ∈
 B
 ∧
 ϕ
 }
 
 
 {\displaystyle \{x\mid x\in B\wedge \phi \}}
 
; 
 
 
 
 {
 f
 (
 
 x
 
 1
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 )
 ∣
 ϕ
 }
 
 
 {\displaystyle \{f(x_{1},\ldots ,x_{n})\mid \phi \}}
 
 is defined as 
 
 
 
 {
 z
 ∣
 ∃
 
 x
 
 1
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 
 (
 z
 =
 f
 (
 
 x
 
 1
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 )
 ∧
 ϕ
 )
 }
 
 
 {\displaystyle \{z\mid \exists x_{1},\ldots ,x_{n}\,(z=f(x_{1},\dots ,x_{n})\wedge \phi )\}}
 
, where 
 
 
 
 f
 (
 
 x
 
 1
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 )
 
 
 {\displaystyle f(x_{1},\ldots ,x_{n})}
 
 is an expression already defined.
Expressions definable in set-builder notation make sense in both ZFC and NFU: it may be that both theories prove that a given definition succeeds, or that neither do (the expression 
 
 
 
 {
 x
 ∣
 x
 ∉
 x
 }
 
 
 {\displaystyle \{x\mid x\not \in x\}}
 
 fails to refer to anything in any set theory with classical logic; in <a href="/facts/Class_(set_theory)/F5EmDd9b">class</a> theories like <a href="/facts/Von_Neumann%25E2%2580%2593Bernays%25E2%2580%2593G%25C3%25B6del_set_theory/5wLhAIMz">NBG</a> this notation does refer to a class, but it is defined differently), or that one does and the other doesn't. Further, an object defined in the same way in ZFC and NFU may turn out to have different properties in the two theories (or there may be a difference in what can be proved where there is no provable difference between their properties).
Further, set theory imports concepts from other branches of mathematics (in intention, all branches of mathematics). In some cases, there are different ways to import the concepts into ZFC and NFU. For example, the usual definition of the first infinite <a href="/facts/Ordinal_number/GelFLjJt">ordinal</a> 
 
 
 
 ω
 
 
 {\displaystyle \omega }
 
 in ZFC is not suitable for NFU because the object (defined in purely set theoretical language as the set of all finite <a href="/facts/Von_Neumann_ordinal/GelFLjJt">von Neumann ordinals</a>) cannot be shown to exist in NFU. The usual definition of 
 
 
 
 ω
 
 
 {\displaystyle \omega }
 
 in NFU is (in purely set theoretical language) the set of all infinite <a href="/facts/Well-ordering/GrWEBWlW">well-orderings</a> all of whose proper initial segments are finite, an object which can be shown not to exist in ZFC. In the case of such imported objects, there may be different definitions, one for use in ZFC and related theories, and one for use in NFU and related theories. For such "implementations" of imported mathematical concepts to make sense, it is necessary to be able to show that the two parallel interpretations have the expected properties: for example, the implementations of the natural numbers in ZFC and NFU are different, but both are implementations of the same mathematical structure, because both include definitions for all the primitives of <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a> and satisfy (the translations of) the Peano axioms. It is then possible to compare what happens in the two theories as when only set theoretical language is in use, as long as the definitions appropriate to ZFC are understood to be used in the <a href="/facts/ZFC/UYIsPbXw">ZFC</a> context and the definitions appropriate to NFU are understood to be used in the NFU context.
Whatever is proven to exist in a theory clearly provably exists in any extension of that theory; moreover, analysis of the proof that an object exists in a given theory may show that it exists in weaker versions of that theory (one may consider <a href="/facts/Zermelo_set_theory/o3fzd9nl">Zermelo set theory</a> instead of ZFC for much of what is done in this article, for example).

<h2 id="empty-set-singleton-unordered-pairs-and-tuples">Empty set, singleton, unordered pairs and tuples</h2>
These constructions appear first because they are the simplest constructions in set theory, not because they are the first constructions that come to mind in mathematics (though the notion of finite set is certainly fundamental). Even though NFU also allows the construction of set <a href="/facts/Urelement/YLbuKp37">ur-elements</a> yet to become members of a set, the <a href="/facts/Empty_set/ffEk3eA6">empty set</a> is the unique set with no members:

∅
          
        
        
        
          
            =
            
              d
              e
              f
              .
            
          
        
        
          {
          
            x
            :
            x
            ≠
            x
          
          }
        
      
    
    {\displaystyle \left.\varnothing \right.\,{\overset {\mathrm {def.} }{=}}\left\{x:x\neq x\right\}}

For each object 
 
 
 
 x
 
 
 {\displaystyle x}
 
, there is a set 
 
 
 
 {
 x
 }
 
 
 {\displaystyle \{x\}}
 
 with 
 
 
 
 x
 
 
 {\displaystyle x}
 
 as its only element:

{
          x
          }
        
        
          
            =
            
              d
              e
              f
              .
            
          
        
        
          {
          
            y
            :
            y
            =
            x
          
          }
        
      
    
    {\displaystyle \left\{x\right\}{\overset {\mathrm {def.} }{=}}\left\{y:y=x\right\}}

For objects 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
, there is a set 
 
 
 
 {
 x
 ,
 y
 }
 
 
 {\displaystyle \{x,y\}}
 
 containing 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
 as its only elements:

{
          
            x
            ,
            y
          
          }
        
        
          
            =
            
              d
              e
              f
              .
            
          
        
        
          {
          
            z
            :
            z
            =
            x
            ∨
            z
            =
            y
          
          }
        
      
    
    {\displaystyle \left\{x,y\right\}{\overset {\mathrm {def.} }{=}}\left\{z:z=x\vee z=y\right\}}

The <a href="/facts/Union_(set_theory)/KVVXKfWl">union</a> of two sets is defined in the usual way:

x
            ∪
            y
          
          
        
        
        
          
            =
            
              d
              e
              f
              .
            
          
        
        
          {
          
            z
            :
            z
            ∈
            x
            ∨
            z
            ∈
            y
          
          }
        
      
    
    {\displaystyle \left.x\cup y\right.\,{\overset {\mathrm {def.} }{=}}\left\{z:z\in x\vee z\in y\right\}}

This is a recursive definition of unordered 
 
 
 
 n
 
 
 {\displaystyle n}
 
-tuples for any concrete 
 
 
 
 n
 
 
 {\displaystyle n}
 
 (finite sets given as lists of their elements:)

{
          
            
              x
              
                1
              
            
            ,
            …
            ,
            
              x
              
                n
              
            
            ,
            
              x
              
                n
                +
                1
              
            
          
          }
        
        
          
            =
            
              d
              e
              f
              .
            
          
        
        
          {
          
            
              x
              
                1
              
            
            ,
            …
            ,
            
              x
              
                n
              
            
          
          }
        
        ∪
        
          {
          
            x
            
              n
              +
              1
            
          
          }
        
      
    
    {\displaystyle \left\{x_{1},\ldots ,x_{n},x_{n+1}\right\}{\overset {\mathrm {def.} }{=}}\left\{x_{1},\ldots ,x_{n}\right\}\cup \left\{x_{n+1}\right\}}

In NFU, all the set definitions given work by stratified comprehension; in ZFC, the existence of the unordered pair is given by the <a href="/facts/Axiom_of_pairing/yva0UafC">Axiom of Pairing</a>, the existence of the empty set follows by <a href="/facts/Axiom_schema_of_separation/FVgjEBfT">Separation</a> from the existence of any set, and the binary union of two sets exists by the axioms of Pairing and <a href="/facts/Axiom_of_union/J8ANgm91">Union</a> (
 
 
 
 x
 ∪
 y
 =
 ⋃
 {
 x
 ,
 y
 }
 
 
 {\displaystyle x\cup y=\bigcup \{x,y\}}
 
).

<h2 id="ordered-pair">Ordered pair</h2>
Main article: <a href="/facts/Ordered_pair/EInLVI0r">Ordered pair</a>
First, consider the ordered pair. The reason that this comes first is technical: ordered pairs are needed to implement <a href="/facts/Relation_(mathematics)/HjblDaMy">relations</a> and <a href="/facts/Function_(mathematics)/CdReEKCh">functions</a>, which are needed to implement other concepts which may seem to be prior.
The first definition of the ordered pair was the definition 
 
 
 
 (
 x
 ,
 y
 )
 
 
 =
 
 d
 e
 f
 
 
 
 {
 {
 {
 x
 }
 ,
 ∅
 }
 ,
 {
 {
 y
 }
 }
 }
 
 
 {\displaystyle (x,y){\overset {\mathrm {def} }{=}}\{\{\{x\},\emptyset \},\{\{y\}\}\}}
 
 proposed by <a href="/facts/Norbert_Wiener/cVMRAHCU">Norbert Wiener</a> in 1914 in the context of the type theory of <a href="/facts/Principia_Mathematica/7ufeceV4">Principia Mathematica</a>. Wiener observed that this allowed the elimination of types of n-ary relations for n > 1 from the system of that work.
It is more usual now to use the definition 
 
 
 
 (
 x
 ,
 y
 )
 
 
 =
 
 d
 e
 f
 .
 
 
 
 {
 {
 x
 }
 ,
 {
 x
 ,
 y
 }
 }
 
 
 {\displaystyle (x,y){\overset {\mathrm {def.} }{=}}\{\{x\},\{x,y\}\}}
 
, due to <a href="/facts/Kazimierz_Kuratowski/8xoKvo5b">Kuratowski</a>.
Either of these definitions works in either ZFC or NFU. In NFU, these two definitions have a technical disadvantage: the 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 
 
 
 
 (
 x
 ,
 y
 )
 
 
 {\displaystyle (x,y)}
 
 which is the same type as its <a href="/facts/Projection_(mathematics)/QxxC9XTp">projections</a>) 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 
 
 
 
 (
 x
 ,
 y
 )
 
 
 {\displaystyle (x,y)}
 
 of ordered pair, the thing that matters is that it satisfies the defining condition

(
        x
        ,
        y
        )
        =
        (
        z
        ,
        w
        )
         
        ≡
         
        x
        =
        z
        ∧
        y
        =
        w
      
    
    {\displaystyle (x,y)=(z,w)\ \equiv \ x=z\wedge y=w}

…and that it be reasonably easy to collect ordered pairs into sets.

<h2 id="relations">Relations</h2>
<a href="/facts/Relation_(mathematics)/HjblDaMy">Relations</a> are sets whose members are all <a href="/facts/Ordered_pair/EInLVI0r">ordered pairs</a>. Where possible, a relation 
 
 
 
 R
 
 
 {\displaystyle R}
 
 (understood as a <a href="/facts/Binary_predicate/r9BwGgaK">binary predicate</a>) is implemented as 
 
 
 
 {
 (
 x
 ,
 y
 )
 ∣
 x
 R
 y
 }
 
 
 {\displaystyle \{(x,y)\mid xRy\}}
 
 (which may be written as 
 
 
 
 {
 z
 ∣
 
 π
 
 1
 
 
 (
 z
 )
 R
 
 π
 
 2
 
 
 (
 z
 )
 }
 
 
 {\displaystyle \{z\mid \pi _{1}(z)R\pi _{2}(z)\}}
 
). When 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is a relation, the notation 
 
 
 
 x
 R
 y
 
 
 {\displaystyle xRy}
 
 means 
 
 
 
 
 (
 
 x
 ,
 y
 
 )
 
 ∈
 R
 
 
 {\displaystyle \left(x,y\right)\in R}
 
.
In ZFC, some relations (such as the general equality relation or subset relation on sets) are 'too large'
to be sets (but may be harmlessly reified as <a href="/facts/Proper_class/F5EmDd9b">proper classes</a>). In NFU, some relations (such as the membership relation) are not sets because their definitions are not stratified: in 
 
 
 
 {
 (
 x
 ,
 y
 )
 ∣
 x
 ∈
 y
 }
 
 
 {\displaystyle \{(x,y)\mid x\in y\}}
 
, 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
 would
need to have the same type (because they appear as projections of the same pair), but also
successive types (because 
 
 
 
 x
 
 
 {\displaystyle x}
 
 is considered as an element of 
 
 
 
 y
 
 
 {\displaystyle y}
 
).

<h3>Related definitions</h3>
Let 
 
 
 
 R
 
 
 {\displaystyle R}
 
 and 
 
 
 
 S
 
 
 {\displaystyle S}
 
 be given <a href="/facts/Binary_relation/r9BwGgaK">binary relations</a>. Then the following concepts are useful:
The <a href="/facts/Converse_relation/EVGlRSz7">converse</a> of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the relation 
 
 
 
 
 {
 
 
 (
 
 y
 ,
 x
 
 )
 
 :
 x
 R
 y
 
 }
 
 
 
 {\displaystyle \left\{\left(y,x\right):xRy\right\}}
 
.
The domain of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the set 
 
 
 
 
 {
 
 x
 :
 ∃
 y
 
 (
 
 x
 R
 y
 
 )
 
 
 }
 
 
 
 {\displaystyle \left\{x:\exists y\left(xRy\right)\right\}}
 
.
The range of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the domain of the converse of 
 
 
 
 R
 
 
 {\displaystyle R}
 
. That is, the set 
 
 
 
 
 {
 
 y
 :
 ∃
 x
 
 (
 
 x
 R
 y
 
 )
 
 
 }
 
 
 
 {\displaystyle \left\{y:\exists x\left(xRy\right)\right\}}
 
.
The field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the <a href="/facts/Union_(set_theory)/KVVXKfWl">union</a> of the domain and range of 
 
 
 
 R
 
 
 {\displaystyle R}
 
.
The <a href="/facts/Preimage/KANefMAl">preimage</a> of a member 
 
 
 
 x
 
 
 {\displaystyle x}
 
 of the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the set 
 
 
 
 
 {
 
 y
 :
 y
 R
 x
 
 }
 
 
 
 {\displaystyle \left\{y:yRx\right\}}
 
 (used in the definition of 'well-founded' below.)
The downward closure of a member 
 
 
 
 x
 
 
 {\displaystyle x}
 
 of the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is the smallest set 
 
 
 
 D
 
 
 {\displaystyle D}
 
 containing 
 
 
 
 x
 
 
 {\displaystyle x}
 
, and containing each 
 
 
 
 z
 R
 y
 
 
 {\displaystyle zRy}
 
 for each 
 
 
 
 y
 ∈
 D
 
 
 {\displaystyle y\in D}
 
 (i.e., including the preimage of each of its elements with respect to 
 
 
 
 R
 
 
 {\displaystyle R}
 
 as a subset.)
The <a href="/facts/Relation_composition/tD8joBlo">relative product</a> 
 
 
 
 R
 ;
 S
 
 
 {\displaystyle R;S}
 
 of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 and 
 
 
 
 S
 
 
 {\displaystyle S}
 
 is the relation 
 
 
 
 
 {
 
 
 (
 
 x
 ,
 z
 
 )
 
 :
 ∃
 y
 
 
 (
 
 x
 R
 y
 ∧
 y
 S
 z
 
 )
 
 
 }
 
 
 
 {\displaystyle \left\{\left(x,z\right):\exists y\,\left(xRy\wedge ySz\right)\right\}}
 
.
Notice that with our formal definition of a binary relation, the range and codomain of a relation are not distinguished. This could be done by representing a relation 
 
 
 
 R
 
 
 {\displaystyle R}
 
 with codomain 
 
 
 
 B
 
 
 {\displaystyle B}
 
 as 
 
 
 
 
 (
 
 R
 ,
 B
 
 )
 
 
 
 {\displaystyle \left(R,B\right)}
 
, but our development will not require this.
In ZFC, any relation whose domain is a subset of a set 
 
 
 
 A
 
 
 {\displaystyle A}
 
 and whose range is a subset of a set 
 
 
 
 B
 
 
 {\displaystyle B}
 
 will be a set, since the <a href="/facts/Cartesian_product/BfqBWzdL">Cartesian product</a> 
 
 
 
 A
 ×
 B
 =
 
 {
 
 
 (
 
 a
 ,
 b
 
 )
 
 :
 a
 ∈
 A
 ∧
 b
 ∈
 B
 
 }
 
 
 
 {\displaystyle A\times B=\left\{\left(a,b\right):a\in A\wedge b\in B\right\}}
 
 is a set (being a subclass of 
 
 
 
 
 
 P
 
 
 
 
 (
 
 A
 ∪
 B
 
 )
 
 
 
 {\displaystyle {\mathcal {P}}\!\left(A\cup B\right)}
 
), and Separation provides for the existence of 
 
 
 
 
 {
 
 
 (
 
 x
 ,
 y
 
 )
 
 ∈
 A
 ×
 B
 :
 x
 R
 y
 
 }
 
 
 
 {\displaystyle \left\{\left(x,y\right)\in A\times B:xRy\right\}}
 
. In NFU, some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
 are three types lower than 
 
 
 
 R
 
 
 {\displaystyle R}
 
 in 
 
 
 
 x
 R
 y
 
 
 {\displaystyle xRy}
 
 (one type lower if a type-level ordered pair is used).

<h3>Properties and kinds of relations</h3>
A binary relation 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is:

<ul><li><a href="/facts/Reflexive_relation/NzTytEg9">Reflexive</a> if 
 
 
 
 x
 R
 x
 
 
 {\displaystyle xRx}
 
 for every 
 
 
 
 x
 
 
 {\displaystyle x}
 
 in the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
.</li>
<li><a href="/facts/Symmetric_relation/ekCWDIAH">Symmetric</a> if 
 
 
 
 ∀
 x
 ,
 y
 
 (
 x
 R
 y
 →
 y
 R
 x
 )
 
 
 {\displaystyle \forall x,y\,(xRy\to yRx)}
 
.</li>
<li><a href="/facts/Transitive_relation/9r90y50r">Transitive</a> if 
 
 
 
 ∀
 x
 ,
 y
 ,
 z
 
 (
 x
 R
 y
 ∧
 y
 R
 z
 →
 x
 R
 z
 )
 
 
 {\displaystyle \forall x,y,z\,(xRy\wedge yRz\rightarrow xRz)}
 
.</li>
<li><a href="/facts/Antisymmetric_relation/YhuqG4z8">Antisymmetric</a> if 
 
 
 
 ∀
 x
 ,
 y
 
 (
 x
 R
 y
 ∧
 y
 R
 x
 →
 x
 =
 y
 )
 
 
 {\displaystyle \forall x,y\,(xRy\wedge yRx\rightarrow x=y)}
 
.</li>
<li><a href="/facts/Well-founded_relation/zyRRyJ4M">Well-founded</a> if for every set 
 
 
 
 S
 
 
 {\displaystyle S}
 
 which meets the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
, 
 
 
 
  
 ∃
 x
 ∈
 S
 
 
 {\displaystyle \ \exists x\in S}
 
 whose preimage under 
 
 
 
 R
 
 
 {\displaystyle R}
 
 does not meet 
 
 
 
 S
 
 
 {\displaystyle S}
 
.</li>
<li>Extensional if for every 
 
 
 
 x
 ,
 y
 
 
 {\displaystyle x,y}
 
 in the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
, 
 
 
 
 x
 =
 y
 
 
 {\displaystyle x=y}
 
 if and only if 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
 have the same preimage under 
 
 
 
 R
 
 
 {\displaystyle R}
 
.</li></ul>
Relations having certain combinations of the above properties have standard names. A binary relation 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is:

<ul><li>An <a href="/facts/Equivalence_relation/1MQ5rtkW">equivalence relation</a> if 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is reflexive, symmetric, and transitive.</li>
<li>A <a href="/facts/Partial_order/qb4a3FAX">partial order</a> if 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is reflexive, antisymmetric, and transitive.</li>
<li>A <a href="/facts/Linear_order/xnTtmuYJ">linear order</a> if 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is a partial order and for every 
 
 
 
 x
 ,
 y
 
 
 {\displaystyle x,y}
 
 in the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
, either 
 
 
 
 x
 R
 y
 
 
 {\displaystyle xRy}
 
 or 
 
 
 
 y
 R
 x
 
 
 {\displaystyle yRx}
 
.</li>
<li>A <a href="/facts/Well-ordering/GrWEBWlW">well-ordering</a> if 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is a linear order and well-founded.</li>
<li>A set picture if 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is well-founded and extensional, and the field of 
 
 
 
 R
 
 
 {\displaystyle R}
 
 either equals the downward closure of one of its members (called its top element), or is empty.</li></ul>
<h2 id="functions">Functions</h2>
A functional relation is a <a href="/facts/Binary_predicate/r9BwGgaK">binary predicate</a> 
 
 
 
 F
 
 
 {\displaystyle F}
 
 such that 
 
 
 
 ∀
 x
 ,
 y
 ,
 z
 
 
 (
 
 x
 F
 y
 ∧
 x
 F
 z
 →
 y
 =
 z
 
 )
 
 .
 
 
 {\displaystyle \forall x,y,z\,\left(xFy\wedge xFz\to y=z\right).}
 
 Such a <a href="/facts/Relation_(mathematics)/HjblDaMy">relation</a> (<a href="/facts/Predicate_(logic)/5WazAvKF">predicate</a>) is implemented as a relation (set) exactly as described in the previous section. So the predicate 
 
 
 
 F
 
 
 {\displaystyle F}
 
 is implemented by the set 
 
 
 
 
 {
 
 
 (
 
 x
 ,
 y
 
 )
 
 :
 x
 F
 y
 
 }
 
 
 
 {\displaystyle \left\{\left(x,y\right):xFy\right\}}
 
. A relation 
 
 
 
 F
 
 
 {\displaystyle F}
 
 is a function if and only if 
 
 
 
 ∀
 x
 ,
 y
 ,
 z
 
 
 (
 
 
 (
 
 x
 ,
 y
 
 )
 
 ∈
 F
 ∧
 
 (
 
 x
 ,
 z
 
 )
 
 ∈
 F
 →
 y
 =
 z
 
 )
 
 .
 
 
 {\displaystyle \forall x,y,z\,\left(\left(x,y\right)\in F\wedge \left(x,z\right)\in F\to y=z\right).}
 
 It is therefore possible to define the value function 
 
 
 
 F
 
 
 (
 x
 )
 
 
 
 {\displaystyle F\!\left(x\right)}
 
 as the unique object 
 
 
 
 y
 
 
 {\displaystyle y}
 
 such that 
 
 
 
 x
 F
 y
 
 
 {\displaystyle xFy}
 
 – i.e.: 
 
 
 
 x
 
 
 {\displaystyle x}
 
 is 
 
 
 
 F
 
 
 {\displaystyle F}
 
-related to 
 
 
 
 y
 
 
 {\displaystyle y}
 
 such that the relation 
 
 
 
 f
 
 
 {\displaystyle f}
 
 holds between 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and 
 
 
 
 y
 
 
 {\displaystyle y}
 
 – or as the unique object 
 
 
 
 y
 
 
 {\displaystyle y}
 
 such that 
 
 
 
 
 (
 
 x
 ,
 y
 
 )
 
 ∈
 F
 
 
 {\displaystyle \left(x,y\right)\in F}
 
. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation 
 
 
 
 F
 
 
 (
 x
 )
 
 
 
 {\displaystyle F\!\left(x\right)}
 
 both for sets 
 
 
 
 F
 
 
 {\displaystyle F}
 
 and for important functional predicates. As long as one does not quantify over functions in the latter sense, all such uses are in principle eliminable.
Outside of formal set theory, we usually specify a function in terms of its domain and codomain, as in the phrase "Let 
 
 
 
 f
 :
 A
 →
 B
 
 
 {\displaystyle f:A\to B}
 
 be a function". The domain of a function is just its domain as a relation, but we have not yet defined the codomain of a function. To do this we introduce the terminology that a function is from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 if its domain equals 
 
 
 
 A
 
 
 {\displaystyle A}
 
 and its range is contained in 
 
 
 
 B
 
 
 {\displaystyle B}
 
. In this way, every function is a function from its domain to its range, and a function 
 
 
 
 f
 
 
 {\displaystyle f}
 
 from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 is also a function from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 C
 
 
 {\displaystyle C}
 
 for any set 
 
 
 
 C
 
 
 {\displaystyle C}
 
 containing 
 
 
 
 B
 
 
 {\displaystyle B}
 
.
Indeed, no matter which set we consider to be the codomain of a function, the function does not change as a set since by definition it is just a set of ordered pairs. That is, a function does not determine its codomain by our definition. If one finds this unappealing then one can instead define a function as the ordered pair 
 
 
 
 (
 f
 ,
 B
 )
 
 
 {\displaystyle (f,B)}
 
, where 
 
 
 
 f
 
 
 {\displaystyle f}
 
 is a functional relation and 
 
 
 
 B
 
 
 {\displaystyle B}
 
 is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as 
 
 
 
 (
 x
 ,
 y
 ,
 z
 )
 =
 (
 x
 ,
 (
 y
 ,
 z
 )
 )
 
 
 {\displaystyle (x,y,z)=(x,(y,z))}
 
- then one could define a function as the ordered triple 
 
 
 
 (
 f
 ,
 A
 ,
 B
 )
 
 
 {\displaystyle (f,A,B)}
 
 so as to also include the domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let 
 
 
 
 R
 ⊆
 A
 ×
 B
 
 
 {\displaystyle R\subseteq A\times B}
 
 be a binary relation", but formally 
 
 
 
 R
 
 
 {\displaystyle R}
 
 is a set of ordered pairs such that 
 
 
 
 
 dom
 
 
 R
 ⊆
 A
 
 
 {\displaystyle {\text{dom}}\,R\subseteq A}
 
 and 
 
 
 
 
 ran
 
 
 R
 ⊆
 B
 
 
 {\displaystyle {\text{ran}}\,R\subseteq B}
 
.
In NFU, 
 
 
 
 x
 
 
 {\displaystyle x}
 
 has the same type as 
 
 
 
 F
 
 
 (
 x
 )
 
 
 
 {\displaystyle F\!\left(x\right)}
 
, and 
 
 
 
 F
 
 
 {\displaystyle F}
 
 is three types higher than 
 
 
 
 F
 
 
 (
 x
 )
 
 
 
 {\displaystyle F\!\left(x\right)}
 
 (one type higher, if a type-level ordered pair is used). To solve this problem, one could define 
 
 
 
 F
 
 [
 A
 ]
 
 
 
 {\displaystyle F\left[A\right]}
 
 as 
 
 
 
 
 {
 
 y
 :
 ∃
 x
 
 
 (
 
 x
 ∈
 A
 ∧
 y
 =
 F
 
 
 (
 x
 )
 
 
 )
 
 
 }
 
 
 
 {\displaystyle \left\{y:\exists x\,\left(x\in A\wedge y=F\!\left(x\right)\right)\right\}}
 
 for any set 
 
 
 
 A
 
 
 {\displaystyle A}
 
, but this is more conveniently written as 
 
 
 
 
 {
 
 F
 
 
 (
 x
 )
 
 :
 x
 ∈
 A
 
 }
 
 
 
 {\displaystyle \left\{F\!\left(x\right):x\in A\right\}}
 
. Then, if 
 
 
 
 A
 
 
 {\displaystyle A}
 
 is a set and 
 
 
 
 F
 
 
 {\displaystyle F}
 
 is any functional relation, the <a href="/facts/Axiom_of_replacement/dmJn0BaS">Axiom of Replacement</a> assures that 
 
 
 
 F
 
 [
 A
 ]
 
 
 
 {\displaystyle F\left[A\right]}
 
 is a set in <a href="/facts/ZFC/UYIsPbXw">ZFC</a>. In NFU, 
 
 
 
 F
 
 [
 A
 ]
 
 
 
 {\displaystyle F\left[A\right]}
 
 and 
 
 
 
 A
 
 
 {\displaystyle A}
 
 now have the same type, and 
 
 
 
 F
 
 
 {\displaystyle F}
 
 is two types higher than 
 
 
 
 F
 
 [
 A
 ]
 
 
 
 {\displaystyle F\left[A\right]}
 
 (the same type, if a type-level ordered pair is used).
The function 
 
 
 
 I
 
 
 {\displaystyle I}
 
 such that 
 
 
 
 I
 
 
 (
 x
 )
 
 =
 x
 
 
 {\displaystyle I\!\left(x\right)=x}
 
 is not a set in ZFC because it is "too large". 
 
 
 
 I
 
 
 {\displaystyle I}
 
 is however a set in NFU. The function (predicate) 
 
 
 
 S
 
 
 {\displaystyle S}
 
 such that 
 
 
 
 S
 
 
 (
 x
 )
 
 =
 
 {
 x
 }
 
 
 
 {\displaystyle S\!\left(x\right)=\left\{x\right\}}
 
 is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be <a href="/facts/Stratified_formula/RXXeG04r">stratified</a>. Moreover, 
 
 
 
 S
 
 
 {\displaystyle S}
 
 can be proved not to exist in NFU (see the resolution of <a href="/facts/Cantor%2527s_paradox/hbPpKd5r">Cantor's paradox</a> in <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a>.)

<h3>Operations on functions</h3>
Let 
 
 
 
 f
 
 
 {\displaystyle f}
 
 and 
 
 
 
 g
 
 
 {\displaystyle g}
 
 be arbitrary functions. The <a href="/facts/Function_composition/r5Pvnmth">composition</a> of 
 
 
 
 f
 
 
 {\displaystyle f}
 
 and 
 
 
 
 g
 
 
 {\displaystyle g}
 
, 
 
 
 
 g
 ∘
 f
 
 
 {\displaystyle g\circ f}
 
, is defined as the relative product 
 
 
 
 f
 
 
 |
 
 
 g
 
 
 {\displaystyle f\,|\,g}
 
, but only if this results in a function such that 
 
 
 
 g
 ∘
 f
 
 
 {\displaystyle g\circ f}
 
 is also a function, with 
 
 
 
 
 (
 
 g
 ∘
 f
 
 )
 
 
 
 (
 x
 )
 
 =
 g
 
 
 (
 
 f
 
 
 (
 x
 )
 
 
 )
 
 
 
 {\displaystyle \left(g\circ f\right)\!\left(x\right)=g\!\left(f\!\left(x\right)\right)}
 
, if the range of 
 
 
 
 f
 
 
 {\displaystyle f}
 
 is a subset of the domain of 
 
 
 
 g
 
 
 {\displaystyle g}
 
. The <a href="/facts/Inverse_function/Tg5nnXlu">inverse</a> of 
 
 
 
 f
 
 
 {\displaystyle f}
 
, 
 
 
 
 
 f
 
 
 (
 
 −
 1
 
 )
 
 
 
 
 
 {\displaystyle f^{\left(-1\right)}}
 
, is defined as the <a href="/facts/Converse_relation/EVGlRSz7">converse</a> of 
 
 
 
 f
 
 
 {\displaystyle f}
 
 if this is a function. Given any set 
 
 
 
 A
 
 
 {\displaystyle A}
 
, the identity function 
 
 
 
 
 i
 
 A
 
 
 
 
 {\displaystyle i_{A}}
 
 is the set 
 
 
 
 
 {
 
 
 (
 
 x
 ,
 x
 
 )
 
 ∣
 x
 ∈
 A
 
 }
 
 
 
 {\displaystyle \left\{\left(x,x\right)\mid x\in A\right\}}
 
, and this is a set in both ZFC and NFU for different reasons.

<h3>Special kinds of function</h3>
A function 
 
 
 
 f
 
 
 {\displaystyle f}
 
 from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 is a:

<ul><li><a href="/facts/Injective_function/5ES6tqf5">Injection</a> from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 if the <a href="/facts/Image_(mathematics)/KANefMAl">images</a> under 
 
 
 
 f
 
 
 {\displaystyle f}
 
 of distinct members of 
 
 
 
 A
 
 
 {\displaystyle A}
 
 are distinct members of 
 
 
 
 B
 
 
 {\displaystyle B}
 
.</li>
<li><a href="/facts/Surjection/KezhLpCb">Surjection</a> from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 if the range of 
 
 
 
 f
 
 
 {\displaystyle f}
 
 is 
 
 
 
 B
 
 
 {\displaystyle B}
 
.</li>
<li><a href="/facts/Bijection/j4gTuTmW">Bijection</a> from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
 if 
 
 
 
 f
 
 
 {\displaystyle f}
 
 is both an injection and a surjection.</li></ul>
Defining functions as ordered pairs 
 
 
 
 (
 f
 ,
 B
 )
 
 
 {\displaystyle (f,B)}
 
 or ordered triples 
 
 
 
 (
 f
 ,
 A
 ,
 B
 )
 
 
 {\displaystyle (f,A,B)}
 
 has the advantages that we do not have to introduce the terminology of being a function "from 
 
 
 
 A
 
 
 {\displaystyle A}
 
 to 
 
 
 
 B
 
 
 {\displaystyle B}
 
", and that we can speak of "being surjective" outright as opposed to only being able to speak of "being surjective onto 
 
 
 
 B
 
 
 {\displaystyle B}
 
".

<h2 id="size-of-sets">Size of sets</h2>
In both <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>, two sets A and B are the same size (or are <a href="/facts/Equinumerous/7hMvasXx">equinumerous</a>) if and only if there is a <a href="/facts/Bijection/j4gTuTmW">bijection</a> f from A to B. This can be written as 
 
 
 
 
 |
 
 A
 
 |
 
 =
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|=|B|}
 
, but note that (for the moment) this expresses a relation between A and B rather than a relation between yet-undefined objects 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 and 
 
 
 
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |B|}
 
. Denote this relation by 
 
 
 
 A
 ∼
 B
 
 
 {\displaystyle A\sim B}
 
 in contexts such as the actual definition of the <a href="/facts/Cardinal_number/ccoKwU4R">cardinals</a> where even the appearance of presupposing abstract cardinals should be avoided.
Similarly, define 
 
 
 
 
 |
 
 A
 
 |
 
 ≤
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|\leq |B|}
 
 as holding if and only if there is an <a href="/facts/Injective_function/5ES6tqf5">injection</a> from A to B.
It is straightforward to show that the relation of equinumerousness is an <a href="/facts/Equivalence_relation/1MQ5rtkW">equivalence relation</a>: equinumerousness of A with A is witnessed by 
 
 
 
 
 i
 
 A
 
 
 
 
 {\displaystyle i_{A}}
 
; if f witnesses 
 
 
 
 
 |
 
 A
 
 |
 
 =
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|=|B|}
 
, then 
 
 
 
 
 f
 
 −
 1
 
 
 
 
 {\displaystyle f^{-1}}
 
 witnesses 
 
 
 
 
 |
 
 B
 
 |
 
 =
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |B|=|A|}
 
; and if f witnesses 
 
 
 
 
 |
 
 A
 
 |
 
 =
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|=|B|}
 
 and g witnesses 
 
 
 
 
 |
 
 B
 
 |
 
 =
 
 |
 
 C
 
 |
 
 
 
 {\displaystyle |B|=|C|}
 
, then 
 
 
 
 g
 ∘
 f
 
 
 {\displaystyle g\circ f}
 
 witnesses 
 
 
 
 
 |
 
 A
 
 |
 
 =
 
 |
 
 C
 
 |
 
 
 
 {\displaystyle |A|=|C|}
 
.
It can be shown that 
 
 
 
 
 |
 
 A
 
 |
 
 ≤
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|\leq |B|}
 
 is a <a href="/facts/Linear_order/xnTtmuYJ">linear order</a> on abstract cardinals, but not on sets. Reflexivity is obvious and transitivity is proven just as for equinumerousness. The <a href="/facts/Cantor%25E2%2580%2593Bernstein%25E2%2580%2593Schroeder_theorem/uKUbvFpo">Schröder–Bernstein theorem</a>, provable in <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> in an entirely standard way, establishes that

<ul><li>
 
 
 
 
 |
 
 A
 
 |
 
 ≤
 
 |
 
 B
 
 |
 
 ∧
 
 |
 
 B
 
 |
 
 ≤
 
 |
 
 A
 
 |
 
 →
 
 |
 
 A
 
 |
 
 =
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|\leq |B|\wedge |B|\leq |A|\rightarrow |A|=|B|}
 
</li></ul>
(this establishes antisymmetry on cardinals), and

<ul><li>
 
 
 
 
 |
 
 A
 
 |
 
 ≤
 
 |
 
 B
 
 |
 
 ∨
 
 |
 
 B
 
 |
 
 ≤
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|\leq |B|\vee |B|\leq |A|}
 
</li></ul>
follows in a standard way in either theory from the <a href="/facts/Axiom_of_choice/1Ura2HTh">axiom of choice</a>.

<h2 id="finite-sets-and-natural-numbers">Finite sets and natural numbers</h2>
Natural numbers can be considered either as finite ordinals or finite cardinals. Here consider them as finite cardinal numbers. This is the first place where a major difference between the implementations in <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> becomes evident.
The Axiom of Infinity of ZFC tells us that there is a set A which contains 
 
 
 
 ∅
 
 
 {\displaystyle \emptyset }
 
 and contains 
 
 
 
 y
 ∪
 {
 y
 }
 
 
 {\displaystyle y\cup \{y\}}
 
 for each 
 
 
 
 y
 ∈
 A
 
 
 {\displaystyle y\in A}
 
. This set A is not uniquely determined (it can be made larger while preserving this closure property): the set N of natural numbers is

<ul><li>
 
 
 
 {
 x
 ∈
 A
 ∣
 ∀
 B
 
 (
 ∅
 ∈
 B
 ∧
 ∀
 y
 
 (
 y
 ∈
 B
 →
 y
 ∪
 {
 y
 }
 ∈
 B
 )
 →
 x
 ∈
 B
 )
 }
 
 
 {\displaystyle \{x\in A\mid \forall B\,(\emptyset \in B\wedge \forall y\,(y\in B\rightarrow y\cup \{y\}\in B)\rightarrow x\in B)\}}
 
</li></ul>
which is the intersection of all sets which contain the empty set and are closed under the "successor" operation 
 
 
 
 y
 ↦
 y
 ∪
 {
 y
 }
 
 
 {\displaystyle y\mapsto y\cup \{y\}}
 
.
In ZFC, a set 
 
 
 
 A
 
 
 {\displaystyle A}
 
 is finite if and only if there is 
 
 
 
 n
 ∈
 N
 
 
 {\displaystyle n\in N}
 
 such that 
 
 
 
 
 |
 
 n
 
 |
 
 =
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |n|=|A|}
 
: further, define 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 as this n for finite A. (It can be proved that no two distinct natural numbers are the same size).
The usual operations of arithmetic can be defined recursively and in a style very similar to that in which the set of natural numbers itself is defined. For example, + (the addition operation on natural numbers) can be defined as the smallest set which contains 
 
 
 
 (
 (
 x
 ,
 ∅
 )
 ,
 x
 )
 
 
 {\displaystyle ((x,\emptyset ),x)}
 
 for each natural number 
 
 
 
 x
 
 
 {\displaystyle x}
 
 and contains 
 
 
 
 (
 (
 x
 ,
 y
 ∪
 {
 y
 }
 )
 ,
 z
 ∪
 {
 z
 }
 )
 
 
 {\displaystyle ((x,y\cup \{y\}),z\cup \{z\})}
 
 whenever it contains 
 
 
 
 (
 (
 x
 ,
 y
 )
 ,
 z
 )
 
 
 {\displaystyle ((x,y),z)}
 
.
In NFU, it is not obvious that this approach can be used, since the successor operation 
 
 
 
 y
 ∪
 {
 y
 }
 
 
 {\displaystyle y\cup \{y\}}
 
 is unstratified and so the set N as defined above cannot be shown to exist in NFU (it is consistent for the set of finite von Neumann ordinals to exist in NFU, but this strengthens the theory, as the existence of this set implies the Axiom of Counting (for which see below or the <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> article)).
The standard definition of the natural numbers, which is actually the oldest <a href="/facts/Set-theoretic_definition_of_natural_numbers/pdr0WSDC">set-theoretic definition of natural numbers</a>, is as equivalence classes of finite sets under equinumerousness. Essentially the same definition is appropriate to <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> (this is not the usual definition, but the results are the same): define Fin, the set of finite sets, as

{
        A
        ∣
        ∀
        F
        
        (
        ∅
        ∈
        F
        ∧
        ∀
        x
        ,
        y
        
        (
        x
        ∈
        F
        →
        x
        ∪
        {
        y
        }
        ∈
        F
        )
        →
        A
        ∈
        F
        )
        }
      
    
    {\displaystyle \{A\mid \forall F\,(\emptyset \in F\wedge \forall x,y\,(x\in F\rightarrow x\cup \{y\}\in F)\rightarrow A\in F)\}}

For any set 
 
 
 
 A
 ∈
 F
 i
 n
 
 
 {\displaystyle A\in Fin}
 
, define 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 as 
 
 
 
 {
 B
 ∣
 A
 ∼
 B
 }
 
 
 {\displaystyle \{B\mid A\sim B\}}
 
. Define N as the set 
 
 
 
 {
 
 |
 
 A
 
 |
 
 ∣
 A
 ∈
 F
 i
 n
 }
 
 
 {\displaystyle \{|A|\mid A\in Fin\}}
 
.
The Axiom of Infinity of NFU can be expressed as 
 
 
 
 V
 ∉
 F
 i
 n
 
 
 {\displaystyle V\not \in Fin}
 
: this is enough to establish that each natural number has a nonempty successor (the successor of 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 being 
 
 
 
 
 |
 
 A
 ∪
 {
 x
 }
 
 |
 
 
 
 {\displaystyle |A\cup \{x\}|}
 
 for any 
 
 
 
 x
 ∉
 A
 
 
 {\displaystyle x\not \in A}
 
) which is the hard part of showing that the Peano axioms of arithmetic are satisfied.
The operations of arithmetic can be defined in a style similar to the style given above (using the definition of successor just given). They can also be defined in a natural set theoretical way: if A and B are disjoint finite sets, define |A|+|B| as 
 
 
 
 
 |
 
 A
 ∪
 B
 
 |
 
 
 
 {\displaystyle |A\cup B|}
 
. More formally, define m+n for m and n in N as

{
        A
        ∣
        ∃
        B
        ,
        C
        
        (
        B
        ∈
        m
        ∧
        C
        ∈
        n
        ∧
        B
        ∩
        C
        =
        ∅
        ∧
        A
        =
        B
        ∪
        C
        )
        }
      
    
    {\displaystyle \{A\mid \exists B,C\,(B\in m\wedge C\in n\wedge B\cap C=\emptyset \wedge A=B\cup C)\}}

(But note that this style of definition is feasible for the ZFC numerals as well, but more circuitous: the form of the <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> definition facilitates set manipulations while the form of the ZFC definition facilitates recursive definitions, but either theory supports either style of definition).
The two implementations are quite different. In ZFC, choose a <a href="/facts/Representative_(mathematics)/1d2sh0TB">representative</a> of each finite cardinality (the equivalence classes themselves are too large to be sets); in NFU the equivalence classes themselves are sets, and are thus an obvious choice for objects to stand in for the cardinalities. However, the arithmetic of the two theories is identical: the same abstraction is implemented by these two superficially different approaches.

<h2 id="equivalence-relations-and-partitions">Equivalence relations and partitions</h2>
A general technique for implementing abstractions in set theory is the use of equivalence classes. If an equivalence relation R tells us that elements of its field A are alike in some particular respect, then for any set x, regard the set 
 
 
 
 [
 x
 
 ]
 
 R
 
 
 =
 {
 y
 ∈
 A
 ∣
 x
 R
 y
 }
 
 
 {\displaystyle [x]_{R}=\{y\in A\mid xRy\}}
 
 as representing an abstraction from the set x respecting just those features (identify elements of A <a href="/facts/Up_to/ydz4ztzX">up to</a> R).
For any set A, a set 
 
 
 
 P
 
 
 {\displaystyle P}
 
 is a partition of A if all elements of P are nonempty, any two distinct elements of P are disjoint, and 
 
 
 
 A
 =
 ⋃
 P
 
 
 {\displaystyle A=\bigcup P}
 
.
For every equivalence relation R with field A, 
 
 
 
 {
 [
 x
 
 ]
 
 R
 
 
 ∣
 x
 ∈
 A
 }
 
 
 {\displaystyle \{[x]_{R}\mid x\in A\}}
 
 is a partition of A. Moreover, each partition P of A determines an equivalence relation 
 
 
 
 {
 (
 x
 ,
 y
 )
 ∣
 ∃
 A
 ∈
 P
 
 (
 x
 ∈
 A
 ∧
 y
 ∈
 A
 )
 }
 
 
 {\displaystyle \{(x,y)\mid \exists A\in P\,(x\in A\wedge y\in A)\}}
 
.
This technique has limitations in both <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>. In ZFC, since the universe is not a set, it seems possible to abstract features only from elements of small domains. This can be circumvented using a trick due to <a href="/facts/Dana_Scott/XEVddlVg">Dana Scott</a>: if R is an equivalence relation on the universe, define 
 
 
 
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle [x]_{R}}
 
 as the set of all y such that 
 
 
 
 y
 R
 x
 
 
 {\displaystyle yRx}
 
 and the <a href="/facts/Rank_(set_theory)/EhkJAxXc">rank</a> of y is less than or equal to the rank of any 
 
 
 
 z
 R
 x
 
 
 {\displaystyle zRx}
 
. This works because the ranks are sets. Of course, there still may be a proper class of 
 
 
 
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle [x]_{R}}
 
's. In NFU, the main difficulty is that 
 
 
 
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle [x]_{R}}
 
 is one type higher than x, so for example the "map" 
 
 
 
 x
 ↦
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle x\mapsto [x]_{R}}
 
 is not in general a (set) function (though 
 
 
 
 {
 x
 }
 ↦
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle \{x\}\mapsto [x]_{R}}
 
 is a set). This can be circumvented by the use of the Axiom of Choice to select a representative from each equivalence class to replace 
 
 
 
 [
 x
 
 ]
 
 R
 
 
 
 
 {\displaystyle [x]_{R}}
 
, which will be at the same type as x, or by choosing a canonical representative if there is a way to do this without invoking Choice (the use of representatives is hardly unknown in ZFC, either). In NFU, the use of equivalence class constructions to abstract properties of general sets is more common, as for example in the definitions of cardinal and ordinal number below.

<h2 id="ordinal-numbers">Ordinal numbers</h2>
Two well-orderings 
 
 
 
 
 W
 
 1
 
 
 
 
 {\displaystyle W_{1}}
 
 and 
 
 
 
 
 W
 
 2
 
 
 
 
 {\displaystyle W_{2}}
 
 are similar and write 
 
 
 
 
 W
 
 1
 
 
 ∼
 
 W
 
 2
 
 
 
 
 {\displaystyle W_{1}\sim W_{2}}
 
 just in case there is a bijection f from the field of 
 
 
 
 
 W
 
 1
 
 
 
 
 {\displaystyle W_{1}}
 
 to the field of 
 
 
 
 
 W
 
 2
 
 
 
 
 {\displaystyle W_{2}}
 
 such that 
 
 
 
 x
 
 W
 
 1
 
 
 y
 ↔
 f
 (
 x
 )
 
 W
 
 2
 
 
 f
 (
 y
 )
 
 
 {\displaystyle xW_{1}y\leftrightarrow f(x)W_{2}f(y)}
 
 for all x and y.
Similarity is shown to be an equivalence relation in much the same way that equinumerousness was shown to be an equivalence relation above.
In <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> (NFU), the order type of a well-ordering W is the set of all well-orderings which are similar to W. The set of ordinal numbers is the set of all order types of well-orderings.
This does not work in <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, because the equivalence classes are too large. It would be formally possible to use <a href="/facts/Scott%2527s_trick/Xf8RQHLE">Scott's trick</a> to define the ordinals in essentially the same way, but a device of <a href="/facts/John_von_Neumann/aUk6urof">von Neumann</a> is more commonly used.
For any partial order 
 
 
 
 ≤
 
 
 {\displaystyle \leq }
 
, the corresponding strict partial order < is defined as 
 
 
 
 {
 (
 x
 ,
 y
 )
 ∣
 x
 ≤
 y
 ∧
 x
 ≠
 y
 }
 
 
 {\displaystyle \{(x,y)\mid x\leq y\wedge x\neq y\}}
 
. Strict linear orders and strict well-orderings are defined similarly.
A set A is said to be transitive if 
 
 
 
 ⋃
 A
 ⊆
 A
 
 
 {\displaystyle \bigcup A\subseteq A}
 
: each element of an element of A is also an element of A. A (von Neumann) ordinal is a transitive set on which membership is a strict well-ordering.
In ZFC, the order type of a well-ordering W is then defined as the unique von Neumann ordinal which is equinumerous with the field of W and membership on which is isomorphic to the strict well-ordering associated with W. (the equinumerousness condition distinguishes between well-orderings with fields of size 0 and 1, whose associated strict well-orderings are indistinguishable).
In ZFC there cannot be a set of all ordinals. In fact, the von Neumann ordinals are an inconsistent totality in any set theory: it can be shown with modest set theoretical assumptions that every element of a von Neumann ordinal is a von Neumann ordinal and the von Neumann ordinals are strictly well-ordered by membership. It follows that the class of von Neumann ordinals would be a von Neumann ordinal if it were a set: but it would then be an element of itself, which contradicts the fact that membership is a strict well-ordering of the von Neumann ordinals.
The existence of order types for all well-orderings is not a theorem of <a href="/facts/Zermelo_set_theory/o3fzd9nl">Zermelo set theory</a>: it requires the <a href="/facts/Axiom_of_replacement/dmJn0BaS">Axiom of replacement</a>. Even Scott's trick cannot be used in Zermelo set theory without an additional assumption (such as the assumption that every set belongs to a <a href="/facts/Rank_(set_theory)/EhkJAxXc">rank</a> which is a set, which does not essentially
strengthen Zermelo set theory but is not a theorem of that theory).
In NFU, the collection of all ordinals is a set by stratified comprehension. The Burali-Forti paradox is evaded in an unexpected way. There is a natural order on the ordinals defined by 
 
 
 
 α
 ≤
 β
 
 
 {\displaystyle \alpha \leq \beta }
 
 if and only if some (and so any) 
 
 
 
 
 W
 
 1
 
 
 ∈
 α
 
 
 {\displaystyle W_{1}\in \alpha }
 
 is similar to an initial segment of some (and so any) 
 
 
 
 
 W
 
 2
 
 
 ∈
 β
 
 
 {\displaystyle W_{2}\in \beta }
 
. Further, it can be shown that this natural order is a well-ordering of the ordinals and so must have an order type 
 
 
 
 Ω
 
 
 {\displaystyle \Omega }
 
. It would seem that the order type of the ordinals less than

Ω
 
 
 {\displaystyle \Omega }
 
 with the natural order would be 
 
 
 
 Ω
 
 
 {\displaystyle \Omega }
 
, contradicting the fact that 
 
 
 
 Ω
 
 
 {\displaystyle \Omega }
 
 is the order type of the entire natural order on the ordinals (and so not of any of its proper initial segments). But this relies on one's intuition (correct in ZFC) that the order type of the natural order on the ordinals less than 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 is 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 for any ordinal 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
. This assertion is unstratified, because the type of the second 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 is four higher than the type of the first (two higher if a type level pair is used). The assertion which is true and provable in NFU is that the order type of the natural order on the ordinals less than 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 is 
 
 
 
 
 T
 
 4
 
 
 (
 α
 )
 
 
 {\displaystyle T^{4}(\alpha )}
 
 for any ordinal 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
, where 
 
 
 
 T
 (
 α
 )
 
 
 {\displaystyle T(\alpha )}
 
 is the order type of 
 
 
 
 
 W
 
 ι
 
 
 =
 {
 (
 {
 x
 }
 ,
 {
 y
 }
 )
 ∣
 x
 W
 y
 }
 
 
 {\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}
 
 for any 
 
 
 
 W
 ∈
 α
 
 
 {\displaystyle W\in \alpha }
 
 (it is easy to show that this does not depend on the choice of W; note that T raises type by one). Thus the order type of the ordinals less than 
 
 
 
 Ω
 
 
 {\displaystyle \Omega }
 
 with the natural order is 
 
 
 
 
 T
 
 4
 
 
 (
 Ω
 )
 
 
 {\displaystyle T^{4}(\Omega )}
 
, and 
 
 
 
 
 T
 
 4
 
 
 (
 Ω
 )
 <
 Ω
 
 
 {\displaystyle T^{4}(\Omega )<\Omega }
 
. All uses of 
 
 
 
 
 T
 
 4
 
 
 
 
 {\displaystyle T^{4}}
 
 here can be replaced with 
 
 
 
 
 T
 
 2
 
 
 
 
 {\displaystyle T^{2}}
 
 if a type-level pair is used.
This shows that the T operation is nontrivial, which has a number of consequences. It follows immediately that the singleton map 
 
 
 
 x
 ↦
 {
 x
 }
 
 
 {\displaystyle x\mapsto \{x\}}
 
 is not a set, as otherwise restrictions of this map would establish the similarity of W and 
 
 
 
 
 W
 
 ι
 
 
 
 
 {\displaystyle W^{\iota }}
 
 for any well-ordering W. T is (externally) bijective and order-preserving. Because of this, the fact 
 
 
 
 
 T
 
 4
 
 
 (
 Ω
 )
 <
 Ω
 
 
 {\displaystyle T^{4}(\Omega )<\Omega }
 
 establishes that 
 
 
 
 Ω
 >
 T
 (
 Ω
 )
 >
 
 T
 
 2
 
 
 (
 Ω
 )
 …
 
 
 {\displaystyle \Omega >T(\Omega )>T^{2}(\Omega )\ldots }
 
 is a "descending sequence" in the ordinals which cannot be a set.
Ordinals fixed by T are called Cantorian ordinals, and ordinals which dominate only cantorian ordinals (which are easily shown to be cantorian themselves) are said to be strongly cantorian. There can be no set of cantorian ordinals or set of strongly cantorian ordinals.

<h3>Digression: von Neumann ordinals in NFU</h3>
It is possible to reason about von Neumann ordinals in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>. Recall that a von Neumann ordinal is a transitive set A such that the restriction of membership to A is a strict well-ordering. This is quite a strong condition in the NFU context, since the membership relation involves a difference of type. A von Neumann ordinal A is not an ordinal in the sense of NFU, but 
 
 
 
 ∈
 ⌈
 A
 
 
 {\displaystyle \in \lceil A}
 
 belongs to an ordinal 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 which may be termed the order type of (membership on) A. It is easy to show that the order type of a von Neumann ordinal A is cantorian: for any well-ordering W of order type 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
, the induced well-ordering of initial segments of W by inclusion has order type 
 
 
 
 T
 (
 α
 )
 
 
 {\displaystyle T(\alpha )}
 
 (it is one type higher, thus the application of T): but the order types of the well-ordering of a von Neumann ordinal A by membership and the well-ordering of its initial segments by inclusion are clearly the same because the two well-orderings are actually the same relation, so the order type of A is fixed under T. Moreover, the same argument applies to any smaller ordinal (which will be the order type of an initial segment of A, also a von Neumann ordinal) so the order type of any von Neumann ordinal is strongly cantorian.
The only von Neumann ordinals which can be shown to exist in NFU without additional assumptions are the concrete finite ones. However, the application of a permutation method can convert any model of NFU to a model in which every strongly cantorian ordinal is the order type of a von Neumann ordinal. This suggests that the concept "strongly cantorian ordinal of NFU" might be a better analogue to "ordinal of ZFC" than is the apparent analogue "ordinal of NFU".

<h2 id="cardinal-numbers">Cardinal numbers</h2>
Cardinal numbers are defined in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> in a way which generalizes the definition of natural
number: for any set A, 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 
 =
 
 d
 e
 f
 
 
 
 
 {
 
 B
 ∣
 B
 ∼
 A
 
 }
 
 
 
 {\displaystyle |A|\,{\overset {\mathrm {def} }{=}}\left\{B\mid B\sim A\right\}}
 
.
In <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, these equivalence classes are too large as usual. Scott's trick could be used (and indeed is used in <a href="/facts/Zermelo%25E2%2580%2593Fraenkel_set_theory/UYIsPbXw">ZF</a>), 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 is usually defined as the smallest order type (here a von Neumann ordinal) of a well-ordering of A (that every set can be well-ordered follows from
the Axiom of Choice in the usual way in both theories).
The natural order on cardinal numbers is seen to be a well-ordering: that it is reflexive, antisymmetric (on abstract cardinals, which are now available) and transitive has been shown above. That it is a linear order follows from the Axiom of Choice: well-order two sets and an 
initial segment of one well-ordering will be isomorphic to the other, so one set will have cardinality smaller than that of the other. That it is a well-ordering follows from the Axiom of Choice in a similar way.
With each infinite cardinal, many order types are associated for the usual reasons (in either set theory).
Cantor's theorem shows (in both theories) that there are nontrivial distinctions between infinite cardinal numbers. In <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, one proves 
 
 
 
 
 |
 
 A
 
 |
 
 <
 
 |
 
 P
 (
 A
 )
 
 |
 
 .
 
 
 {\displaystyle |A|<|P(A)|.}
 
 In <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>, the usual form of Cantor's theorem is false (consider the case A=V), but Cantor's theorem is an ill-typed statement. The correct form of the theorem in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> is 
 
 
 
 
 |
 
 
 P
 
 1
 
 
 (
 A
 )
 
 |
 
 <
 
 |
 
 P
 (
 A
 )
 
 |
 
 
 
 {\displaystyle |P_{1}(A)|<|P(A)|}
 
, where 
 
 
 
 
 P
 
 1
 
 
 (
 A
 )
 
 
 {\displaystyle P_{1}(A)}
 
 is the set of one-element subsets of A. 
 
 
 
 
 |
 
 
 P
 
 1
 
 
 (
 V
 )
 
 |
 
 <
 
 |
 
 P
 (
 V
 )
 
 |
 
 
 
 {\displaystyle |P_{1}(V)|<|P(V)|}
 
 shows that there are "fewer" singletons than sets (the obvious bijection 
 
 
 
 x
 ↦
 {
 x
 }
 
 
 {\displaystyle x\mapsto \{x\}}
 
 from 
 
 
 
 
 P
 
 1
 
 
 (
 V
 )
 
 
 {\displaystyle P_{1}(V)}
 
 to V has already been seen not to be a set). It is actually provable in NFU + Choice that 
 
 
 
 
 |
 
 
 P
 
 1
 
 
 (
 V
 )
 
 |
 
 <
 
 |
 
 P
 (
 V
 )
 
 |
 
 ≪
 
 |
 
 V
 
 |
 
 
 
 {\displaystyle |P_{1}(V)|<|P(V)|\ll |V|}
 
 (where 
 
 
 
 ≪
 
 
 {\displaystyle \ll }
 
 signals the existence of many intervening cardinals; there are many, many urelements!). Define a type-raising T operation on cardinals analogous to the T operation on ordinals: 
 
 
 
 T
 (
 
 |
 
 A
 
 |
 
 )
 =
 
 |
 
 
 P
 
 1
 
 
 (
 A
 )
 
 |
 
 
 
 {\displaystyle T(|A|)=|P_{1}(A)|}
 
; this is an external endomorphism of the cardinals just as the T operation on ordinals is an external endomorphism of the ordinals.
A set A is said to be cantorian just in case 
 
 
 
 
 |
 
 A
 
 |
 
 =
 
 |
 
 
 P
 
 1
 
 
 (
 A
 )
 
 |
 
 =
 T
 (
 
 |
 
 A
 
 |
 
 )
 
 
 {\displaystyle |A|=|P_{1}(A)|=T(|A|)}
 
; the cardinal 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
 is also said to be a cantorian cardinal. A set A is said to be strongly cantorian (and its cardinal to be strongly cantorian as well) just in case the restriction of the singleton map to A (
 
 
 
 (
 x
 ↦
 {
 x
 }
 )
 ⌈
 A
 
 
 {\displaystyle (x\mapsto \{x\})\lceil A}
 
) is a set. Well-orderings of strongly cantorian sets are always strongly cantorian ordinals; this is not always true of well-orderings of cantorian sets (though the shortest well-ordering of a cantorian set will be cantorian). A cantorian set is a set which satisfies the usual form of Cantor's theorem.
The operations of cardinal arithmetic are defined in a set-theoretically motivated way in both theories. 
 
 
 
 
 |
 
 A
 
 |
 
 +
 
 |
 
 B
 
 |
 
 =
 {
 C
 ∪
 D
 ∣
 C
 ∼
 A
 ∧
 D
 ∼
 B
 ∧
 C
 ∩
 D
 =
 ∅
 }
 
 
 {\displaystyle |A|+|B|=\{C\cup D\mid C\sim A\wedge D\sim B\wedge C\cap D=\emptyset \}}
 
. One would like to define 
 
 
 
 
 |
 
 A
 
 |
 
 ⋅
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|\cdot |B|}
 
 as 
 
 
 
 
 |
 
 A
 ×
 B
 
 |
 
 
 
 {\displaystyle |A\times B|}
 
, and one does this in <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, but there is an obstruction in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> when using the Kuratowski pair: one defines 
 
 
 
 
 |
 
 A
 
 |
 
 ⋅
 
 |
 
 B
 
 |
 
 
 
 {\displaystyle |A|\cdot |B|}
 
 as 
 
 
 
 
 T
 
 −
 2
 
 
 (
 
 |
 
 A
 ×
 B
 
 |
 
 )
 
 
 {\displaystyle T^{-2}(|A\times B|)}
 
 because of the type displacement of 2 between the pair and its projections, which implies a type displacement of two between a cartesian product and its factors. It is straightforward to prove that the product always exists (but requires attention because the inverse of T is not total).
Defining the exponential operation on cardinals requires T in an essential way: if 
 
 
 
 
 B
 
 A
 
 
 
 
 {\displaystyle B^{A}}
 
 was defined as the collection of functions from A to B, this is three types higher than A or B, so it is reasonable to define 
 
 
 
 
 |
 
 B
 
 
 |
 
 
 
 |
 
 A
 
 |
 
 
 
 
 
 {\displaystyle |B|^{|A|}}
 
 as 
 
 
 
 
 T
 
 −
 3
 
 
 (
 
 |
 
 
 B
 
 A
 
 
 
 |
 
 )
 
 
 {\displaystyle T^{-3}(|B^{A}|)}
 
 so that it is the same type as A or B (
 
 
 
 
 T
 
 −
 1
 
 
 
 
 {\displaystyle T^{-1}}
 
 replaces 
 
 
 
 
 T
 
 −
 3
 
 
 
 
 {\displaystyle T^{-3}}
 
 with type-level pairs). An effect of this is that the exponential operation is partial: for example, 
 
 
 
 
 2
 
 
 |
 
 V
 
 |
 
 
 
 
 
 {\displaystyle 2^{|V|}}
 
 is undefined. In <a href="/facts/ZFC/UYIsPbXw">ZFC</a> one defines 
 
 
 
 
 |
 
 B
 
 
 |
 
 
 
 |
 
 A
 
 |
 
 
 
 
 
 {\displaystyle |B|^{|A|}}
 
 as 
 
 
 
 
 |
 
 
 B
 
 A
 
 
 
 |
 
 
 
 {\displaystyle |B^{A}|}
 
 without difficulty.
The exponential operation is total and behaves exactly as expected on cantorian cardinals, since T fixes such cardinals and it is easy to show that a function space between cantorian sets is cantorian (as are power sets, cartesian products, and other usual type constructors). This offers further encouragement to the view that the "standard" cardinalities in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> are the cantorian (indeed, the strongly cantorian) cardinalities, just as the "standard" ordinals seem to be the strongly cantorian ordinals.
Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including 
 
 
 
 κ
 ⋅
 κ
 =
 κ
 
 
 {\displaystyle \kappa \cdot \kappa =\kappa }
 
. From the case 
 
 
 
 
 |
 
 V
 
 |
 
 ⋅
 
 |
 
 V
 
 |
 
 =
 
 |
 
 V
 
 |
 
 
 
 {\displaystyle |V|\cdot |V|=|V|}
 
 the existence of a type level ordered pair can be derived: 
 
 
 
 
 |
 
 V
 
 |
 
 ⋅
 
 |
 
 V
 
 |
 
 =
 
 T
 
 −
 2
 
 
 (
 
 |
 
 V
 ×
 V
 
 |
 
 )
 
 
 {\displaystyle |V|\cdot |V|=T^{-2}(|V\times V|)}
 
 is equal to 
 
 
 
 
 |
 
 V
 
 |
 
 
 
 {\displaystyle |V|}
 
 just in case 
 
 
 
 
 |
 
 V
 ×
 V
 
 |
 
 =
 
 T
 
 2
 
 
 (
 
 |
 
 V
 
 |
 
 )
 =
 
 |
 
 
 P
 
 1
 
 
 2
 
 
 (
 V
 )
 
 |
 
 
 
 {\displaystyle |V\times V|=T^{2}(|V|)=|P_{1}^{2}(V)|}
 
, which would be witnessed by a one-to-one correspondence between Kuratowski pairs 
 
 
 
 (
 a
 ,
 b
 )
 
 
 {\displaystyle (a,b)}
 
 and double singletons 
 
 
 
 {
 {
 c
 }
 }
 
 
 {\displaystyle \{\{c\}\}}
 
: redefine 
 
 
 
 (
 a
 ,
 b
 )
 
 
 {\displaystyle (a,b)}
 
 as the c such that 
 
 
 
 {
 {
 c
 }
 }
 
 
 {\displaystyle \{\{c\}\}}
 
 is associated with the Kuratowski 
 
 
 
 (
 a
 ,
 b
 )
 
 
 {\displaystyle (a,b)}
 
: this is a type-level notion of ordered pair.

<h2 id="the-axiom-of-counting-and-subversion-of-stratification">The Axiom of Counting and subversion of stratification</h2>
So there are two different implementations of the natural numbers in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> (though they are the same in <a href="/facts/ZFC/UYIsPbXw">ZFC</a>): finite ordinals and finite cardinals. Each of these supports a T operation in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> (basically the same operation). It is easy to prove that 
 
 
 
 T
 (
 n
 )
 
 
 {\displaystyle T(n)}
 
 is a natural number if n is a natural number in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> + Infinity + Choice (and so 
 
 
 
 
 |
 
 N
 
 |
 
 
 
 {\displaystyle |N|}
 
 and the first
infinite ordinal 
 
 
 
 ω
 
 
 {\displaystyle \omega }
 
 are cantorian) but it is not possible to prove in this theory that 
 
 
 
 T
 (
 n
 )
 =
 n
 
 
 {\displaystyle T(n)=n}
 
. However, common sense indicates that this should be true, and so it can be adopted as an axiom:

<ul><li>Rosser's Axiom of Counting: For each natural number n, 
 
 
 
 T
 (
 n
 )
 =
 n
 
 
 {\displaystyle T(n)=n}
 
.</li></ul>
One natural consequence of this axiom (and indeed its original formulation) is

<ul><li>
 
 
 
 
 |
 
 {
 1
 ,
 …
 ,
 n
 }
 
 |
 
 =
 n
 
 
 {\displaystyle |\{1,\ldots ,n\}|=n}
 
 for each natural number n.</li></ul>
All that can be proved in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> without Counting is 
 
 
 
 
 |
 
 {
 1
 ,
 …
 ,
 n
 }
 
 |
 
 =
 
 T
 
 2
 
 
 (
 n
 )
 
 
 {\displaystyle |\{1,\ldots ,n\}|=T^{2}(n)}
 
.
A consequence of Counting is that N is a strongly cantorian set (again, this is an equivalent assertion).

<h3>Properties of strongly cantorian sets</h3>
The type of any variable restricted to a strongly cantorian set A can be raised or lowered as desired by replacing references to 
 
 
 
 a
 ∈
 A
 
 
 {\displaystyle a\in A}
 
 with references to 
 
 
 
 ⋃
 f
 (
 a
 )
 
 
 {\displaystyle \bigcup f(a)}
 
 (type of a raised; this presupposes that it is known that a is a set; otherwise one must say "the element of 
 
 
 
 f
 (
 a
 )
 
 
 {\displaystyle f(a)}
 
" to get this effect) or 
 
 
 
 
 f
 
 −
 1
 
 
 (
 {
 a
 }
 )
 
 
 {\displaystyle f^{-1}(\{a\})}
 
 (type of a lowered) where 
 
 
 
 f
 (
 a
 )
 =
 {
 a
 }
 
 
 {\displaystyle f(a)=\{a\}}
 
 for all 
 
 
 
 a
 ∈
 A
 
 
 {\displaystyle a\in A}
 
, so it is not necessary to assign types to such variables for purposes of stratification.
Any subset of a strongly cantorian set is strongly cantorian. The power set of a strongly cantorian set is strongly cantorian. The cartesian product of two strongly cantorian sets is strongly cantorian.
Introducing the Axiom of Counting means that types need not be assigned to variables restricted to N or to P(N), R (the set of reals) or indeed any set ever considered in classical mathematics outside of set theory.
There are no analogous phenomena in <a href="/facts/ZFC/UYIsPbXw">ZFC</a>. See the main <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> article for stronger axioms that can be adjoined to NFU to enforce "standard" behavior of familiar mathematical objects.

<h2 id="familiar-number-systems-positive-rationals-magnitudes-and-reals">Familiar number systems: positive rationals, magnitudes, and reals</h2>
Represent positive fractions as pairs of positive natural numbers (0 is excluded): 
 
 
 
 
 
 p
 q
 
 
 
 
 {\displaystyle {\frac {p}{q}}}
 
 is represented by the pair 
 
 
 
 (
 p
 ,
 q
 )
 
 
 {\displaystyle (p,q)}
 
. To make 
 
 
 
 
 
 p
 q
 
 
 =
 
 
 r
 s
 
 
 ↔
 p
 s
 =
 q
 r
 
 
 {\displaystyle {\frac {p}{q}}={\frac {r}{s}}\leftrightarrow ps=qr}
 
, introduce the relation 
 
 
 
 ∼
 
 
 {\displaystyle \sim }
 
 defined by 
 
 
 
 (
 p
 ,
 q
 )
 ∼
 (
 r
 ,
 s
 )
 ↔
 p
 s
 =
 q
 r
 
 
 {\displaystyle (p,q)\sim (r,s)\leftrightarrow ps=qr}
 
. It is provable that this is an equivalence relation: define positive rational numbers as equivalence classes of pairs of positive natural numbers under this relation. Arithmetic operations on positive rational numbers and the order relation on positive rationals are defined just as in elementary school and proved (with some effort) to have the expected properties.
Represent magnitudes (positive reals) as nonempty proper initial segments of the positive rationals with no largest element. The operations of addition and multiplication on magnitudes are implemented by elementwise addition of the positive rational elements of the magnitudes. Order is implemented as set inclusion.
Represent real numbers as differences 
 
 
 
 m
 −
 n
 
 
 {\displaystyle m-n}
 
 of magnitudes: formally speaking, a real number is an equivalence class of pairs 
 
 
 
 (
 m
 ,
 n
 )
 
 
 {\displaystyle (m,n)}
 
 of magnitudes under the equivalence relation 
 
 
 
 ∼
 
 
 {\displaystyle \sim }
 
 defined by 
 
 
 
 (
 m
 ,
 n
 )
 ∼
 (
 r
 ,
 s
 )
 ↔
 m
 +
 s
 =
 n
 +
 r
 
 
 {\displaystyle (m,n)\sim (r,s)\leftrightarrow m+s=n+r}
 
. The operations of addition and multiplication on real numbers are defined just as one would expect from the algebraic rules for adding and multiplying differences. The treatment of order is also as in elementary algebra.
This is the briefest sketch of the constructions. Note that the constructions are exactly the same in <a href="/facts/ZFC/UYIsPbXw">ZFC</a> and in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>, except for the difference in the constructions of the natural numbers: since all variables are restricted to strongly cantorian sets, there is no need to worry about stratification restrictions. Without the Axiom of Counting, it might be necessary to introduce some applications of T in a full discussion of these constructions.

<h2 id="operations-on-indexed-families-of-sets">Operations on indexed families of sets</h2>
In this class of constructions it appears that <a href="/facts/ZFC/UYIsPbXw">ZFC</a> has an advantage over <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>: though the constructions are clearly feasible in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>, they are more complicated than in ZFC for reasons having to do with stratification.
Throughout this section assume a type-level ordered pair. Define 
 
 
 
 (
 
 x
 
 1
 
 
 ,
 
 x
 
 2
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 )
 
 
 {\displaystyle (x_{1},x_{2},\ldots ,x_{n})}
 
 as 
 
 
 
 (
 
 x
 
 1
 
 
 ,
 (
 
 x
 
 2
 
 
 ,
 …
 ,
 
 x
 
 n
 
 
 )
 )
 
 
 {\displaystyle (x_{1},(x_{2},\ldots ,x_{n}))}
 
. The definition of the general n-tuple using the Kuratowski pair is trickier, as one needs to keep the types of all the projections the same, and the type displacement between the n-tuple and its projections increases as n increases. Here, the n-tuple has the same type as each of its projections.
General cartesian products are defined similarly: 
 
 
 
 
 A
 
 1
 
 
 ×
 
 A
 
 2
 
 
 ×
 …
 ×
 
 A
 
 n
 
 
 =
 
 A
 
 1
 
 
 ×
 (
 
 A
 
 2
 
 
 ×
 …
 ×
 
 A
 
 n
 
 
 )
 
 
 {\displaystyle A_{1}\times A_{2}\times \ldots \times A_{n}=A_{1}\times (A_{2}\times \ldots \times A_{n})}

The definitions are the same in ZFC but without any worries about stratification (the grouping given here is opposite to that more usually used, but this is easily corrected for).
Now consider the infinite cartesian product 
 
 
 
 
 Π
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle \Pi _{i\in I}A_{i}}
 
. In ZFC, this is defined as the set of all functions f with domain I such that 
 
 
 
 f
 (
 i
 )
 ∈
 
 A
 
 i
 
 
 
 
 {\displaystyle f(i)\in A_{i}}
 
 (where A is implicitly understood as a function taking each i to 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
).
In NFU, this is requires attention to type. Given a set I and set valued function A whose value at 
 
 
 
 {
 i
 }
 
 
 {\displaystyle \{i\}}
 
 in 
 
 
 
 
 P
 
 1
 
 
 (
 I
 )
 
 
 {\displaystyle P_{1}(I)}
 
 is written 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
, Define 
 
 
 
 
 Π
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle \Pi _{i\in I}A_{i}}
 
 as the set of all functions f with domain I such that 
 
 
 
 f
 (
 i
 )
 ∈
 
 A
 
 i
 
 
 
 
 {\displaystyle f(i)\in A_{i}}
 
: notice that 
 
 
 
 f
 (
 i
 )
 ∈
 
 A
 
 i
 
 
 =
 A
 (
 {
 i
 }
 )
 
 
 {\displaystyle f(i)\in A_{i}=A(\{i\})}
 
 is stratified because of our convention that A is a function with values at singletons of the indices. Note that the very largest families of sets (which cannot be indexed by sets of singletons) will not have cartesian products under this definition. Note further that the sets 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
 are at the same type as the index set I (since one type higher than its elements); the product, as a set of functions with domain I (so at the same type as I) is one type higher (assuming a type-level ordered pair).
Now consider the product 
 
 
 
 
 Π
 
 i
 ∈
 I
 
 
 
 |
 
 
 A
 
 i
 
 
 
 |
 
 
 
 {\displaystyle \Pi _{i\in I}|A_{i}|}
 
 of the cardinals of these sets. The cardinality |
 
 
 
 
 Π
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle \Pi _{i\in I}A_{i}}
 
| is one type higher than the cardinals 
 
 
 
 
 |
 
 
 A
 
 i
 
 
 
 |
 
 
 
 {\displaystyle |A_{i}|}
 
, so the correct definition of the infinite product of cardinals is 
 
 
 
 
 T
 
 −
 1
 
 
 (
 
 |
 
 
 Π
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 |
 
 )
 
 
 {\displaystyle T^{-1}(|\Pi _{i\in I}A_{i}|)}
 
 (because the inverse of T is not total, it is possible that this may not exist).
Repeat this for disjoint unions of families of sets and sums of families of cardinals. Again, let A be a set-valued function with domain 
 
 
 
 
 P
 
 1
 
 
 (
 I
 )
 
 
 {\displaystyle P_{1}(I)}
 
: write 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
 for 
 
 
 
 A
 (
 {
 i
 }
 )
 
 
 {\displaystyle A(\{i\})}
 
. The disjoint union 
 
 
 
 
 Σ
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle \Sigma _{i\in I}A_{i}}
 
 is the set 
 
 
 
 {
 (
 i
 ,
 a
 )
 ∣
 a
 ∈
 
 A
 
 i
 
 
 }
 
 
 {\displaystyle \{(i,a)\mid a\in A_{i}\}}
 
. This set is at the same type as the sets 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
.
The correct definition of the sum 
 
 
 
 
 Σ
 
 i
 ∈
 I
 
 
 
 |
 
 
 A
 
 i
 
 
 
 |
 
 
 
 {\displaystyle \Sigma _{i\in I}|A_{i}|}
 
 is thus 
 
 
 
 
 |
 
 
 Σ
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 |
 
 
 
 {\displaystyle |\Sigma _{i\in I}A_{i}|}
 
, since there is no type displacement.
It is possible to extend these definitions to handle index sets which are not sets of singletons, but this introduces an additional type level and is not needed for most purposes.
In ZFC, define the disjoint union 
 
 
 
 
 Σ
 
 i
 ∈
 I
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle \Sigma _{i\in I}A_{i}}
 
 as 
 
 
 
 {
 (
 i
 ,
 a
 )
 ∣
 a
 ∈
 
 A
 
 i
 
 
 }
 
 
 {\displaystyle \{(i,a)\mid a\in A_{i}\}}
 
, where 
 
 
 
 
 A
 
 i
 
 
 
 
 {\displaystyle A_{i}}
 
 abbreviates 
 
 
 
 A
 (
 i
 )
 
 
 {\displaystyle A(i)}
 
.
Permutation methods can be used to show relative consistency with NFU of the assertion that for every strongly cantorian set A there is a set I of the same size whose elements are self-singletons: 
 
 
 
 i
 =
 {
 i
 }
 
 
 {\displaystyle i=\{i\}}
 
 for each i in I.

<h2 id="the-cumulative-hierarchy">The cumulative hierarchy</h2>
In <a href="/facts/ZFC/UYIsPbXw">ZFC</a>, define the cumulative hierarchy as the ordinal-indexed sequence of sets satisfying the following conditions: 
 
 
 
 
 V
 
 0
 
 
 =
 ∅
 
 
 {\displaystyle V_{0}=\emptyset }
 
; 
 
 
 
 
 V
 
 α
 +
 1
 
 
 =
 P
 (
 
 V
 
 α
 
 
 )
 
 
 {\displaystyle V_{\alpha +1}=P(V_{\alpha })}
 
; 
 
 
 
 
 V
 
 λ
 
 
 =
 ⋃
 {
 
 V
 
 β
 
 
 ∣
 β
 <
 λ
 }
 
 
 {\displaystyle V_{\lambda }=\bigcup \{V_{\beta }\mid \beta <\lambda \}}
 
 for limit ordinals 
 
 
 
 λ
 
 
 {\displaystyle \lambda }
 
. This is an example of a construction by <a href="/facts/Transfinite_recursion/XlolgTDl">transfinite recursion</a>. The rank of a set A is said to be 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 if and only if 
 
 
 
 A
 ∈
 
 V
 
 α
 +
 1
 
 
 −
 
 V
 
 α
 
 
 
 
 {\displaystyle A\in V_{\alpha +1}-V_{\alpha }}
 
. The existence of the ranks as sets depends on the axiom of replacement at each limit step (the hierarchy cannot be constructed in <a href="/facts/Zermelo_set_theory/o3fzd9nl">Zermelo set theory</a>); by the axiom of foundation, every set belongs to some rank.
The cardinal 
 
 
 
 
 |
 
 P
 (
 
 V
 
 ω
 +
 α
 
 
 )
 
 |
 
 
 
 {\displaystyle |P(V_{\omega +\alpha })|}
 
 is called 
 
 
 
 
 ℶ
 
 α
 
 
 
 
 {\displaystyle \beth _{\alpha }}
 
.
This construction cannot be carried out in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> because the power set operation is not a set function in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> (
 
 
 
 P
 (
 A
 )
 
 
 {\displaystyle P(A)}
 
 is one type higher than A for purposes of stratification).
The sequence of cardinals 
 
 
 
 
 ℶ
 
 α
 
 
 
 
 {\displaystyle \beth _{\alpha }}
 
 can be implemented in NFU. Recall that 
 
 
 
 
 2
 
 
 |
 
 A
 
 |
 
 
 
 
 
 {\displaystyle 2^{|A|}}
 
 is defined as 
 
 
 
 
 T
 
 −
 1
 
 
 (
 
 |
 
 {
 0
 ,
 1
 
 }
 
 A
 
 
 
 |
 
 )
 
 
 {\displaystyle T^{-1}(|\{0,1\}^{A}|)}
 
, where 
 
 
 
 {
 0
 ,
 1
 }
 
 
 {\displaystyle \{0,1\}}
 
 is a convenient set of size 2, and 
 
 
 
 
 |
 
 {
 0
 ,
 1
 
 }
 
 A
 
 
 
 |
 
 =
 
 |
 
 P
 (
 A
 )
 
 |
 
 
 
 {\displaystyle |\{0,1\}^{A}|=|P(A)|}
 
. Let 
 
 
 
 ℶ
 
 
 {\displaystyle \beth }
 
 be the smallest set of cardinals which contains 
 
 
 
 
 |
 
 N
 
 |
 
 
 
 {\displaystyle |N|}
 
 (the cardinality of the set of natural numbers), contains the cardinal 
 
 
 
 
 2
 
 
 |
 
 A
 
 |
 
 
 
 
 
 {\displaystyle 2^{|A|}}
 
 whenever it contains 
 
 
 
 
 |
 
 A
 
 |
 
 
 
 {\displaystyle |A|}
 
, and which is closed under suprema of sets of cardinals.
A convention for ordinal indexing of any well-ordering 
 
 
 
 
 W
 
 α
 
 
 
 
 {\displaystyle W_{\alpha }}
 
 is defined as the element x of the field of 
 
 
 
 W
 
 
 {\displaystyle W}
 
 such that
the order type of the restriction of 
 
 
 
 W
 
 
 {\displaystyle W}
 
 to 
 
 
 
 {
 y
 ∣
 y
 W
 x
 }
 
 
 {\displaystyle \{y\mid yWx\}}
 
 is 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
; then define 
 
 
 
 
 ℶ
 
 α
 
 
 
 
 {\displaystyle \beth _{\alpha }}
 
 as the element with index 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 in the natural order on the elements of 
 
 
 
 ℶ
 
 
 {\displaystyle \beth }
 
. The cardinal 
 
 
 
 
 ℵ
 
 α
 
 
 
 
 {\displaystyle \aleph _{\alpha }}
 
 is the element with index 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 in the natural order on all infinite cardinals (which is a well-ordering, see above). Note that 
 
 
 
 
 ℵ
 
 0
 
 
 =
 
 |
 
 N
 
 |
 
 
 
 {\displaystyle \aleph _{0}=|N|}
 
 follows immediately from this definition. In all these constructions, notice that the type of the index 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 is two higher (with type-level ordered pair) than the type of 
 
 
 
 
 W
 
 α
 
 
 
 
 {\displaystyle W_{\alpha }}
 
.
Each set A of ZFC has a transitive closure 
 
 
 
 T
 C
 (
 A
 )
 
 
 {\displaystyle TC(A)}
 
 (the intersection of all transitive sets which contains A). By the axiom of foundation, the restriction of the membership relation to the transitive closure of A is a <a href="/facts/Well-founded_relation/zyRRyJ4M">well-founded relation</a>. The relation 
 
 
 
 ∈
 ⌈
 T
 C
 (
 A
 )
 
 
 {\displaystyle \in \lceil TC(A)}
 
 is either empty or has A as its top element, so this relation is a set picture. It can be proved in ZFC that every set picture is isomorphic to some 
 
 
 
 ∈
 ⌈
 T
 C
 (
 A
 )
 
 
 {\displaystyle \in \lceil TC(A)}
 
.
This suggests that (an initial segment of) the cumulative hierarchy can be studied by considering the isomorphism classes of set pictures. These isomorphism classes are sets and make up a set in <a href="/facts/New_Foundations/jT6vAvj5">NFU</a>. There is a natural set relation analogous to membership on isomorphism classes of set pictures: if 
 
 
 
 x
 
 
 {\displaystyle x}
 
 is a set picture, write 
 
 
 
 [
 x
 ]
 
 
 {\displaystyle [x]}
 
 for its isomorphism class and define 
 
 
 
 [
 x
 ]
 E
 [
 y
 ]
 
 
 {\displaystyle [x]E[y]}
 
 as holding if 
 
 
 
 [
 x
 ]
 
 
 {\displaystyle [x]}
 
 is the isomorphism class of the restriction of y to the downward closure of one of the elements of the preimage under y of the top element of y. The relation E is a set relation, and it is straightforward to prove that it is well-founded and extensional. If the definition of E is confusing, it can be deduced from the observation that it is induced by precisely the relationship which holds between the set picture associated with A and the set picture associated with B when 
 
 
 
 A
 ∈
 B
 
 
 {\displaystyle A\in B}
 
 in the usual set theory.
There is a T operation on isomorphism classes of set pictures analogous to the T operation on ordinals: if x is a set picture, so is 
 
 
 
 
 x
 
 ι
 
 
 =
 {
 (
 {
 a
 }
 ,
 {
 b
 }
 )
 ∣
 (
 a
 ,
 b
 )
 ∈
 x
 }
 
 
 {\displaystyle x^{\iota }=\{(\{a\},\{b\})\mid (a,b)\in x\}}
 
. Define 
 
 
 
 T
 (
 [
 x
 ]
 )
 
 
 {\displaystyle T([x])}
 
 as 
 
 
 
 [
 
 x
 
 ι
 
 
 ]
 
 
 {\displaystyle [x^{\iota }]}
 
. It is easy to see that 
 
 
 
 [
 x
 ]
 E
 [
 y
 ]
 ↔
 T
 (
 [
 x
 ]
 )
 =
 T
 (
 [
 y
 ]
 )
 
 
 {\displaystyle [x]E[y]\leftrightarrow T([x])=T([y])}
 
.
An axiom of extensionality for this simulated set theory follows from E's extensionality. From its well-foundedness follows an axiom of foundation. There remains the question of what comprehension axiom E may have. Consider any collection of set pictures 
 
 
 
 {
 
 x
 
 ι
 
 
 ∣
 x
 ∈
 S
 }
 
 
 {\displaystyle \{x^{\iota }\mid x\in S\}}
 
 (collection of set pictures whose fields are made up entirely of singletons). Since each 
 
 
 
 
 x
 
 ι
 
 
 
 
 {\displaystyle x^{\iota }}
 
 is one type higher than x (using a type-level ordered pair), replacing each element 
 
 
 
 {
 a
 }
 
 
 {\displaystyle \{a\}}
 
 of the field of each 
 
 
 
 
 x
 
 ι
 
 
 
 
 {\displaystyle x^{\iota }}
 
 in the collection with 
 
 
 
 (
 x
 ,
 {
 a
 }
 )
 
 
 {\displaystyle (x,\{a\})}
 
 results in a collection of set pictures isomorphic to the original collection but with their fields disjoint. The union of these set
pictures with a new top element yields a set picture whose isomorphism type will have as its preimages under E exactly the elements of the original collection. That is, for any collection of isomorphism types 
 
 
 
 [
 
 x
 
 ι
 
 
 ]
 =
 T
 (
 [
 x
 ]
 )
 
 
 {\displaystyle [x^{\iota }]=T([x])}
 
, there is an isomorphism type 
 
 
 
 [
 y
 ]
 
 
 {\displaystyle [y]}
 
 whose preimage under E is exactly this collection.
In particular, there will be an isomorphism type [v] whose preimage under E is the collection of all T[x]'s (including T[v]). Since T[v] E v and E is well-founded, 
 
 
 
 T
 [
 v
 ]
 ≠
 v
 
 
 {\displaystyle T[v]\neq v}
 
. This resembles the resolution of the Burali–Forti paradox discussed above and in the <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> article, and is in fact the local resolution of Mirimanoff's paradox of the set of all well-founded sets.
There are ranks of isomorphism classes of set pictures just as there are ranks of sets in the usual set theory. For any collection of set pictures A, define S(A) as the set of all isomorphism classes of set pictures whose preimage under E is a subset of A; call A a "complete" set if every subset of A is a preimage under E. The collection of "ranks" is the smallest collection containing the empty set and closed under the S operation (which is a kind of power set construction) and under unions of its subcollections. It is straightforward to prove (much as in the usual set theory) that the ranks are well-ordered by inclusion, and so the ranks have an index in this well-order: refer to the rank with index 
 
 
 
 α
 
 
 {\displaystyle \alpha }
 
 as 
 
 
 
 
 R
 
 α
 
 
 
 
 {\displaystyle R_{\alpha }}
 
. It is provable that 
 
 
 
 
 |
 
 
 R
 
 α
 
 
 
 |
 
 =
 
 ℶ
 
 α
 
 
 
 
 {\displaystyle |R_{\alpha }|=\beth _{\alpha }}
 
 for complete ranks 
 
 
 
 
 R
 
 α
 
 
 
 
 {\displaystyle R_{\alpha }}
 
. The union of the complete ranks (which will be the first incomplete rank) with the relation E looks like an initial segment of the universe of Zermelo-style set theory (not necessarily like the full universe of <a href="/facts/ZFC/UYIsPbXw">ZFC</a> because it may not be large enough). It is provable that if 
 
 
 
 
 R
 
 α
 
 
 
 
 {\displaystyle R_{\alpha }}
 
 is the first incomplete rank, then 
 
 
 
 
 R
 
 T
 (
 α
 )
 
 
 
 
 {\displaystyle R_{T(\alpha )}}
 
 is a complete rank and thus 
 
 
 
 T
 (
 α
 )
 <
 α
 
 
 {\displaystyle T(\alpha )<\alpha }
 
. So there is a "rank of the cumulative hierarchy" with an "external automorphism" T moving the rank downward, exactly the condition on a nonstandard model of a rank in the cumulative hierarchy under which a model of NFU is constructed in the <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> article. There are technical details to verify, but there is an interpretation not only of a fragment of <a href="/facts/ZFC/UYIsPbXw">ZFC</a> but of <a href="/facts/New_Foundations/jT6vAvj5">NFU</a> itself in this structure, with 
 
 
 
 [
 x
 ]
 
 ∈
 
 N
 F
 U
 
 
 [
 y
 ]
 
 
 {\displaystyle [x]\in _{NFU}[y]}
 
 defined as 
 
 
 
 T
 (
 [
 x
 ]
 )
 E
 [
 y
 ]
 ∧
 [
 y
 ]
 ∈
 
 R
 
 T
 (
 α
 )
 +
 1
 
 
 
 
 {\displaystyle T([x])E[y]\wedge [y]\in R_{T(\alpha )+1}}
 
: this "relation" 
 
 
 
 
 E
 
 N
 F
 U
 
 
 
 
 {\displaystyle E_{NFU}}
 
 is not a set relation but has the same type displacement between its arguments as the usual membership relation 
 
 
 
 ∈
 
 
 {\displaystyle \in }
 
.
So there is a natural construction inside NFU of the cumulative hierarchy of sets which internalizes the natural construction of a model of NFU in Zermelo-style set theory.
Under the Axiom of Cantorian Sets described in the <a href="/facts/New_Foundations/jT6vAvj5">New Foundations</a> article, the strongly cantorian part of the set of isomorphism classes of set pictures with the E relation as membership becomes a (proper class) model of ZFC (in which there are n-Mahlo cardinals for each n; this extension of NFU is strictly stronger than ZFC). This is a proper class model because the strongly cantorian isomorphism classes do not make up a set.
Permutation methods can be used to create from any model of NFU a model in which every strongly cantorian isomorphism type of set pictures is actually realized as the restriction of the true membership relation to the transitive closure of a set.

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Axiomatic_set_theory/1ptfsvUP">Axiomatic set theory</a></li></ul>

<ul><li><a href="/facts/Keith_Devlin/9YsdjXjk">Keith Devlin</a>, 1994. The Joy of Sets, 2nd ed. Springer-Verlag.</li>
<li>Holmes, Randall, 1998. <a href="https://randall-holmes.github.io/head.pdf">Elementary Set Theory with a Universal Set</a>. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this introduction to NFU via the web. Copyright is reserved.</li>
<li>Potter, Michael, 2004. Set Theory and its Philosophy, 2nd ed. Oxford Univ. Press.</li>
<li>Suppes, Patrick, 1972. Axiomatic Set Theory. Dover.</li>
<li>Tourlakis, George, 2003. Lectures in Logic and Set Theory, Vol. 2. Cambridge Univ. Press.</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="http://us.metamath.org/">Metamath:</a> A web site devoted to an ongoing derivation of mathematics from the axioms of ZFC and <a href="/facts/First-order_logic/lcISqWIg">first-order logic</a>.</li>
<li><a href="/facts/Stanford_Encyclopedia_of_Philosophy/LDuL5HW4">Stanford Encyclopedia of Philosophy</a>:
<ul><li><a href="http://plato.stanford.edu/entries/quine-nf">Quine's New Foundations</a>—by Thomas Forster.</li>
<li><a href="http://setis.library.usyd.edu.au/stanford/entries/settheory-alternative/">Alternative axiomatic set theories</a>—by Randall Holmes.</li></ul></li>
<li>Randall Holmes: <a href="https://randall-holmes.github.io/nf.html">New Foundations Home Page</a></li></ul>

Implementation of mathematics in set theory open-in-new

Implementation of mathematics in set theory