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 deduction, computational execution, and categorical geometry are mathematically equivalent.
In Introduction to Higher-Order Categorical Logic (1986), J. Lambek and P.J. Scott established the rigorous isomorphism connecting deductive proof systems, typed \(\lambda\)-calculi, and Cartesian Closed Categories. Michael Barr and Charles Wells (Category Theory for Computer Science, 1990) extended this correspondence directly into computational state machines.
- Lambek, J., & Scott, P. J. (1986). Introduction to Higher-Order Categorical Logic. Cambridge University Press. Part I (§1–§6).
- Barr, M., & Wells, C. (1990). Category Theory for Computer Science. Ch. 1 (§1.1–§1.4) and Ch. 2 (§2.1–§2.3).
The Trinity of Computation (Curry-Howard-Lambek)
The Curry-Howard-Lambek correspondence proves that Logic, Computer Science, and Category Theory represent three distinct vantage points of the exact same mathematical structure:
Category Theory (CCCs)
▲ ▲
╱ ╲
▼ ▼
Proof Theory ◄────► Type Theory
(Propositions) (Programs)| Category Theory | Logical Proof Semantics | Computer Science / Typed \(\lambda\)-Calculus |
|---|---|---|
| Object \(A\) | Proposition / Formula \(A\) | Data Type \(A\) (Int, String, Struct) |
| Arrow \(f: A \to B\) | Deductive Proof of \(A \vdash B\) | Executable Term / Function \(f(x) : B\) |
| Terminal Object \(1\) | Truth Constant \(\top\) | Unit Type () / Primitive Value * |
| Product \(A \times B\) | Conjunction \(A \land B\) | Pair / Product Type (A, B) |
| Exponential \(B^A\) | Material Implication \(A \implies B\) | Function Type A -> B / Closure |
| Evaluation \(\epsilon_{A,B}\) | Modus Ponens Step | Function Application f(a) |
| Initial Object \(0\) | Falsehood \(\bot\) | Empty / Bottom Type Void |
| Coproduct \(A + B\) | Disjunction \(A \lor B\) | Sum / Either Type Either<A, B> |
Functional Completeness: Eliminating Bound Variables
A major achievement of categorical logic is Functional Completeness: any logical deduction that depends on an assumed hypothesis variable \(x: 1 \to A\) can be algebraically translated into a pure morphism composed of constant structural arrows (evaluations, projections, exponential adjoints).
Bound variables are an artifact of human notation. In category theory, computation evaluates as a static, coordinate-free geometric trajectory across arrows.
Untyped Systems and C-Monoids
While typed programming languages correspond strictly to Cartesian Closed Categories, untyped systems (like pure untyped \(\lambda\)-calculus and Quine’s universal set \(V\)) correspond algebraically to C-Monoids.
A C-Monoid is a single-object Cartesian Closed Category that explicitly excludes a terminal object.
Standard CCC (Typed):
Multiple distinct objects A, B, C... + Terminal Object 1
C-Monoid (Untyped):
Single Universal Object U containing all morphisms (No Terminal Object)In an untyped universe where everything is an element of \(V\), every function can accept any other function as input, including itself (\(f(f)\)). If an untyped system possessed a classical terminal object, this universal self-application would trigger an immediate Russellian contradiction, collapsing the category into a single trivial point. C-Monoids provide the exact topological boundary conditions required for an untyped engine to process self-referential loops safely.
State Transitions & Automata (Barr & Wells)
Barr and Wells demonstrated how categorical morphisms execute on physical computing hardware:
- Functions as Arrows: A software routine
fn(x: S) -> Toperates as a morphism \(f: S \to T\). Pure subroutines define deterministic operational paths across typed memory domains. - State Automata as Monoid Actions: A classical state machine with states \(S\) and an input alphabet \(\Sigma\) acts algebraically as a Monoid action. Feeding a string \(w = \sigma_1 \sigma_2 \dots \sigma_n\) into the automaton corresponds to navigating a directed composition path \(\delta_n \circ \dots \circ \delta_1\) across the state transition graph.
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.