Implementation of mathematics in set theory

The aim of this article is to examine the implementation of mathematical concepts in set theory. The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice). For details of these two systems, consult their main articles.

It is not the primary aim of this article to say anything about the relative merits of these theories as foundations for mathematics. The reason for the use of two different set theories is to illustrate that multiple approaches to the implementation of mathematics are feasible. Precisely because of this approach, this article is not a source of "official" definitions for any mathematical concept.

Empty set, singleton, unordered pairs and tuples

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!)

${\displaystyle \emptyset \equiv _{def}\{x\mid x\neq x\}}$ 

The empty set is the unique set with no members. In NFU, there are also urelements with no members.

${\displaystyle \{x\}\equiv _{def}\{y\mid y=x\}}$ 

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

${\displaystyle \{x,y\}\equiv _{def}\{z\mid z=x\vee z=y\}}$ 

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

${\displaystyle x\cup y\equiv _{def}\{z\mid z\in x\vee z\in y\}}$ 

The union of two sets is defined in the usual way.

${\displaystyle \{x_{1},\ldots ,x_{n},x_{n+1}\}\equiv _{def}\{x_{1},\ldots ,x_{n}\}\cup \{x_{n+1}\}}$ 

This is a recursive definition of unordered n-tuples for any n (finite sets given as lists of their elements).

In NFU, all the set definitions given work by stratified comprehension; in ZFC, the existence of the unordered pair is given by the axiom of Pairing, the existence of the empty set follows by Separation from the existence of any set, and the boolean union of two sets exists by the axioms of Pairing and Union (${\displaystyle x\cup y=\bigcup \{x,y\}}$ ).

Ordered pair

The first substantial mathematical construction we consider is the ordered pair. The reason that this comes first is technical: we will need it to implement notions of relation and function which are needed for implementations of other concepts which may seem to be prior.

The first definition of the ordered pair was the definition ${\displaystyle (x,y)\equiv _{def}\{\{\{x\},\emptyset \},\{\{y\}\}\}}$  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 ${\displaystyle n>1}$  from the system of that work.

It is more usual now to use the definition ${\displaystyle (x,y)\equiv _{def}\{\{x\},\{x,y\}\}}$ , due to Kuratowski.

Either of these definitions works in either ZFC or 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 ${\displaystyle (x,y)}$  which is the same type as its projections) in NFU. For the moment, we will use the Kuratowski pair in both systems, until we can give a formal justification for the introduction of the type-level pair.

The internal details of these definitions have nothing to do with their actual mathematical function. For any notion ${\displaystyle (x,y)}$  of ordered pair, the things that matter are that it satisfy the defining condition

• ${\displaystyle (x,y)=(z,w)\equiv x=z\wedge y=w}$ 

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

Relations

