Implementation of mathematics in set theory
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 formula_1 exists", where formula_1 is a formula of our language: the theory proves the existence of "the x such that formula_1" just in case it is a theorem that "there is one and only one x such that formula_1". (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 formula_1" can be contemplated in the two theories. A specific form of definition in the language of set theory is set-builder notation: formula_6 means "the set A such that for all x, formula_7" (A cannot be free in formula_1). This notation admits certain conventional extensions: formula_9 is synonymous with formula_10; formula_11 is defined as formula_12, where formula_13 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 formula_14 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 formula_15 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 formula_15 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: For each object  formula_18, there is a set formula_19 with formula_18 as its only element: For objects formula_18 and formula_23, there is a set formula_24 containing formula_18 and formula_23 as its only elements: The union of two sets is defined in the usual way: This is a recursive definition of unordered formula_29-tuples for any concrete formula_29 (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 binary union of two sets exists by the axioms of Pairing and Union (formula_32). 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 formula_33 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 formula_34, 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 formula_35 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 formula_35 of ordered pair, the thing that matters is that it satisfies the defining condition …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 formula_38 (understood as a binary predicate) is implemented as formula_39 (which may be written as formula_40). When formula_38 is a relation, the notation formula_42 means formula_43. 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 formula_44 formula_18 and formula_23 would need to have the same type (because they appear as projections of the same pair), but also successive types (because formula_18 is considered as an element of formula_23). Related definitions. Let formula_38 and formula_50 be given binary relations. Then the following concepts are useful: The converse of formula_38 is the relation formula_52. The domain of formula_38 is  the set formula_54. The range of formula_38 is the domain of the converse of formula_38. That is, the set formula_57. The field of formula_38 is the union of the domain and range of formula_38. The preimage of a member formula_18 of the field of formula_38 is the set formula_62 (used in the definition of 'well-founded' below.) The downward closure of a member formula_18 of the field of formula_38 is the smallest set formula_65 containing formula_18, and containing each formula_67 for each formula_68 (i.e., including the preimage of each of its elements with respect to formula_38 as a subset.) The  relative product formula_70 of formula_38 and formula_50 is the relation formula_73. 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 formula_38 with codomain formula_75 as formula_76, but our development will not require this. In ZFC, any relation whose domain is a subset of a set formula_77 and whose range is a subset of a set formula_75 will be a set, since the Cartesian product formula_79 is a set (being a subclass of formula_80), and "Separation" provides for the existence of formula_81 . In NFU, some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that formula_18 and formula_23 are three types lower than formula_38 in formula_42 (one type lower if a type-level ordered pair is used). Properties and kinds of relations. A binary relation formula_38 is: Relations having certain combinations of the above properties have standard names. A binary relation formula_38 is: Functions. A functional relation is a binary predicate formula_115 such that formula_116 Such a relation (predicate) is implemented as a relation (set) exactly as described in the previous section . So the predicate formula_115 is implemented by the set formula_118. A relation formula_115 is a function if and only if formula_120 It is therefore possible to define the value function formula_121 as the unique object formula_23 such that formula_123 – i.e.: formula_18 is formula_115-related to formula_23 such that the relation formula_127 holds between formula_18 and formula_23 – or as the unique object formula_23 such that formula_131. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation formula_121 both for sets formula_115 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 formula_134 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 formula_77 to formula_75 if its domain equals formula_77 and its range "is contained in" formula_75. In this way, every function is a function from its  domain to its range, and a function formula_127 from formula_77 to formula_75 is also a function from formula_77 to formula_143 for any set formula_143 containing formula_75. 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 formula_146, where formula_127 is a functional relation and formula_75 is its codomain, but  we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as formula_149- then one could define a function as the ordered triple formula_150 so as to also include the domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let formula_151 be a binary relation", but formally formula_38 is a set of ordered pairs such that formula_153 and formula_154. In NFU, formula_18 has the same type as formula_121, and formula_115 is three types higher than formula_121 (one type higher, if a type-level ordered  pair is used). To solve this problem, one could define formula_159 as formula_160 for any set formula_77, but this is more conveniently written as formula_162. Then, if formula_77 is a set and formula_115 is any functional relation, the Axiom of Replacement assures that formula_159 is a set in ZFC. In NFU, formula_159 and formula_77 now have the same type, and formula_115 is two types higher than formula_159 (the same type, if a type-level ordered pair is used). The function formula_170 is not a set in ZFC because it is "too large". formula_171 is however a set in NFU. The  function (predicate) formula_172 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, formula_173 can be proved not to exist in NFU (see the resolution of Cantor's paradox in New Foundations.) Operations on functions. Let formula_127 and formula_175 be arbitrary functions. The composition of formula_127 and formula_175, formula_178, is defined as the relative product formula_179, but only if this results in a function such that formula_178 is also a function, with formula_181 , if the range of formula_127 is a subset of the domain of formula_175. The inverse of formula_127, formula_185, is defined as the converse of formula_127 if this is a function. Given any set formula_77, the identity function formula_188 is the set formula_189, and this is a set in both ZFC and NFU for different reasons. Special kinds of function. A function is an injective (also called one-to-one) if it has an inverse function. A function formula_127 from formula_77 to formula_75 is a: Defining functions as ordered pairs formula_146 or ordered triples formula_150 has the advantages that we do  not have to introduce the terminology of being a function "from formula_77 to formula_75", and that we can speak of "being surjective" outright as opposed to only being able to speak of "being surjective onto formula_75". Size of sets. In both ZFC and NFU, 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". This can be written as formula_210, but note that (for the moment) this expresses a relation between "A" and "B" rather than a relation between yet-undefined objects formula_211 and formula_212 . Denote this relation by formula_213 in contexts such as the actual definition of the cardinals where even the appearance of presupposing abstract cardinals should be avoided. Similarly, define formula_214 as holding if and only if 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 formula_188; if "f" witnesses formula_210, then formula_217 witnesses formula_218; and if "f" witnesses formula_210 and "g" witnesses formula_220, then formula_221 witnesses formula_222. It can be shown that formula_214 is a linear order on abstract cardinals , but not on sets. Reflexivity is obvious and transitivity is proven just as for equinumerousness. The Schröder–Bernstein theorem, provable in ZFC and NFU in an entirely standard way, establishes that (this establishes antisymmetry on cardinals), and 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 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 formula_226 and contains formula_227 for each formula_228. This set "A" is not uniquely determined (it can be made larger while preserving this closure property): the set "N" of natural numbers is which is the intersection of all sets which contain the empty set and are closed under the "successor" operation formula_230. In ZFC, a set formula_77 is finite if and only if there is formula_232 such that formula_233: further, define formula_211 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 formula_235 for each natural number formula_18 and contains formula_237 whenever it contains formula_238. In NFU, it is not obvious that this approach can be used, since the successor operation formula_227 is unstratified and so the set "N" as defined above cannot be shown to exist in NFU (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 below or 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. Essentially the same definition is appropriate to NFU (this is not the usual definition, but the results are the same): define "Fin", the set of finite sets, as For any set formula_241, define formula_211 as formula_243. Define "N" as the set  formula_244 whenever it contains formula_211, and which is closed under suprema of sets of cardinals. A convention for ordinal indexing of any well-ordering formula_246 is defined as the element "x" of the field of formula_247 such that the order type of the restriction of formula_247 to formula_249 is formula_250; then define formula_251 as the element with index formula_250 in the natural order on the elements of formula_253. The cardinal formula_254 is the element with index formula_250 in the natural order on all infinite cardinals (which is a well-ordering, see above). Note that formula_256 follows immediately from this definition . In all these constructions, notice that the type of the index formula_250 is two higher (with type-level ordered pair) than the type of formula_258. Each set "A" of ZFC has a transitive closure formula_259 (the intersection of all transitive sets which contains "A"). By the axiom of foundation, the restriction of the membership relation to the transitive closure of "A" is a well-founded relation. The relation formula_260 is either empty or has "A" as its top element, so this relation is a "set picture". It can be proved in ZFC that every set picture is isomorphic to some  formula_260. This suggests that (an initial segment of) the cumulative hierarchy can be studied by considering the isomorphism classes of set pictures. These isomorphism classes are sets and make up a set in NFU. There is a natural set relation analogous to membership on isomorphism classes of set pictures: if formula_18 is a set picture, write formula_263 for its isomorphism class and define formula_264 as holding if formula_263 is the isomorphism class of the restriction of "y" to the downward closure of one of the elements of the preimage under "y" of the top element of "y". The relation E  is a set relation, and it is straightforward to prove that it is well-founded and extensional. If the definition of E is confusing, it can be deduced from the observation that it is induced by precisely the relationship which holds between the set picture associated with "A" and the set picture associated with "B" when formula_266 in the usual set theory. There is a T operation on isomorphism classes of set pictures analogous to the T operation on ordinals: if "x" is a set picture, so is formula_267. Define formula_268 as formula_269. It is easy to see that formula_270 . An axiom of extensionality for this simulated set theory follows from E's extensionality. From its well-foundedness follows an axiom of foundation. There remains the question of what comprehension axiom E may have. Consider any collection of set pictures formula_271 (collection of set pictures whose fields are made up entirely of singletons). Since each formula_272 is one type higher than x (using a type-level ordered pair), replacing each element formula_273 of the field of each formula_272 in the collection with formula_275 results in a collection of set pictures isomorphic to the original collection but with their fields disjoint . The union of these set pictures with a new top element yields a set picture whose isomorphism type will have as its preimages under E exactly the elements of the original collection. That is, for any collection of isomorphism types formula_276, there is an isomorphism type formula_277 whose preimage under E is exactly this collection. In particular, there will be an isomorphism type "[v]" whose preimage under E is the collection of "all" "T"["x"]'s (including "T"["v"]). Since "T"["v"] "E" "v" and E is well-founded, formula_278. This resembles the resolution of the Burali–Forti paradox discussed above and in  the New Foundations article, and is in fact the local resolution of Mirimanoff's paradox of the set of all well-founded sets. There are ranks of isomorphism classes of set pictures just as there are ranks of sets in the usual set theory. For any collection of set pictures "A", define "S"("A") as the set of all isomorphism classes of set pictures whose preimage under E is a subset of A; call A a "complete" set if every subset of "A" is a preimage under E. The collection of "ranks" is the smallest collection containing the empty set and  closed under the S operation (which is a kind of power set construction) and under unions of its subcollections. It is straightforward to prove (much as in the usual set theory) that the ranks are well-ordered by inclusion, and so the ranks have an index in this well-order: refer to the rank with index formula_250 as formula_280. It is provable that formula_281 for complete ranks formula_280. The union of the complete ranks (which will be the first incomplete rank) with the relation E looks like an initial segment of the universe of Zermelo-style set theory (not necessarily  like the full universe of ZFC because it may not be large enough). It is provable that if formula_280 is the first incomplete rank, then formula_284 is a complete rank and thus formula_285. So there is a "rank of the cumulative hierarchy" with an "external automorphism" T moving the rank downward, exactly the condition on a nonstandard model of a rank in the cumulative hierarchy under which a model of NFU is constructed in the New Foundations article. There are technical details to verify, but there is an interpretation not only of a fragment of ZFC but of NFU itself  in this structure, with formula_286 defined as formula_287: this "relation" formula_288 is not a set relation but has the same type displacement between its arguments as the usual membership relation formula_289. So there is a natural construction inside NFU of the cumulative hierarchy of sets which internalizes the natural construction of a model of NFU in Zermelo-style set theory. Under the Axiom of Cantorian Sets described in the New Foundations article, the strongly cantorian part of the set of isomorphism classes of set pictures with the E relation as membership becomes a (proper class) model of ZFC (in which  there are "n"-Mahlo cardinals for each "n"; this extension of NFU is strictly stronger than ZFC). This is a proper class model because the strongly cantorian isomorphism classes do not make up a set. Permutation methods can be used to create from any model of NFU a model in which every strongly cantorian isomorphism type of set pictures is actually realized as the restriction of the true membership relation to the transitive closure of a set.