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).
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.
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).
as its only elements: The union of two sets is defined in the usual way: This is a recursive definition of unordered
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.
Outside of formal set theory, we usually specify a function in terms of its domain and codomain, as in the phrase "Let
is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as
This can be circumvented using a trick due to Dana Scott: if R is an equivalence relation on the universe, define
This can be circumvented by the use of the Axiom of Choice to select a representative from each equivalence class to replace
In NFU, the use of equivalence class constructions to abstract properties of general sets is more common, as for example in the definitions of cardinal and ordinal number below.
It would be formally possible to use Scott's trick to define the ordinals in essentially the same way, but a device of von Neumann is more commonly used.
The existence of order types for all well-orderings is not a theorem of Zermelo set theory: it requires the Axiom of replacement.
Recall that a von Neumann ordinal is a transitive set A such that the restriction of membership to A is a strict well-ordering.
This is quite a strong condition in the NFU context, since the membership relation involves a difference of type.
The only von Neumann ordinals which can be shown to exist in NFU without additional assumptions are the concrete finite ones.
Cantor's theorem shows (in both theories) that there are nontrivial distinctions between infinite cardinal numbers.
The operations of cardinal arithmetic are defined in a set-theoretically motivated way in both theories.
It is straightforward to prove that the product always exists (but requires attention because the inverse of T is not total).
Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including
The type of any variable restricted to a strongly cantorian set A can be raised or lowered as desired by replacing references to
See the main New Foundations article for stronger axioms that can be adjoined to NFU to enforce "standard" behavior of familiar mathematical objects.
of magnitudes: formally speaking, a real number is an equivalence class of pairs
The operations of addition and multiplication on real numbers are defined just as one would expect from the algebraic rules for adding and multiplying differences.
The definitions are the same in ZFC but without any worries about stratification (the grouping given here is opposite to that more usually used, but this is easily corrected for).
In ZFC, define the cumulative hierarchy as the ordinal-indexed sequence of sets satisfying the following conditions:
This suggests that (an initial segment of) the cumulative hierarchy can be studied by considering the isomorphism classes of set pictures.
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
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.