BIGpedia - New Foundations - Encyclopedia and Dictionary Online

In mathematical logic, the New Foundations (NF) of W. V. O. Quine is a candidate set theory, obtained from a streamlined version of the theory of types of Bertrand Russell. It is so called because it was proposed in an article entitled New Foundations for mathematical logic, which appeared in 1937 (reference to be supplied).

The version of the theory of types has a linear hierarchy of types: type 0 consists of "individuals" otherwise undescribed, while for each (meta-) natural number n+1 type n+1 objects are understood to be sets of type n objects. The primitive predicates of this theory are equality and membership. Typing rules for well-formed atomic sentences are succinctly summed up in the formulas $x n = y n$ and $x^{n} \in y^{n+1}$ (notation to be improved). The original type theory of the Principia Mathematica of Bertrand Russell and Alfred North Whitehead implemented a much more complex type system including types of relations with possibly heterogeneous argument types. In 1914, von Neumann discovered that the ordered pair can be coded as a set, and so it is possible to eliminate relation types in favor of a linear hierarchy of types of sets as described here. The usual definition of the ordered pair as a set is not that of von Neumann but a later one due to Kuratowski. In NF, one frequently uses another definition of ordered pair due to Quine.

The axioms of the theory are extensionality (sets of the same (positive) type with the same members are equal) and a comprehension scheme : " $\{x^n \mid \phi(x^n)\}^{n+1}$ exists" for any well-formed formula $φ(x n)$ : i.e., for any such formula $φ(x n)$ there is a set $A n + 1$ such that for all $x^n, x^n \in A^{n+1} \leftrightarrow \phi(x^n)$ .

New Foundations (NF) is obtained from this theory by abandoning the distinctions of type. The axioms of this theory are extensionality (two objects with the same elements are the same object) and all those instances of comprehension obtained by dropping type indices (without introducing new identifications between variables) from an instance of comprehension of the streamlined type theory. It might seem that the resulting comprehension scheme would be the inconsistent scheme of naive set theory, but this is not the case: for example, the impossible Russell class $\{x \mid x \not\in x\}$ is not constructed because there is no way to assign types consistently to all occurrences of x to obtain an instance of comprehension of the type theory.

It is traditional to describe the comprehension scheme of NF in a way which makes no direct reference to types: a formula $φ$ is said to be "stratified" if there is a function f from variables (considered as pieces of syntax) to natural numbers such that for any atomic subformula " $x \in y$ " of $φ$ we have f("y") = f("x") + 1, while for any atomic subformula " $x = y$ " of $φ$ , we have f("x") = f("y"). The comprehension scheme for NF is comprehension " $\{x \mid \phi\}$ exists" for each stratified formula $φ$ . Even the indirect reference to types in the notion of stratification can be eliminated: NF comprehension is equivalent to a finite conjunction of its instances, so NF can be finitely axiomatized without any reference to types at all.

It is notable that NF (and the theory NFU + Infinity + Choice described below, which is known to be consistent) allow the construction of "big" sets. For example, " $x = x$ " is a stratified formula, so the universal set V = " $\{x \mid x=x\}$ " exists by stratified comprehension. In NF (as in the streamlined theory of types) the natural way to define natural numbers is Frege's: define each natural number n as the set of all sets with n elements (this can be done without the circularity of this summary). In general, a cardinal number is an equivalence class of sets under the relation $A \sim B$ defined as "there is a bijection between A and B" and an ordinal number is an equivalence class of well-orderings under similarity. These definitions cannot be used in Zermelo set theory or its extensions because these classes are "too large".

The outstanding problem with this theory is the problem as to whether it is consistent. It is known that NF disproves Choice, and so proves Infinity (Specker, 1953). But it is also known (Jensen, 1969) that the minor(?) modification of allowing urelements (objects in each positive type which have no elements but which are distinct from the empty set and from one another) produces a theory NFU which is known to be consistent (weaker than arithmetic) and consistent with Infinity and Choice as well. Some other variations are known to be consistent.

Positive set theory

Categories: Set theory

New Foundations

Related