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