A relation is implemented as a set of ordered pairs, in either ZFC or NFU. In ZFC, some relations (such as the general equality relation or subset relation on sets) are too large to be sets, and so cannot be implemented as sets (but may harmlessly be reified as proper classes). In NFU, some relations (such as the membership relation) are not sets because their definitions are not stratified: in ${\displaystyle \{(x,y)\mid x\in y\}}$  x and y would need to have the same type (because they appear as projections of the same pair, but also with successive types (because x is considered as an element of y).

Where possible, a relation R (understood as a binary predicate) is implemented as ${\displaystyle \{(x,y)\mid xRy\}}$  (which may be written as ${\displaystyle \{z\mid \pi _{1}(z)R\pi _{2}(z)\}}$ ). Where R is a set of ordered pairs, we read ${\displaystyle xRy}$  as ${\displaystyle (x,y)\in R}$ . In ZFC, any relation which has ___domain a subset of a set A and range a subset of a set B will be a set, since the cartesian product ${\displaystyle A\times B=\{(a,b)\mid a\in A\wedge b\in B\}}$  is a set (being a subclass of ${\displaystyle P(P(A\cup B))}$ ) and Separation provides for the existence of ${\displaystyle \{(x,y)\in A\times B\mid xRy\}}$ . In NFU, some relations with global scope (such as equality and subset) are implemented as sets. In NFU, we need to bear in mind that x and y are three types lower than R in ${\displaystyle xRy}$  (this will drop to one type when a type-level ordered pair is used).

Notice that here we do not support the distinction between range and codomain of a relation: this could be done by representing a relation R with codomain B as (R,B), but we do not find this necessary in our development. Note also that for the moment we do not consider relations of arity greater than 2: all our relations are binary.

Operations on relations

All relations are here understood to be sets.

The converse of a relation R is the relation ${\displaystyle \{(y,x)\mid xRy\}}$ .

The ___domain of a relation R is the set ${\displaystyle \{x\mid (\exists y.xRy)\}}$ .

The range of a relation R is the ___domain of the converse of R.

The field of a relation R is the union of the ___domain and range of R.

The preimage of an element x of the field of R is the set ${\displaystyle \{y\mid yRx\}}$  (used in the definition of "well-founded" below).

The relative product ${\displaystyle R|S}$  is the relation ${\displaystyle \{(x,z)\mid (\exists y.xRy\wedge ySz)\}}$ .

In ZFC, all of these are sets by application of Union, Separation, and Power Set. In NFU, it is easy to see that these are stratified definitions.

Special kinds of relation

Some properties of relations:

• A relation R is reflexive if ${\displaystyle xRx}$  holds for all x in the ___domain of R.

• A relation R is symmetric if ${\displaystyle xRy\leftrightarrow yRx}$  for all x and y.

• A relation R is transitive if ${\displaystyle xRy\wedge yRz\rightarrow xRz}$  for all x,y,z.

• A relation R is antisymmetric if ${\displaystyle xRy\wedge yRx\rightarrow x=y}$  for all x,y.

• A relation R is well-founded if for every set S which meets the field of R, there is x in S whose preimage under R does not meet S.

• A relation R is extensional if for every x,y in the field of R, x=y iff x and y have the same preimage under R.

Some kinds of relations:

• A relation R is an equivalence relation iff it is reflexive, symmetric, and transitive.

• A relation R is a partial order iff it is reflexive, antisymmetric, and transitive.

• A relation R is a linear order iff it is a partial order and for every x,y in the field of R, either ${\displaystyle xRy}$  or ${\displaystyle yRx}$ .

• A relation R is a well-ordering iff it is a linear order and it is well-founded.

• A relation R is a set picture iff it is well-founded and extensional.

Functions

A functional relation (where relation means binary predicate) is a binary predicate F such that ${\displaystyle (\forall xyz.xFy\wedge xFz\rightarrow y=z)}$ . Such a relation (predicate) is implemented as a relation (set) exactly as in the previous section. So the predicate F is implemented by the set ${\displaystyle \{(x,y)\mid xFy\}}$ . We say that a set of ordered pairs F is a function just in case ${\displaystyle (\forall xyz.(x,y)\in F\wedge (x,z)\in F\rightarrow y=z)}$ .

We define F(x) as the unique object y such that ${\displaystyle xFy}$  (if there is one) or as the unique object y such that ${\displaystyle (x,y)\in F}$ . The presence in both theories of functional predicates which are not sets makes it useful to allow the notation F(x) both for sets 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. In NFU, notice that in ${\displaystyle F(x)}$ , x has the same type as the expression ${\displaystyle F(x)}$ , and F is three types higher than ${\displaystyle F(x)}$  (one type higher if a type-level pair is used). For any set A, we define ${\displaystyle F[A]}$  as ${\displaystyle \{y\mid (\exists x.x\in A\wedge y=F(x))\}}$ , more conveniently written as ${\displaystyle \{F(x)\mid x\in A\}}$ . If A is a set and F is any functional relation, ${\displaystyle F[A]}$  is a set in ZFC by Replacement. In NFU, notice that in ${\displaystyle F[A]}$ , A has the same type as the expression ${\displaystyle F[A]}$ , and F is two types higher than ${\displaystyle F[A]}$  (the same type if a type-level pair is used).

The function I defined by I(x) = x does not exist as a set in ZFC because it is "too large" to be a set. It is a set in NFU. The function ${\displaystyle S(x)=\{x\}}$  is not a function in either theory (in ZFC because it is too large; in NFU because its definition is unstratified and further it can be proved that there is no such function: see the resolution of Cantor's paradox in the New Foundations article).

Operations on functions

The composition ${\displaystyle g\circ f}$  of functions f and g is defined as the relative product ${\displaystyle f|g}$ , if this is a function: we have ${\displaystyle g\circ f}$  a function with ${\displaystyle (g\circ f)(x)=g(f(x))}$  if the range of f is a subset of the ___domain of g. The inverse ${\displaystyle f^{-1}}$  is the converse of f (if this is a function). The identity function ${\displaystyle i_{A}}$  is the set ${\displaystyle \{(x,x)\mid x\in A\}}$  for any set A: this is a set in both theories for different reasons.

Special kinds of function

A function is an injection and is said to be one-to-one if its converse is also a function.

If A and B are sets,

• an injection from A to B is an injection whose ___domain is A and whose range is a subset of B.

• a surjection from A to B is a function whose ___domain is A and whose range is B.

• a bijection from A to B is an injection whose ___domain is A and whose range is B.

Notice that our terminology here adjusts for the fact that functions as we have defined them do not determine their codomains.

Size of sets

In both ZFC and NFU, we say that two sets A and B are the same size (or are equinumerous) if and only if there is a bijection f from A to B. We can write this ${\displaystyle |A|=|B|}$  as long as we note that for the moment this expresses a relation between A and B rather than a relation between objects ${\displaystyle |A|}$  and ${\displaystyle |B|}$  which have not yet been defined. We also provide notation ${\displaystyle A\sim B}$  for this relation to be used in contexts such as the actual definition of the cardinals where even the appearance of presupposing abstract cardinals should be avoided.

Similarly, we can define ${\displaystyle |A|\leq |B|}$  as holding iff there is an injection from A to B.

It is straightforward to show that the relation of equinumerousness is an equivalence relation: equinumerousness of A with A is witnessed by ${\displaystyle i_{A}}$ ; if f witnesses ${\displaystyle |A|=|B|}$  then ${\displaystyle f^{-1}}$  witnesses ${\displaystyle |B|=|A|}$ ; if f witnesses ${\displaystyle |A|=|B|}$  and g witnesses ${\displaystyle |B|=|C|}$ , then ${\displaystyle g\circ f}$  witnesses ${\displaystyle |A|=|C|}$ .

We can show that ${\displaystyle |A|\leq |B|}$  is a linear order -- on abstract cardinals, but not on sets. Reflexivity is obvious and transitivity is proven just as for equinumerousness. The Schroder-Bernstein theorem, provable in either ZFC or NFU in an entirely standard way, establishes that

• ${\displaystyle |A|\leq |B|\wedge |B|\leq |A|\rightarrow |A|=|B|}$ 

(this establishes that we have antisymmetry on cardinals (not yet defined), but we are now considering a relation on sets), and

• ${\displaystyle |A|\leq |B|\vee |B|\leq |A|}$ 

follows in a standard way in either theory from the Axiom of Choice.

Finite sets and natural numbers

Natural numbers can be considered either as finite ordinals or finite cardinals. Here we consider them as finite cardinal numbers. This is the first place where a major difference between the implementations in ZFC and NFU becomes evident.

The Axiom of Infinity of ZFC tells us that there is a set A which contains ${\displaystyle \emptyset }$  and contains ${\displaystyle y\cup \{y\}}$  for each ${\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

• ${\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)\}}$ 

which is the intersection of all sets which contain the empty set and are closed under the "successor" operation ${\displaystyle y\mapsto y\cup \{y\}}$ .

In ZFC, we say that a set ${\displaystyle A}$  is finite iff there is ${\displaystyle n\in N}$  such that ${\displaystyle |n|=|A|}$ : further, we define ${\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 ${\displaystyle ((\emptyset ,\emptyset ),\emptyset )}$  and contains ${\displaystyle ((x,y\cup \{y\}),z\cup \{z\})}$  whenever it contains ${\displaystyle ((x,y),z)}$ .

In NFU, it is not obvious that this approach can be used, since the successor operation ${\displaystyle y\cup \{y\}}$  is unstratified and so the set N as defined above cannot be shown to exist in NFU (it is interesting to note that 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 the New Foundations article).

The standard definition of the natural numbers, which is actually the oldest set-theoretic definition of natural numbers, is as equivalence classes of finite sets under equinumerousness. We here present the definition of N appropriate to NFU in exactly this way (this is not the usual way to do it, but the results are the same): define Fin, the set of finite sets, as

• ${\displaystyle \{A\mid (\forall F.(\emptyset \in F\wedge (\forall xy.x\in F\rightarrow x\cup \{y\}\in F))\rightarrow A\in F)\}}$ 

For any set ${\displaystyle A\in Fin}$ , define ${\displaystyle |A|}$  as ${\displaystyle \{B\mid A\sim B\}}$ . Define N as the set ${\displaystyle \{|A|\mid A\in Fin\}}$ .

The Axiom of Infinity of NFU can be expressed as ${\displaystyle V\not \in Fin}$ : this is enough to establish that each natural number has a nonempty successor (the successor of ${\displaystyle |A|}$  being ${\displaystyle |A\cup \{x\}|}$  for any ${\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, we can define |A|+|B| as ${\displaystyle |A\cup B|}$ . More formally, define m+n for m and n in N as

• ${\displaystyle \{A\mid (\exists BC.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 NFU 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, we choose a representative of each finite cardinality to represent that 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.

Equivalence relations and partitions

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 we can regard the set ${\displaystyle [x]_{R}=\{y\in A\mid xRy\}}$  as representing an abstraction from the set x respecting just those features (we identify elements of A up to R).

For any set A, we say that a set ${\displaystyle P}$  is a partition of A if all elements of P are nonempty, any two distinct elements of P are disjoint, and ${\displaystyle A=\bigcup P}$ .

For every equivalence relation R with field A, ${\displaystyle \{[x]_{R}\mid x\in A\}}$  is a partition of A. Moreover, each partition P of A determines an equivalence relation ${\displaystyle \{(x,y)\mid (\exists A\in P.x\in A\wedge y\in A)\}}$ .

This technique has limitations in both ZFC and NFU. In ZFC, since the universe is not a set, it is seems possible to abstract features only from elements of small domains. This can be circumvented using a trick due to Dana Scott: if R is an equivalence relation on the universe, define ${\displaystyle [x]_{R}}$  as the set of all y such that ${\displaystyle yRx}$  and the rank of y is less than or equal to the rank of any ${\displaystyle zRx}$ . This works because the ranks are sets. Of course, there still may be a proper class of ${\displaystyle [x]_{R}}$ 's. In NFU, the main difficulty is that ${\displaystyle [x]_{R}}$  is one type higher than x, so for example the "map" ${\displaystyle x\mapsto [x]_{R}}$  is not in general a (set) function (though ${\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 ${\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.

Ordinal numbers

We say that two well-orderings ${\displaystyle W_{1}}$  and ${\displaystyle W_{2}}$  are similar and write ${\displaystyle W_{1}\sim W_{2}}$  just in case there is a bijection f from the field of ${\displaystyle W_{1}}$  to the field of ${\displaystyle W_{2}}$  such that ${\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 NFU we define the order type of a well-ordering W as the set of all well-orderings which are similar to W. We define the set of ordinal numbers as the set of all order types of well-orderings.

In ZFC we cannot do this, because the equivalence classes are too large. It would be formally possible to use Scott's trick to define the ordinals in essentially this way nonetheless, but instead we use a device of von Neumann.

For any partial order ${\displaystyle \leq }$ , the corresponding strict partial order ${\displaystyle <}$  is defined as ${\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 ${\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 that fact that membership is a strict well-ordering of the von Neumann ordinals.

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 }$  iff some (and so any) ${\displaystyle W_{1}\in \alpha }$  is similar to an initial segment of some (and so any) ${\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 our 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 ${\displaystyle T^{4}(\alpha )}$  for any ordinal ${\displaystyle \alpha }$ , where ${\displaystyle T(\alpha )}$  is the order type of ${\displaystyle W^{\iota }=\{(\{x\},\{y\})\mid xWy\}}$  for any ${\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 ${\displaystyle T^{4}(\Omega )}$ , and ${\displaystyle T^{4}(\Omega )<\Omega }$ . All uses of ${\displaystyle T^{4}}$  here can be replaced with ${\displaystyle T^{2}}$  if a type-level pair is used.

This shows that the T operation is nontrivial, which has a number of interesting consequences. It follows immediately that the singleton map ${\displaystyle x\mapsto \{x\}}$  is not a set, as otherwise restrictions of this map would establish the similarity of W and ${\displaystyle W^{\iota }}$  for any well-ordering W. T is (externally) bijective and order-preserving. Because of this, the fact ${\displaystyle T^{4}(\Omega )<\Omega }$  establishes that ${\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. The motivation for these definitions will be clearer in the next section. It is important to note that there can be no set of cantorian ordinals or set of strongly cantorian ordinals.

It is possible to reason about von Neumann ordinals in NFU. 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 ${\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 ${\displaystyle T(\alpha )}$  (it is one type higher, thus the application of T): but the well-orderings of a von Neumann ordinal A by membership and inclusion are clearly the same because the two relations are actually the same relation, so the order type of A is fixed under T. Moreover, the same argument applies to any smaller ordinal Iwhich 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".

Cardinal numbers

Cardinal numbers are defined in NFU in a way which generalizes the definition of natural number: for any set A, ${\displaystyle |A|\equiv _{def}\{B\mid B\sim A\}}$ .

In ZFC, these equivalence classes are too large as usual. Scott's trick could be used (and indeed is used in ZF without Choice), but we usually define ${\displaystyle |A|}$  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 ZFC, one proves ${\displaystyle |A|<|P(A)|}$ . In NFU, 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 NFU is ${\displaystyle |P_{1}(A)|<|P(A)|}$ , where ${\displaystyle P_{1}(A)}$  is the set of one-element subsets of A. ${\displaystyle |P_{1}(V)|<|P(V)|}$  shows that there are "fewer" singletons than sets (the obvious bijection ${\displaystyle x\mapsto \{x\}}$  from ${\displaystyle P_{1}(V)}$  to V has already been seen not to be a set). It is actually provable in NFU + Choice that ${\displaystyle |P_{1}(V)|<|P(V)|<<|V|}$  (where << signals the existence of many intervening cardinals). We define a type-raising T operation on cardinals analogous to the T operation on ordinals: ${\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 ${\displaystyle |A|=|P_{1}(A)|=T(|A|)}$ ; the cardinal ${\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 (${\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. ${\displaystyle |A|+|B|=\{C\cup D\mid C\sim A\wedge D\sim B\wedge C\cap D=\emptyset \}}$ . One would like to define ${\displaystyle |A|\cdot |B|}$  as ${\displaystyle |A\times B|}$ , and one does this in ZFC, but there is an obstruction in NFU when using the Kuratowski pair: one defines ${\displaystyle |A|\cdot |B|}$  as ${\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 we define ${\displaystyle B^{A}}$  as the collection of functions from A to B, we note that this is three types higher than A or B, so it is reasonable to define ${\displaystyle |B|^{|A|}}$  as ${\displaystyle T^{-3}(|B^{A}|)}$  so that it is the same type as A or B (${\displaystyle T^{-1}}$  replaces ${\displaystyle T^{-3}}$  if we use a type-level pair). An effect of this is that the exponential operation is partial: for example, ${\displaystyle 2^{|V|}}$  is undefined.

The exponential operation is total and behaves exactly as we expect 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 NFU 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 ${\displaystyle |V|\cdot |V|=|V|}$  we can derive the existence of a type level ordered pair: ${\displaystyle |V|\cdot |V|=T^{-2}(|V\times V|)}$  is equal to ${\displaystyle |V|}$  just in case ${\displaystyle |V\times V|=T^{2}(|V|)=|P_{1}^{2}(V)|}$ , which would be witnessed by a one-to-one correspondence between Kuratowski pairs ${\displaystyle (a,b)}$  and double singletons ${\displaystyle \{\{c\}\}}$ : redefine ${\displaystyle (a,b)}$  as the c such that ${\displaystyle \{\{c\}\}}$  is associated with the Kuratowski ${\displaystyle (a,b)}$ : this is a type-level notion of ordered pair.

The Axiom of Counting and subversion of stratification

We now have two different implementations of the natural numbers in NFU (though they are the same in ZFC: finite ordinals and finite cardinals. Each of these supports the T operation in NFU. It is easy to prove that ${\displaystyle T(n)}$  is a natural number in NFU + Infinity + Choice (and so ${\displaystyle |N|}$  and the first infinite ordinal ${\displaystyle \omega }$  are cantorian) but it is not possible to prove in this theory that ${\displaystyle T(n)=n}$ . However, common sense indicates that this should be true, and we adopt this as an axiom:

• Rosser's Axiom of Counting: For each natural number n, ${\displaystyle T(n)=n}$ .

One natural consequence of this axiom (and indeed its original formulation) is

• ${\displaystyle |\{1,\ldots ,n\}|=n}$  for each natural number n.

All that can be proved in NFU without Counting is ${\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).

Strongly cantorian sets have important properties which we review. The type of any variable restricted to a strongly cantorian set A can be raised or lowered as desired by replacing references to ${\displaystyle a\in A}$  with references to ${\displaystyle \bigcup f(a)}$  (type of a raised) or ${\displaystyle f^{-1}(\{a\}}$  (type of a lowered) where ${\displaystyle f(a)=\{a\}}$  for all ${\displaystyle a\in A}$ . 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.