In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, New Foundations (NF) is an
axiomatic set theory, conceived by
Willard Van Orman Quine
Willard Van Orman Quine (; known to his friends as "Van"; June 25, 1908 – December 25, 2000) was an American philosopher and logician in the analytic tradition, recognized as "one of the most influential philosophers of the twentieth century" ...
as a simplification of the
theory of types of ''
Principia Mathematica''. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name. Much of this entry discusses NFU, an important variant of NF due to Jensen (1969) and clarified by Holmes (1998). In 1940 and in a revision in 1951, Quine introduced
an extension of NF sometimes called "Mathematical Logic" or "ML", that included
proper classes as well as
sets.
New Foundations has a
universal set, so it is a
non-well-founded set theory. That is to say, it is an axiomatic set theory that allows infinite descending chains of membership, such as
… x
n ∈ x
n-1 ∈ … ∈ x
2 ∈ x
1. It avoids
Russell's paradox by permitting only
stratifiable formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
s to be defined using the
axiom schema of comprehension. For instance, x ∈ y is a stratifiable formula, but x ∈ x is not.
The Type Theory TST
The primitive predicates of Russellian unramified typed set theory (TST), a streamlined version of the theory of types, are
equality (
) and
membership (
). TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-)
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called '' cardinal ...
''n'', type ''n''+1 objects are sets of type ''n'' objects; sets of type ''n'' have members of type ''n''-1. Objects connected by identity must have the same type. The following two atomic formulas succinctly describe the typing rules:
and
. (Quinean set theory seeks to eliminate the need for such superscripts to denote types.)
The axioms of TST are:
*
Extensionality: sets of the same (positive) type with the same members are equal;
* An axiom schema of comprehension, namely:
::If
is a formula, then the set
exists.
:In other words, given any formula
, the formula