New Foundations

New Foundations (NF) is a set theory in mathematical logic that is finitely axiomatizable and non-well-founded. It was devised by Willard Van Orman Quine as a streamlined version of the theory of types found in Principia Mathematica. The well-formed formulas of NF are the standard ones from propositional calculus, using just two primitive predicates: equality (=) and membership (∈).

Definition

The system can be presented with only two axiom schemata. The first is Extensionality: if two objects have exactly the same elements, they are the same object. The second is a restricted axiom schema of comprehension: the set {x | φ} exists for every stratified formula φ. A formula φ is stratified if there is a function assigning natural numbers to its syntactic parts so that for any atomic subformula x ∈ y, the number for y is one greater than the number for x, and for any atomic subformula x = y, the numbers for x and y are equal.

Finite axiomatization

NF can also be given a finite axiomatization, which has the advantage of removing the concept of stratification. In this approach, the axioms correspond to natural basic constructions, whereas stratified comprehension is powerful but less intuitive. In his introductory book, Holmes took the finite axiomatization as fundamental and proved stratified comprehension as a theorem.

Extensionality: If A and B are sets, and for every object x, x is in A exactly when x is in B, then A = B. (This can also serve as a definition of equality, but then another axiom is needed to justify substitution with that definition.) Singleton: For every object x, the set ι(x) = {x} = {y | y = x} exists. Cartesian Product: For any sets A and B, the set A × B = {(a, b) | a ∈ A and b ∈ B} exists. This can be restricted to just A × V or V × B. Converse: For each relation R, the set R⁻¹ = {(x, y) | (y, x) ∈ R} exists. Singleton Image: For any relation R, the set Rι = {({x}, {y}) | (x, y) ∈ R} exists. Domain: If R is a relation, the set dom(R) = {x | ...} exists.