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. 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.

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 matters 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.

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.

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.