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.

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\}}$ .