New Foundations


In mathematical logic, New Foundations is a non-well-founded, finitely axiomatizable set theory conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica.

Definition

The well-formed formulas of NF are the standard formulas of propositional calculus with two primitive predicates equality and membership. NF can be presented with only two axiom schemata:
  • Extensionality: Two objects with the same elements are the same object; formally, given any set A and any set B, if for every set X, X is a member of A if and only if X is a member of B, then A is equal to B.
  • A restricted axiom schema of comprehension: exists for each stratified formula.
A formula is said to be stratified if there exists a function f from pieces of 's syntax to the natural numbers, such that for any atomic subformula of we have f = f + 1, while for any atomic subformula of, we have f = f.

Finite axiomatization

NF can be finitely axiomatized. One advantage of such a finite axiomatization is that it eliminates the notion of stratification. The axioms in a finite axiomatization correspond to natural basic constructions, whereas stratified comprehension is powerful but not necessarily intuitive. In his introductory book, Holmes opted to take the finite axiomatization as basic, and prove stratified comprehension as a theorem. The precise set of axioms can vary, but includes most of the following, with the others provable as theorems:
  • Extensionality: If and are sets, and for each object, is an element of if and only if is an element of, then.
  • * This statement can also be viewed as the definition of the equality symbol instead of an axiom. However, in that case another axiom is needed to justify substitution with the equality symbol defined this way.
  • Singleton: For every object, the set exists, and is called the singleton of.
  • Cartesian Product: For any sets,, the set, called the Cartesian product of and, exists. This can be restricted to the existence of one of the cross products or.
  • Converse: For each relation, the set exists; observe that exactly if.
  • Singleton Image: For any relation, the set, called the singleton image of, exists.
  • Domain: If is a relation, the set, called the domain of, exists. This can be defined using the operation of type lowering.
  • Inclusion: The set exists. Equivalently, we may consider the set.
  • Complement: For each set, the set, called the complement of, exists.
  • Union: If and are sets, the set, called the union of and, exists.
  • Universal Set: exists. It is straightforward that for any set,.
  • Ordered Pair: For each,, the ordered pair of and,, exists; exactly if and. This and larger tuples can be a definition rather than an axiom if an ordered pair construction is used.
  • Projections: The sets and exist.
  • Diagonal: The set exists, called the equality relation.
  • Set Union: If is a set all of whose elements are sets, the set, called the union of, exists.
  • Relative Product: If, are relations, the set, called the relative product of and, exists.
  • Anti-intersection: exists. This is equivalent to complement and union together, with and.
  • Cardinal one: The set of all singletons,, exists.
  • Tuple Insertions: For a relation, the sets and exist.
  • Type lowering: For any set, the set exists.

    Typed Set Theory

New Foundations is closely related to Russellian unramified typed set theory, a streamlined version of the theory of types of Principia Mathematica with a linear hierarchy of types. In this many-sorted theory, each variable and set is assigned a type. It is customary to write the type indices as superscripts: denotes a variable of type n. Type 0 consists of individuals otherwise undescribed. For each natural number n, type n+1 objects are sets of type n objects; objects connected by identity have equal types and sets of type n have members of type n-1. The axioms of TST are extensionality, on sets of the same type, and comprehension, namely that if is a formula, then the set exists. In other words, given any formula, the formula is an axiom where represents the set and is not free in. This type theory is much less complicated than the one first set out in the Principia Mathematica, which included types for relations whose arguments were not necessarily all of the same types.
There is a correspondence between New Foundations and TST in terms of adding or erasing type annotations. In NF's comprehension schema, a formula is stratified exactly when the formula can be assigned types according to the rules of TST. This can be extended to map every NF formula to a set of corresponding TST formulas with various type index annotations. The mapping is one-to-many because TST has many similar formulas. For example, raising every type index in a TST formula by 1 results in a new, valid TST formula.

Tangled Type Theory

Tangled Type Theory is an extension of TST where each variable is typed by an ordinal rather than a natural number. The well-formed atomic formulas are and where. The axioms of TTT are those of TST where each variable of type is mapped to a variable where is an increasing function.
TTT is considered a "weird" theory because each type is related to each lower type in the same way. For example, type 2 sets have both type 1 members and type 0 members, and extensionality axioms assert that a type 2 set is determined uniquely by either its type 1 members or its type 0 members. Whereas TST has natural models where each type is the power set of type, in TTT each type is being interpreted as the power set of each lower type simultaneously. Regardless, a model of NF can be easily converted to a model of TTT, because in NF all the types are already one and the same. Conversely, with a more complicated argument, it can also be shown that the consistency of TTT implies the consistency of NF.

