New Foundations

New Foundations is an axiomatic set theory introduced by W. V. Quine. Its stratified comprehension scheme permits a set to contain exactly the objects satisfying a formula when that formula admits a consistent assignment of types.

Stratified formula: A formula is stratified when variables can be assigned integer types so equality and membership respect fixed type differences. New Foundations permits comprehension only for formulas that pass this type-consistency test.
W. V. Quine: An American philosopher and logician whose work shaped twentieth-century logic and analytic philosophy. Quine introduced New Foundations in 1937 as a revised approach to set theory.
Zermelo–Fraenkel set theory: An axiomatic set theory whose axioms build sets in stages and restrict comprehension through separation. Unlike New Foundations, it does not admit a universal set.
Consistency of New Foundations: The question of whether New Foundations can derive a contradiction from its axioms. A proof of consistency relative to standard set theories is not known.
Comprehension axiom: A set-theoretic principle asserting the existence of sets whose members satisfy specified conditions. New Foundations restricts comprehension to predicates expressible by stratified formulas.
Mathematical Logic: The study of formal systems, proof, and mathematical reasoning using logical methods. New Foundations emerged from Quine's work in formal logic.
Russell's ramified type theory: A hierarchy of types and orders designed to avoid paradoxes by restricting expressions and impredicative definitions. New Foundations replaces this explicit hierarchy with stratification within an untyped language.
Specker's theorem: A result showing that New Foundations proves the existence of an infinite set while its set of natural numbers is finite in a particular sense. It reveals unusual consequences of the system's treatment of cardinality.
Russell's paradox: A contradiction arising from the purported set of all sets that are not members of themselves. Unrestricted comprehension yields this contradiction; stratification blocks the defining formula.
Principia Mathematica: A foundational work by Alfred North Whitehead and Bertrand Russell that develops mathematics using logic and ramified type theory. Quine's system drew on the type-theoretic setting he encountered through this work.

Linked from 6 pages