This article examines the implementation of mathematical concepts in set theory. The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) 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). What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like, and it is the approaches to implementation of mathematical concepts under these two general views that are being compared and contrasted. 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.
Preliminaries The following sections carry out certain constructions in the two theories ZFC and NFU and compare the resulting implementations of certain mathematical structures (such as the natural numbers). 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 formula of our language: 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 Bertrand Russell's theory of descriptions.) 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 set-builder notation: { 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 free 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 class theories like NBG 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 ordinal ω {\displaystyle \omega } in ZFC is not suitable for NFU because the object (defined in purely set theoretical language as the set of all finite von Neumann ordinals) 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 well-orderings 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 Peano arithmetic 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 ZFC 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 Zermelo set theory instead of ZFC for much of what is done in this article, for example).
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). Even though NFU also allows the construction of set ur-elements yet to become members of a set, the empty set 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 union 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 Axiom of Pairing, the existence of the empty set follows by Separation from the existence of any set, and the binary union of two sets exists by the axioms of Pairing and Union ( x ∪ y = ⋃ { x , y } {\displaystyle x\cup y=\bigcup \{x,y\}} ).
Ordered pair
First, consider the ordered pair. The reason that this comes first is technical: ordered pairs are needed to implement relations and functions, 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 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 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 Kuratowski. 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 projections) 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.
Relations Relations are sets whose members are all ordered pairs. Where possible, a relation R {\displaystyle R} (understood as a binary predicate) 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 proper classes). 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} ).
Related definitions Let R {\displaystyle R} and S {\displaystyle S} be given binary relations. Then the following concepts are useful: The converse 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 union of the domain and range of R {\displaystyle R} . The preimage 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 relative product 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 Cartesian product 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 ( P ( A ∪ B ) ) {\displaystyle {\mathcal {P}}\!\left({\mathcal {P}}\!\left(A\cup B\right)\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).
Properties and kinds of relations A binary relation R {\displaystyle R} is:
Reflexive if x R x {\displaystyle xRx} for every x {\displaystyle x} in the field of R {\displaystyle R} . Symmetric if ∀ x , y ( x R y → y R x ) {\displaystyle \forall x,y\,(xRy\to yRx)} . Transitive if ∀ x , y , z ( x R y ∧ y R z → x R z ) {\displaystyle \forall x,y,z\,(xRy\wedge yRz\rightarrow xRz)} . Antisymmetric if ∀ x , y ( x R y ∧ y R x → x = y ) {\displaystyle \forall x,y\,(xRy\wedge yRx\rightarrow x=y)} . Well-founded 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} . 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} . Relations having certain combinations of the above properties have standard names. A binary relation R {\displaystyle R} is:
An equivalence relation if R {\displaystyle R} is reflexive, symmetric, and transitive. A partial order if R {\displaystyle R} is reflexive, antisymmetric, and transitive. A linear order 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} . A well-ordering if R {\displaystyle R} is a linear order and well-founded. 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.
Functions A functional relation is a binary predicate 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 relation (predicate) 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 Axiom of Replacement assures that F [ A ] {\displaystyle F\left[A\right]} is a set in ZFC. 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 stratified. Moreover, S {\displaystyle S} can be proved not to exist in NFU (see the resolution of Cantor's paradox in New Foundations.)
Operations on functions Let f {\displaystyle f} and g {\displaystyle g} be arbitrary functions. The composition 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 inverse of f {\displaystyle f} , f ( − 1 ) {\displaystyle f^{\left(-1\right)}} , is defined as the converse of f {\displaystyle f} if this is a function. Given any set A {