8. Stratified Semantics (McLarty & Forster)
The Crisis of Categorical Closedness in NF
Categorical logic relies heavily on Cartesian Closed Categories (categories equipped with products and exponentials) to provide semantics for the \(\lambda\)-calculus. Because Quine’s New Foundations (NF) permits a universal set (\(V\)) and avoids external class hierarchies, it initially appeared to be the ideal foundation for a self-containing “Category of all Categories.”
However, evaluating New Foundations through categorical semantics exposes a critical structural paradox.
- McLarty, C. (1992). Failure of Cartesian closedness in NF. Journal of Symbolic Logic, 57(2), pp. 555–556.
- Forster, T., Lewicki, A., & Vidrine, A. (2019). Category Theory with Stratified Set Theory. Sections 1–4.
McLarty: The Failure of Cartesian Closedness (1992)
In 1992, Colin McLarty definitively proved that the category of sets within New Foundations cannot constitute a topos, and furthermore, it is fundamentally not Cartesian Closed.
A topos represents an idealized mathematical universe possessing:
- Finite limits (products, pullbacks, equalizers).
- Cartesian closedness (exponential function objects \(B^A\) with evaluation maps).
- A subobject classifier (\(\Omega\)).
McLarty constructed a devastating proof using the internal language of a topos:
Subsets have Monic Inclusions
│
▼
Every Set has a Monic to V
│
▼
Topos Collapses to a Trivial Point- In NF, every subset \(S \subseteq A\) possesses a canonical monic inclusion function \(S \hookrightarrow A\).
- Because \(V\) contains all sets, every set in the universe possesses a monomorphism (an injective embedding) into the Universal Set \(V\).
- McLarty proved a foundational lemma: Only a trivial topos (where all objects collapse into a single terminal point) can possess an object to which every other object has a monic mapping.
- If pure NF possessed full exponential objects \(B^A\) with standard evaluation maps \(ev(f, x) = f(x)\), a Cantorian diagonal subobject \(R \subseteq V\) can be constructed such that both \(i(R) \in R\) and \(\sim(i(R) \in R)\) evaluate as true.
The Architectural Consequence: In pure NF, if categorical products \(A \times B\) exist, classical exponentials \(B^A\) cannot. True function abstraction fails structurally under strict Cartesian conditions.
Forster, Lewicki, and Vidrine: Stratified Pseudo Elephants (2019)
If classical Cartesian closedness fails, how do we execute category theory inside New Foundations?
In 2019, Thomas Forster, Adam Lewicki, and Alice Vidrine resolved this foundational crisis by formalizing categorical structures native to stratified boundaries: the Stratified Pseudo Elephant (SPE).
Standard Evaluation (Breaks Stratification):
ev(⟨x, f⟩) = f(x) : A × B^A ──► B
Stratified Evaluation (T-Functor Guarded):
ev_T(⟨T(x), f⟩) = T(f(x)) : TA × (A ⇒ B) ──► TBThe \(T\)-Functor & Pseudo-Cartesian Closure
Standard evaluation \(\text{ev}(\langle x, f \rangle) = f(x)\) fails in NF because the function \(f\) (a set of pairs) and the element \(x\) operate across unequal stratification tiers.
Forster et al. achieved Pseudo-Cartesian Closure by routing evaluations through the \(T\)-Functor (\(T: \mathcal{C} \to \mathcal{C}\)), which maps objects to their unit subsets (\(x \mapsto \iota``x\)). The stratified evaluation arrow executes legally as:
\[\text{ev}_T : TA \times (A \Rightarrow B) \longrightarrow TB\]
By shifting the domain and codomain through the \(T\)-functor, the typing disparity is algebraically balanced.
The Stratified Yoneda Lemma
Because of the typing differential between arrows and objects, the classical Yoneda isomorphism fails in NF. The authors formulated the Stratified Yoneda Lemma, which accounts for the \(T\)-functor shift across natural transformations:
\[\text{Nat}(\mathcal{C}(U, -), F) \cong T(F(U))\]
The Structure of a Stratified Pseudo Elephant (SPE)
A Stratified Pseudo Elephant (SPE) is a regular category equipped with:
- Finite coproducts and a subobject classifier (\(2 = \{\bot, \top\}\)).
- A full embedding endofunctor \(T\) generating finite limits.
- Relative adjunctions for pullbacks and pseudo-power objects.
Within an SPE, the subcategory of Strongly Cantorian sets forms a true elementary topos. Classical topos logic remains completely operational inside the Strongly Cantorian core, while the outer SPE environment safely encompasses the universal set \(V\) without triggering McLarty’s collapse.
Guided Example: Functorial Mapping
A functor \(F\) maps objects to objects, and morphisms to morphisms, preserving structure.
{
"functor": "T",
"maps_object": { "from": "A", "to": "T(A)" },
"maps_morphism": { "from": "f", "to": "_____" }
}(Hint: If the functor is \(T\), and it maps morphism \(f\), what is the standard notation for the resulting mapped morphism?)
The Stratified Pseudo Elephant (SPE)
The resulting categorical environment is called a Stratified Pseudo Elephant (SPE). It operates as a regular category with finite coproducts, a subobject classifier, and a full embedding endofunctor \(T\). Within an SPE, only the subcategory of Strongly Cantorian sets forms a true elementary topos.
API Schema: SPE Flags
When modeling this environment, you will use the following JSON metadata structure on your root category object:
{
"category_type": "Stratified_Pseudo_Elephant",
"true_topos_subcategory": "strongly_cantorian",
"T_functor_applied": true
}Use these exact keys when completing the problem sets to ensure your model mathematically aligns with Forster’s resolution.
Problem 8.1: The T-Functor JSON Property
To bypass stratification violations in evaluation maps, Forster uses the \(T\)-functor. Write the JSON structure for a morphism that utilizes the T_functor_applied flag to legally execute a pseudo-evaluation across type boundaries.
Problem 8.2: Topos Boundaries
Because NF is not Cartesian Closed natively, only the subcategory of Strongly Cantorian sets forms a true Elementary Topos.
Write the JSON structural properties that establish the system as a Stratified_Pseudo_Elephant, while allowing the true_topos_subcategory to be extracted based on the strongly_cantorian property.