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 focus from defensive consistency proofs toward exploiting the unique topological topology of an untyped universe.
In the logicist tradition, sets represent predicates-in-extension. Conscious experience and conceptual frameworks are unitary; imposing external hierarchies (like ZF) fragments this unitary perspective. Set theories with a universal set treat \(V\) as a legitimate, manipulable object, creating 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).
Cantorian and Strongly Cantorian Sets (Forster)
In standard math, the size of a set \(x\) is trivially equal to the size of its singletons \(\{x\}\). In NF, mapping a set to its singletons changes its logical type, requiring the \(T\)-operation (type-raising).
- Cantorian: A set \(x\) is Cantorian if there exists some bijection between \(x\) and its singleton set \(\iota`x\).
- Strongly Cantorian: A set is Strongly Cantorian if the restriction of the singleton function itself (\(f(x) = \{x\}\)) acts as that bijection.
[!TIP] Subverting Stratification Strongly Cantorian sets subvert stratification requirements. Variables bounded within Strongly Cantorian sets can have their types raised or lowered freely during logical deductions, making them incredibly powerful tools for mathematical proofs.
Mechanical Implications for Software Engines: Because a Strongly Cantorian set has a natural bijection with its singletons, you can safely ignore the strict \(+1\) typing flags (like Hailperin’s Axiom P2) when evaluating variables bounded strictly within that set. It allows your ontological framework to treat the set as a perfectly stable type across all boundaries.
Guided Example: T-Operation Shift
The \(T\)-operation raises the type of a set by mapping it to its singletons.
If we have a base set \(A = \{1, 2, 3\}\), then applying the \(T\)-operation yields: \(T(A) = \{\{1\}, \{2\}, \_\_\_\_\_\}\)
(Hint: What is the singleton of the final element in set A?)
NFU as an “Elementary” Foundation (Holmes)
M. Randall Holmes utilized Jensen’s NFU to build a comprehensive foundation for mathematics in his text Elementary Set Theory with a Universal Set. Because NFU permits a universal set, absolute complements, and Boolean algebra, it supports the natural, intuitive constructions found in Frege’s “naive” set theory without triggering paradoxes.
Holmes successfully implements: 1. Burali-Forti Resolution: Proving \(T^2(\Omega) < \Omega\) (the order type of the ordinals is strictly greater than the order type of its double-singleton image), meaning the set of all ordinals possesses no maximum Cantorian ordinal.
Surreal Numbers: Instantiated as equivalence classes of iterated cut systems.
Stratified \(\lambda\)-Calculus: Replacing sets with functions as the fundamental primitive.
2025: The Absolute Consistency of Pure NF (Wilshaw)
For nearly 90 years, pure NF (without Urelements) remained an open consistency problem. In 2024/2025, M. Randall Holmes and Sky Wilshaw finalized the absolute proof that NF is Consistent.
They proved that NF is consistent if and only if Tangled Type Theory (TTT) is consistent. TTT functions as a multi-sorted first-order theory parametrized by a limit ordinal \(\lambda\). By establishing the “Freedom of Action” theorem (proving every coherent structural approximation approximates a valid allowable permutation), they formalized the multi-sorted construction computationally in the Lean theorem prover, permanently vindicating Quine’s original 1937 architecture.
- Holmes, M. R. (2012). 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. 21 (Surreal Numbers), Ch. 23 (Stratified Lambda-Calculus).
- Forster, T. (1995). Set Theory with a Universal Set. Section 2.1.1 (The axiom of counting) and Section 2.2 (Cardinal and ordinal arithmetic).
- Wilshaw, S. (2025). New Foundations is Consistent. Sections 1.1 - 1.5 (Transitioning to TTT and finite axioms) and Section 4.4 (Freedom of Action).
Prerequisite Stratification Review: If you struggle with the syntactic mechanics of the \(T\)-operation below, we recommend reviewing Holmes (2012) Chapter 7 (Stratified Comprehension) before proceeding.
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?