Practical Foundations of Mathematics

Paul Taylor

Chapter 4
Cartesian Closed Categories

C ategory theory unifies the symbolic (Formalist) and model-based (Platonist) views of mathematics. In particular it offers an agnostic solution to the question that we raised in Section 1.3 of whether a function is an algorithm or an input-output relation.

Traditionally, categories were congregations, each object being a set with structure: a topological space, an algebra or a model of some theory. The morphisms are functions that preserve this structure (homomorphisms), so the notion of composition is ultimately that for relations (Definition 1.3.7). As an approach to logic, this went round ``three sides of a square'' ( cf Remark  1.6.13 for model theory) and so ran into some foundational problems over the category of all categories.

In informatics, the principal examples are constructed from l-calculi and programming languages; being syntactic, they are typically recursively enumerable. Composition is by substitution of terms (Definition 1.1.10), or by the cut rule (Definition  1.4.8), which uses old conclusions as new hypotheses. A category Cn[]L of this kind encodes a certain theory L itself, instead of collecting its models; we call it the category of contexts and substitutions by analogy with categories of objects and homomorphisms in semantics.

We shall give a novel construction of Cn[]L that embodies well-established techniques for proving correctness of programs and works uniformly for any fragment of logic. At the unary level, the ideas come from geometry and physics (groups), automata and topology; we also carry it out for algebraic theories ( Cn×L) before turning to the l-calculus ( Cn® L ).

The fragment of logic in question, [], corresponds to certain categorical structure defined by universal properties: products and exponentials in this chapter, coproducts and factorisation systems in the next. The recursively defined interpretation functor [[-]]:Cn[]L® S preserves this structure, so the semantic universe S must also have it. Cn[]L is also called the classifying category for (models of) the theory, because there is a correspondence between such functors and models in S.