4. The Axiom of Choice Crisis

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

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

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), pp. 972–975.
  • Orey, S. (1956). On the Relative Consistency of Set Theory. The Journal of Symbolic Logic, 21(3), pp. 280–290.
  • 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 authorization of a universal set (\(V \in V\)). This structural rule directly collided with classical set-theoretic operations, sparking a foundational crisis across cardinal arithmetic, choice principles, and extensionality.


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

In 1953, Ernst P. Specker established a profound result in non-well-founded mathematics: the Axiom of Choice (AC) is demonstrably false within pure New Foundations.

In classical set theory (ZFC), the map sending each element to its singleton (\(x \mapsto \{x\}\)) is a direct bijection, meaning a set and its singletons share identical cardinality. In NF, however, mapping \(x\) to its singleton \(\{x\}\) elevates its logical type from \(n\) to \(n+1\). To compare cardinalities across stratification tiers, Specker introduced the \(T\)-operation:

\[T(m) = \text{Nc}(\text{USC}(a)) \quad \text{where } m = \text{Nc}(a)\]

Specker analyzed the power set of the universal set, \(\text{SC}(V)\). Because every subset of \(V\) is itself an entity in the universe, the power set is identical to the universe itself: \(\text{SC}(V) = V\). Cantor’s theorem manifests in NF as a strict inequality between the collection of unit subsets (\(\text{USC}(V)\)) and the universal set:

\[\text{Nc}(\text{USC}(V)) < \text{Nc}(V)\]

Classical ZFC:
  |Singletons(A)| = |A|  ──►  Cantor: |A| < |PowerSet(A)|

Quinean NF:
  |PowerSet(V)| = |V|    ──►  Cantor: |USC(V)| < |V|

If the Axiom of Choice held in NF, the universal set \(V\) could be well-ordered. Specker proved that well-ordering \(V\) forces its cardinalities to satisfy finite arithmetic identities (\(n = T(n)+1\) or \(n = T(n)+2\)) that are mathematically impossible for finite cardinals. The absolute extensionality of a universal set shatters the Axiom of Choice.

WarningThe Provability of Infinity

Because the Axiom of Choice is provably true for all finite sets, its refutation in NF directly proves that the universe must be infinite. Unlike ZFC, which requires a standalone Axiom of Infinity, pure NF derives the existence of an infinite universe as an internal deductive theorem.


Orey: Relative Consistency & Host Logic Modeling (1956)

Despite the failure of the Axiom of Choice, Steven Orey demonstrated that classical set theory can be embedded directly inside New Foundations.

Orey utilized NF as a Host Logic (\(L_2\)) to construct an internal simulation of a cumulative, pluralistic hierarchy (\(L_1\), specifically von Neumann-Bernays-Gödel set theory). By restricting Gödel’s constructible universe mapping functions with stratified indexing parameters \(s\) and \(\sigma\), Orey proved:

\[\text{Con}(NF) \implies \text{Con}(ZFC)\]

A universe that contains a universal set (\(V \in V\)) possesses sufficient structural capacity to model a universe that strictly forbids a universal set (ZFC). The pluralistic hierarchy of classical mathematics emerges as a localized simulation running inside a flat, monistic host logic.


Jensen: Urelements and the Consistency of NFU (1969)

To restore the Axiom of Choice and resolve consistency concerns, Ronald Björn Jensen engineered NFU (New Foundations with Urelements).

In pure NF, the Axiom of Extensionality dictates that all objects are sets, defined entirely by their constituent members. Any two entities sharing the exact same elements must be identical. Jensen weakened extensionality to apply only to non-empty collections:

\[\exists z (z \in x) \implies (\forall z (z \in x \leftrightarrow z \in y) \implies x = y)\]

Collections containing at least one member remain strictly extensional. However, entities containing no members are exempted. This permits the coexistence of the true empty set alongside distinct Urelements (atoms that contain no members, yet are distinct from the empty set).

Pure NF:   Object with no members  ──►  Must be Empty Set ∅  (Extensionality Rigid)
NFU:       Objects with no members ──►  Empty Set ∅ OR Urelements u₁, u₂, u₃... (Buffered)

By introducing Urelements, Jensen broke the rigid extensional symmetry of the universal set. Using Ramsey’s theorem on infinite sets of indiscernibles and shifting automorphisms (\(\sigma: U_i \to U_{i+1}\)), Jensen proved:

  1. NFU is Consistent: Its consistency is provable within elementary number theory (Peano Arithmetic).
  2. Full Compatibility with Choice and Infinity: Both the Axiom of Choice and the Axiom of Infinity can be added to NFU without triggering Specker’s contradiction.

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 ➔