Quine's New Foundations (NF)

https://www.wikiwand.com/en/New_Foundations https://plato.stanford.edu/entries/quine-nf/

Quine's system of axiomatic set theory, NF, takes its name from the title "New Foundations for Mathematical Logic", which was a 1937 article which introduced it. The axioms of NF are extensionality together with stratified comprehension.

New Foundations (NF) is an axiomatic set theory, proposed in a 1937's article, "New Foundations for Mathematical Logic" by Willard Van Orman Quine, as a simplification of the theory of types of Principia Mathematica.

In 1940 and in a revision of 1951 Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included proper classes as well as sets.

NF has a universal set, so it's a non-well founded set theory i.e. it's an axiomatic set theory that allows infinite descending chains of membership such as $\dots x_n \in x_{n-1} \in \dots x_3\in x_2 \in x_1$.

It avoids Russell's paradox by permitting only stratifiable formulae to be defined using the axiom (schema) of comprehension. For instance $x \in y$ is a stratifiable formula, but $x \in x$ is not.

Much of this entry discusses NFU, an important variant of NF due to Jensen (1969) and exposited in Holmes (1998).