5. Untyped Universes (Forster & Holmes)
Modern Synthesis and Untyped Realities
The modern era of New Foundations (NF) research, led by Thomas Forster and M. Randall Holmes, shifts the foundational focus from defensive consistency debates toward exploiting the unique computational and topological properties of an untyped universe.
In the logicist tradition, mathematical sets represent predicates-in-extension. Conscious cognition and conceptual frameworks operate as unified totalities; imposing external type hierarchies (such as Russell’s type ladder or ZFC’s cumulative hierarchy) fragments this unitary perspective.
Set theories with a universal set treat \(V\) as a legitimate, first-class mathematical object, establishing a complete Boolean algebra under set inclusion.
- Forster, T. (1995). Set Theory with a Universal Set. Sections 1.2.1 (Sets as predicates-in-extension), 2.1 (NF), and 2.3.2 (NFU).
- Holmes, M. R. (1998). Elementary Set Theory with a Universal Set. Ch. 15.2 (Burali-Forti meets T), Ch. 17.5 (Cantorian Sets), Ch. 19.1 (Subversion Theorem), Ch. 23 (Stratified Lambda-Calculus).
Cantorian Sets vs. Strongly Cantorian Sets (Forster)
In classical mathematics, the size of a set \(A\) equals the size of its singletons \(\{\{x\} \mid x \in A\}\). In New Foundations, mapping an element to its singleton (\(x \mapsto \{x\}\)) is an impredicative operation that raises its logical type from \(n\) to \(n+1\). This establishes a profound distinction between two classes of sets:
- Cantorian Sets: A set \(A\) is Cantorian if there exists some internal bijection \(f: A \to \iota``A\). The set and its singletons share identical cardinality, though the bijection \(f\) may not be the standard singleton mapping.
- Strongly Cantorian Sets: A set \(A\) is Strongly Cantorian if the canonical singleton function itself (\(x \mapsto \{x\}\)) exists as a set within the universe.
Cantorian Set:
Exists abstract bijection f : A ──► Singletons(A)
Strongly Cantorian Set:
Direct singleton map (x ↦ {x}) is an internal setStrongly Cantorian Sets as “Classical Sanctuaries”
Strongly Cantorian sets serve as islands of classical stability inside the non-well-founded universe.
Because the singleton function exists internally for a Strongly Cantorian set, variables bounded strictly within that set can have their typestate levels raised or lowered freely (\(T(n) = n\)). Stratification restrictions vanish within these boundaries.
┌──────────────────────────────────────────────┐
│ Universal Set V (Non-Well-Founded) │
│ │
│ ┌────────────────────────────────────────┐ │
│ │ Strongly Cantorian: Nat, Lists, Graphs │ │
│ │ - Stratification neutralized: T(n) = n │ │
│ │ - Classical ZFC algorithms safe │ │
│ │ - Direct singleton bijection │ │
│ └────────────────────────────────────────┘ │
│ │
│ Outer Field: Universal Monics, SC(V) = V │
└──────────────────────────────────────────────┘Mechanical Utility for Computational Engines:
Standard discrete data structures—natural numbers (\(\mathbb{N}\)), finite trees, lists, and state transition graphs—are provably Strongly Cantorian. When evaluating algorithms over these collections, a compiler or theorem prover can safely bypass \(+1\) type-elevation guards (such as Hailperin’s Axiom P2), executing operations with zero stratification friction.
NFU as an “Elementary” Foundation (Holmes)
M. Randall Holmes demonstrated in Elementary Set Theory with a Universal Set that Jensen’s NFU provides an intuitive foundation for concrete mathematics:
- Burali-Forti Resolution: The paradox of the largest ordinal is resolved through the \(T\)-operation: \(T^2(\Omega) < \Omega\). The order type of the ordinals is strictly greater than the order type of its double-singleton image, meaning the collection of all ordinals possesses no maximum Cantorian ordinal.
- Frege Arithmetic: Natural numbers are instantiated as equivalence classes of equinumerous finite sets (0 is \(\{\emptyset\}\), 1 is the set of all singletons), avoiding the asymmetric nesting of von Neumann ordinals.
- Stratified \(\lambda\)-Calculus: Functions replace sets as the fundamental primitive. The Axiom of Abstraction generates functions \((x \mapsto T)\) for expressions \(T\) stratified relative to \(x\), implementing sets as characteristic functions mapping terms to truth-value projectors.
2024–2025: Absolute Consistency of Pure NF (Holmes & Wilshaw)
For nearly ninety years, the consistency of pure New Foundations (without Urelements) remained one of the most famous open problems in mathematical logic. In 2024 and 2025, M. Randall Holmes and Sky Wilshaw completed and formalized the definitive proof that New Foundations is Consistent.
Simple Theory of Types (TST) ──► Tangled Type Theory (TTT)
│
▼
NF Formalized in Lean 4 ◄── Freedom of Action TheoremThe Mechanism of Tangled Type Theory (TTT)
Holmes and Wilshaw reduced the consistency of NF to the consistency of Tangled Type Theory (TTT).
TTT is a multi-sorted first-order logic indexed by a limit ordinal \(\lambda\). Unlike standard type theory where membership is restricted to consecutive tiers (\(x^n \in y^{n+1}\)), Tangled Type Theory permits membership relations across arbitrary gaps whenever the source index is strictly lower than the target index (\(\alpha < \beta\)):
\[x^\alpha \in y^\beta \quad \text{for any } \alpha < \beta < \lambda\]
The proof centers on the Freedom of Action Theorem: every locally coherent structural approximation on atoms and litters can be extended into a global allowable permutation preserving the entire membership hierarchy. By formalizing this inductive construction in the Lean 4 proof assistant, Wilshaw verified that Quine’s 1937 syntactic foundations are fully sound.
Problem Set: Categorical Mapping
Problem 5.1: Tracking the T-Operation
In your future categorical ontology, a node representing a Strongly Cantorian set requires a specific flag.
Conceptually, how does tracking the \(T\)-operation allow an automated system to bypass the strict \(+1\) typing requirements of Hailperin’s Axiom P2?