4. The Axiom of Choice Crisis

Specker, Orey, and Jensen: Stress-Testing the Monistic Universe

While Hailperin proved Quine’s system could be finitely mechanized, the mid-century saw mathematical logicians stress-testing the topological reality of this Monistic Universe against the established boundaries of Zermelo-Fraenkel (ZF).

Suggested Reading:
  • Specker, E. P. (1953). The Axiom of Choice in Quine’s New Foundations for Mathematical Logic. Proceedings of the National Academy of Sciences, 39(9).
  • Orey, S. (1956). On the Relative Consistency of Set Theory. The Journal of Symbolic Logic, 21(3).
  • Jensen, R. B. (1969). On the Consistency of a Slight Modification of Quine’s New Foundations. Synthese, 19(1/2), pp. 228-236.

The defining feature of New Foundations (NF) is its explicit permission of a universal set (\(V \in V\)). This structural rule directly collided with classical set-theoretic operations, sparking a foundational crisis.

Specker: The Failure of the Axiom of Choice (1953)

Ernst P. Specker fundamentally altered the trajectory of NF research by proving that the Axiom of Choice (AC) is demonstrably false within pure NF.

Specker did not rely on combinatorial models to prove this; he used raw Cantorian arithmetic. He analyzed the set of all singletons (unit subsets) within the universe, denoted as \(USC(V)\). Because mapping sets to their unit subsets changes their logical type in NF, we must use a \(T\)-operation to compare their cardinalities. Specker proved that Cantor’s theorem manifests in NF as a strict inequality between the size of the singleton set and the universe itself:

\[Nc(USC(V)) < Nc(V)\]

If the Axiom of Choice were true, the universal set \(V\) could be well-ordered. However, Specker demonstrated that attempting to well-order \(V\) forces a direct arithmetic contradiction against this size discrepancy. The universe simply cannot be well-ordered. The monistic rigidity of absolute extensionality forces the Axiom of Choice to fail.

[!WARNING] Because AC is provable for all finite sets, its failure in NF implies the Axiom of Infinity. Specker’s theorem proves Quine’s universe must contain infinitely many elements, but it cannot be well-ordered.

Orey: Relative Consistency Modeling (1956)

Despite the failure of AC, Steven Orey proved that standard set theory could still operate inside NF. Orey utilized the monistic framework of NF as a “host logic” (\(L_2\)) to construct an internal model of a pluralistic, cumulative hierarchy (\(L_1\), specifically von Neumann-Gödel or Zermelo set theory).

Orey embedded the pluralistic ZF universe directly into Quine’s monistic universe by restricting Gödel’s constructible universe mapping functions. Orey created stratified functions \(s\) and \(\sigma\) to ensure the mappings strictly adhered to NF type rules. This proved that a universe forbidding a universal set (ZF) could be perfectly modeled inside a universe containing a universal set (NF).

Jensen: Urelements and the Consistency of NFU (1969)

Recognizing the structural barriers within pure NF, Ronald Björn Jensen salvaged Quine’s stratification approach by introducing a definitive modification: NFU (New Foundations with Urelements).

In standard NF, the Axiom of Extensionality dictates that all objects are sets, defined entirely by their members. Jensen relaxed this axiom to explicitly accommodate Urelements—objects that have no members but are distinct from the empty set.

By breaking the strict monistic reduction of all entities to pure sets, Jensen stabilized the universe. Using Ramsey’s theorem and shifting automorphisms (mapping infinite sets of indiscernibles across domains to preserve truth values), Jensen proved that NFU is consistent, and is fully compatible with both the Axiom of Choice and the Axiom of Infinity.

The Standard Axiom of Extensionality

To complete the upcoming problem set, you must understand how Extensionality is traditionally written in First-Order Logic (FOL): \(\forall x \forall y (\forall z (z \in x \iff z \in y) \implies x = y)\)

(Translation: For all sets \(x\) and \(y\), if they contain the exact same elements \(z\), then \(x\) and \(y\) are identical.) When Urelements are introduced, this strict axiom must be modified because Urelements have no members, but are not identical to the empty set.

Guided Example: The Empty Set vs Urelement

If we permit Urelements, both they and the empty set share the property of having no members: \(\forall y (y \notin x)\).

To distinguish them, some formalizations state that a Urelement is uniquely identical to its own singleton set, while the empty set is not.

Empty Set: \(x = \emptyset \iff \forall y (y \notin x) \land x \neq \{x\}\) Urelement: \(x \in U \iff \forall y (y \notin x) \land \_\_\_\_\_\_\_\_\_\_\)

(Hint: How would you express the condition that the Urelement IS identical to its own singleton?)


The Pivot to JSON: Urelements as Atomic Primitives

In our forthcoming JSON ontology, Urelements represent atomic data primitives (like strings, integers, or booleans). These atomic nodes do not structurally contain other elements (they have no members), yet they are fundamentally distinct from an empty container (like an empty JSON array [] or object {}). By allowing objects that are not sets, NFU perfectly mirrors the architecture of a standard computational database where sets/arrays eventually bottom out at raw, non-iterable data primitives.

Problem Set: Logical Construction of Urelements

Problem 4.1: Urelements vs The Empty Set

In standard ZFC, the only object with no members is the empty set (\(\emptyset\)). In NFU, there are multiple objects with no members (urelements), plus the actual empty set.

Write out the First-Order Logic definitions that clearly distinguish the empty set from an urelement, ensuring you account for extensionality.

Problem 4.2: The Choice Axiom Restoration

Specker proved that AC fails in pure NF because the universe contains too many symmetrical “large” sets.

Explain conceptually (using logic rather than code) how the introduction of urelements breaks this symmetry and allows the Axiom of Choice to function without triggering a contradiction.


Next: Untyped Universes ➔