7. Higher-Order Logic (Lambek & Scott), Barr, and Wells
Categorical Semantics for Logic and Computation
To successfully map our NF ontology to JSON, we must understand how logical derivation and computational states are inherently structural.
J. Lambek and P.J. Scott’s Introduction to Higher-Order Categorical Logic (1986) demonstrated the fundamental mathematical equivalence between structural logic systems and specific category types. Barr and Wells’ Category Theory for Computer Science (1990) extended these maps directly into computational state architecture.
- Mac Lane, S. (1998). Categories for the Working Mathematician. Ch. I (§5), Ch. II (§3), Ch. III (§4–§6), Ch. IV (§6).
- Holmes, M. R. (2012). Elementary Set Theory with a Universal Set. Ch. 11.1, 11.3 (Operations on Functions; Stratification), Ch. 23.1, 23.3 (Abstraction; State Machines & C-Monoids).
- Wilshaw, S. (2025). New Foundations is Consistent. Sections 3.1, 3.2 (Codes and Clouds) and Section 4.6 (Structural Actions).
The Equivalence of Logic and Category
Lambek and Scott established a strict dictionary between formal deductive systems, \(\lambda\)-calculus, and Category Theory:
| Category Theory | Logical Semantics | Typed \(\lambda\)-Calculus |
|---|---|---|
| Object \(A\) | Formula \(A\) | Type \(A\) |
| Arrow \(f: A \rightarrow B\) | Proof of \(A \vdash B\) | Term \(f(x)\) of type \(B\) |
| Terminal Object \(1\) | Truth \(\top\) | Basic term \(*\) |
| Product \(A \times B\) | Conjunction \(A \wedge B\) | Product Type |
| Exponential \(B^A\) | Implication \(A \Rightarrow B\) | Function Type / Abstraction |
| Evaluation \(\epsilon_{A,B}\) | Modus Ponens | Application |
Functional Completeness
A major achievement of categorical logic is Functional Completeness: the ability to eliminate bound variables entirely. Any logical deduction dependent on an assumed variable can be algebraically translated into a pure categorical morphism composed of constant structural arrows (evaluations, projections, exponential adjoints). This proves that logic is structurally geometric.
Untyped Systems and C-Monoids
While typed \(\lambda\)-calculus strictly correlates to Cartesian Closed Categories, the untyped \(\lambda\)-calculus semantically maps to C-Monoids. A C-monoid is a single-object Cartesian Closed Category that explicitly excludes a terminal object. Because NF allows for a universal set, handling untyped or reflexively typed loops requires leveraging these specialized single-object mapping behaviors.
Computer Science and State Transitions
Barr and Wells contextualized these categorical mappings directly into functional programming.
- Programs as Arrows: Functions \(f: S \to T\) operate as structural morphisms. Anonymous functions (\(x \mapsto x^2\)) define internal operational paths distinct from their formal signature.
- Types as Objects: Data types (Booleans, Integers, complex structs) function as the objects defining the domain and codomain boundaries.
- State Machines as Monoids: A classical automaton operating on an input alphabet acts algebraically as a Monoid (a single object category) where the input string evaluates as a directed path navigating through a free category.
Guided Example: Categorical Modus Ponens
In a Cartesian Closed Category, logical deduction is a geometric mapping. If we have an exponential object \(B^A\) (representing \(A \to B\)) and the domain object \(A\), the “Evaluation” morphism (\(eval\)) maps their product to the target.
\(eval : B^A \times A \to \_\_\_\_\_\)
(Hint: What is the resulting object when you successfully apply a function to its required input?)
Translating to JSON: Products and Limits
When building your JSON ontology, you must translate these Cartesian elements into explicit properties:
- The
sourceArray: In a Cartesian Closed Category, evaluating a function requires the cross-product of the function and the input (\(B^A \times A\)). In JSON, represent products by feeding an array of IDs into thesourcekey:"source": ["Exponential_Object", "Domain_Object"]. - The
topology_limitsConstraint: Because C-Monoids lack a terminal object, your JSON models must enforce this structurally. Adding"topology_limits": ["no_terminal_object"]to your morphism’sconstraintsarray establishes the structural boundary your future proofs must rely on to prevent recursive paradoxes when tracing compositions.
Problem 7.1: Modeling Modus Ponens
In a Cartesian Closed Category (CCC), the logical rule of Modus Ponens is modeled geometrically via the Evaluation Arrow.
Write the JSON structure for a morphism that evaluates \(B^A \times A \to B\). How will you define the source array to represent the product of the exponential object and the domain?
Problem 7.2: The C-Monoid Topology
To model an untyped lambda calculus (or an untyped universe like \(V\)), Lambek introduced the C-Monoid.
Since a C-Monoid lacks a terminal object (to prevent paradoxes), how will you design your JSON syntax to process arrow compositions without hitting a recursive loop? Define the topology_limits constraint in JSON.