8. Stratified Semantics (McLarty & Forster)
The Crisis of Categorical Closedness in NF
Categorical logic relies heavily on Cartesian Closed Categories (categories with products and exponentials) to provide semantics for the \(\lambda\)-calculus. Because Quine’s New Foundations (NF) permits a universal set and avoids external class hierarchies, it seemed like the perfect foundation for a “Category of all Categories.” However, evaluating NF through categorical semantics exposes a critical structural paradox.
- McLarty, C. (1992). Failure of Cartesian closedness in NF. Journal of Symbolic Logic, 57(2), pp. 1-25.
- Forster, T., Lewicki, A., & Vidrine, A. (2019). Category Theory with Stratified Set Theory.
- Holmes, M. R. (2012). Elementary Set Theory with a Universal Set. Ch. 3 (Boolean Operations), Ch. 17.1 (Exponentiation meets T), Ch. 19.2 (ZFC in Cantorian Ordinals).
- Forster, T. (1995). Set Theory with a Universal Set. Sections 1.4 (Avoiding paradoxes) and 2.2.2 (Closure properties of small sets).
- Wilshaw, S. (2025). New Foundations is Consistent. Sections 3.3, 5.4, 7.1, and 7.2 (Singletons, Recoding, and Proving Consistency).
McLarty: The Failure of Cartesian Closedness (1992)
Colin McLarty definitively proved that the category of sets within NF cannot constitute a topos, and furthermore, it is not Cartesian Closed.
A topos represents a mathematical universe possessing finite limits, Cartesian closedness (exponential objects for functions), and a subobject classifier (\(\Omega\)). McLarty demonstrated that:
- In NF, subsets have monic inclusion functions.
- Therefore, every set has a monic mapping to the Universal Set \(V\).
- Using the internal language of a topos, McLarty proved that only a trivial topos can have an object to which every other object has a monic mapping.
- Because NF contains a universal monic, assuming it has exponential objects (like \(B^A\)) leads to a direct contradiction.
Thus, in pure NF, if categorical products exist, exponentials do not. True function abstraction fails structurally under strict Cartesian conditions.
Forster, Lewicki, and Vidrine: Stratified Pseudo Elephants (2019)
If true Cartesian closedness fails, how do we perform category theory in NF? Thomas Forster, Adam Lewicki, and Alice Vidrine resolved this by formalizing categorical mechanics native to NF’s stratified boundaries.
The category of NF sets (Category N) achieves Pseudo-Cartesian Closure through the T-Functor. The standard evaluation map \(ev(\langle x, f \rangle) = f(x)\) violates Quine’s stratification rules. To fix this, the T-functor maps elements to their singletons (\(x \mapsto \{x\}\)). The pseudo-evaluation arrow operates via \(TA \times (A \Rightarrow B) \to TB\), mathematically resolving the typing barrier.
The Stratified Yoneda Lemma
Because of the typing differentials between morphisms and objects, the classical Yoneda isomorphism fails in NF. The authors formulated the Stratified Yoneda Lemma, mapping natural transformations to the target object modified by the T-functor:
\[Nat(C(U,-),F) \cong T(F(U))\]
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.