NFU and other variants

NF with urelements is an important variant of NF due to Jensen and clarified by Holmes. Urelements are objects that are not sets and do not contain any elements, but can be contained in sets. One of the simplest forms of axiomatization of NFU regards urelements as multiple, unequal empty sets, thus weakening the extensionality axiom of NF to:
  • Weak extensionality: Two non-empty objects with the same elements are the same object; formally,
In this axiomatization, the comprehension schema is unchanged, although the set will not be unique if it is empty.
However, for ease of use, it is more convenient to have a unique, "canonical" empty set. This can be done by introducing a sethood predicate to distinguish sets from atoms. The axioms are then:
  • Sets: Only sets have members, i.e.
  • Extensionality: Two sets with the same elements are the same set, i.e.
  • Comprehension: The set exists for each stratified formula, i.e.
NF3 is the fragment of NF with full extensionality and those instances of comprehension which can be stratified using at most three types. NF4 is the same theory as NF.
Mathematical Logic is an extension of NF that includes proper classes as well as sets. ML was proposed by Quine and revised by Hao Wang, who proved that NF and the revised ML are equiconsistent.

Constructions

This section discusses some problematic constructions in NF. For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see implementation of mathematics in set theory.

Ordered pairs

and functions are defined in TST as sets of ordered pairs in the usual way. For purposes of stratification, it is desirable that a relation or function is merely one type higher than the type of the members of its field. This requires defining the ordered pair so that its type is the same as that of its arguments. The usual definition of the ordered pair, namely, results in a type two higher than the type of its arguments a and b. Hence for purposes of determining stratification, a function is three types higher than the members of its field. NF and related theories usually employ Quine's set-theoretic definition of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements a and b, and therefore does not directly work in NFU.
As an alternative approach, Holmes takes the ordered pair as a primitive notion, as well as its left and right projections and, i.e., functions such that and . Fortunately, whether the ordered pair is type-level by definition or by assumption usually does not matter.

Natural numbers and the axiom of infinity

The usual form of the axiom of infinity is based on the von Neumann construction of the natural numbers, which is not suitable for NF, since the description of the successor operation is necessarily unstratified. The usual form of natural numbers used in NF follows Frege's definition, i.e., the natural number n is represented by the set of all sets with n elements. Under this definition, 0 is easily defined as, and the successor operation can be defined in a stratified way: Under this definition, one can write down a statement analogous to the usual form of the axiom of infinity. However, that statement would be trivially true, since the universal set would be an inductive set.
Since inductive sets always exist, the set of natural numbers can be defined as the intersection of all inductive sets. This definition enables mathematical induction for stratified statements, because the set can be constructed, and when satisfies the conditions for mathematical induction, this set is an inductive set.
Finite sets can then be defined as sets that belong to a natural number. However, it is not trivial to prove that is not a "finite set", i.e., that the size of the universe is not a natural number. Suppose that. Then ,, and each subsequent natural number would be too, causing arithmetic to break down. To prevent this, one can introduce the axiom of infinity for NF:
It may intuitively seem that one should be able to prove Infinity in NF by constructing any "externally" infinite sequence of sets, such as. However, such a sequence could only be constructed through unstratified constructions, so such a proof could not be carried out in NF. In fact, Infinity is logically independent of NFU: There exists models of NFU where is a non-standard natural number. In such models, mathematical induction can prove statements about, making it impossible to "distinguish" from standard natural numbers.
However, there are some cases where Infinity can be proven :
  • In NF, Specker has shown that the axiom of choice is false. Since it can be proved through induction that every finite set has a choice function, it follows that is infinite.
  • In NFU with axioms asserting the existence of a type-level ordered pair, is equinumerous with its proper subset, which implies Infinity. Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair. NFU + Infinity interprets NFU + "there is a type-level ordered pair".
Stronger axioms of infinity exist, such as that the set of natural numbers is a strongly Cantorian set, or NFUM = NFU + Infinity + Large Ordinals + Small Ordinals which is equivalent to Morse–Kelley set theory plus a predicate on proper classes which is a κ-complete nonprincipal ultrafilter on the proper class ordinal κ.