New Foundations (NF, NFU)

Origin. W. V. Quine, "New foundations for mathematical logic" (American Mathematical Monthly, 1937), motivated by Russell's type theory: Quine's idea was to keep the type restriction on formulas and drop it from the ontology, so that there is one sort of object and the stratification is a syntactic condition. Specker (1953) proved NF refutes choice; Jensen (1969) showed the urelement variant NFU is consistent; Rosser's Logic for Mathematicians (1953) developed mathematics in it.

Models. ZFC bans the universal set by the cumulative hierarchy — sets are built in stages, and no stage contains everything. NF bans it differently, or rather does not: {x : x = x} is a set, because "x = x" is stratified. What is banned is Russell's {x : x ∉ x}, because "x ∉ x" cannot be stratified. The paradox is blocked by a condition on the formula rather than by a condition on the universe.

Formalism.

Stratification: A formula φ is stratified iff integers can be assigned to its variables such that for every atomic subformula x ∈ y: type(y) = type(x) + 1 for every atomic subformula x = y: type(y) = type(x) "x = x" stratifies (any assignment). "x ∉ x" does not: it needs type(x) = type(x) + 1.

Axioms: Extensionality: ∀z (z ∈ x ↔ z ∈ y) → x = y Stratified comprehension: ∃A ∀x (x ∈ A ↔ φ(x)), for φ stratified, A not free in φ. That is the whole theory.

What exists: V = {x : x = x}, the universal set. V ∈ V. The complement of any set. The set of all singletons. Not: {x : x ∉ x}.

Specker's theorem (1953): NF ⊢ ¬AC. Hence NF ⊢ Infinity (since AC holds for finite sets). A theory that refutes choice and proves infinity — neither by assumption.

Cantor's theorem, restricted: |℘(V)| ≤ |V| since ℘(V) ⊆ V, contradicting Cantor? No: Cantor's diagonal argument is not stratified for V. NF proves Cantor's theorem only for cantorian sets — those with |A| = |{x} : x ∈ A}|. V is not cantorian.

Finite axiomatizability (Hailperin 1944): Stratified comprehension reduces to finitely many instances. NF is finitely axiomatized, unlike ZFC.

NFU (Jensen 1969): Weaken extensionality to allow urelements. NFU is consistent relative to a weak fragment of Z; NFU + Infinity + Choice is consistent relative to Z. NFU proves AC rather than refuting it. Holmes has developed mathematics in NFU extensively.

Consistency of NF: Open from 1937. Holmes announced a proof (2010), revised repeatedly; a Lean formalization was completed in 2024, which is the current state of the claim.

Symbols.

Metatheory. NF is the only serious alternative to the cumulative hierarchy that has survived, and everything interesting about it is a consequence of stratification being a condition on syntax: Specker's refutation of choice, the failure of Cantor's theorem for V, and the finite axiomatizability all come from the same place. That NFU is consistent and NF's consistency was open for over eighty years is the standing oddity — the urelements make no difference to the intuition and all the difference to the proof, and the reason is that extensionality plus stratification interact in a way nobody had a model-building technique for. Holmes's proof, now machine-checked, is the answer if it stands.

Applies to. The foundations debate, as the live alternative to the iterative conception. Type theory's history, since NF is Russell's types with the ontology collapsed. Category theory's size problems, where a universal set would help and NF's does not, because the category-theoretic constructions are unstratified. Comparative axiomatics, where NF is the standing test of whether the cumulative hierarchy is necessary or merely sufficient.

Limitations. Mathematics in NF is awkward: the standard constructions of ordinals and cardinals are unstratified, and Rosser's development needs care at every step that ZFC does not. Refuting choice is a serious cost, since most of analysis assumes it. The consistency question dominated the subject for eighty years and starved it of workers, so the theory around NF is thin compared to ZFC's — there is no NF forcing, no NF inner model theory, and the large-cardinal scale has no NF counterpart.

© 2026 Lingenic LLC