New Foundations

In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine 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 exposited in Holmes (1998). In 1940 and 1951 Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included 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 a logical theory that allows infinite descending chains of membership such as … x_n ∈ x_n-1 ∈ …x₃ ∈ x₂ ∈ x₁. It avoids Russell's paradox by only allowing stratifiable formulae in the axiom of comprehension. For instance x ∈ y is a stratifiable formula, but x ∈ x is not (for details of how this works see below).

The primitive predicates of Russellian unramified typed set theory (TST), a streamlined version of the theory of types, are equality (${\displaystyle =}$) and membership (${\displaystyle \in }$). TST has a linear hierarchy of types: type 0 consists of individuals otherwise undescribed. For each (meta-) natural number 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: ${\displaystyle x^{n}=y^{n}\!}$ and ${\displaystyle x^{n}\in y^{n+1}}$. (Quinean set theory seeks to eliminate the need for such superscripts.)

...
Wikipedia