Categorical Logic: Structure, Quantification, and Internal Languages

A logical operation can be described by a symbolic rule. It can also be characterized by what constructions it permits and how those constructions compose.

Categorical logic develops the second approach. Products describe pairing, function objects describe abstraction and application, and adjunctions describe the relationship between substitution and quantification.

The purpose is not to replace formulas with unfamiliar vocabulary. A structural description can reveal that apparently different languages have the same mathematical organization, or that the same formal language admits several kinds of interpretation.

The categorical background

Samuel Eilenberg and Saunders Mac Lane introduced category theory in their 1945 paper on natural equivalences, in a setting shaped by algebra and topology.

A category has objects, arrows between objects, identity arrows, and associative composition. Sets with functions form a category. Groups with homomorphisms form another. The arrows specify which relationships the category treats as structure-preserving.

Alexander Grothendieck's work on sheaves and toposes arose from geometry. F. William Lawvere's work in the 1960s brought categorical methods directly into logic and foundations. Joachim Lambek developed close connections between categories, deductive systems, and typed lambda calculus.

These developments supplied several related projects: semantics for formal languages, structural accounts of theories, and proposed axioms for mathematics itself. Their aims should be distinguished even when they use the same categorical tools.

Proofs as composable arrows

Suppose an arrow $f:A\to B$ represents a construction taking evidence for $A$ to evidence for $B$. Another arrow $g:B\to C$ can be composed with it:

Composition expresses a basic form of inference. Identity arrows represent using an assumption directly.

This interpretation alone does not provide every connective. A category must possess suitable additional structure to interpret them.

It also raises a question about proof identity. If two derivations differ only by eliminating an introduction–elimination detour, should they represent the same arrow? A categorical model often identifies proofs according to specified equations. The choice of equations is part of the interpretation.

Products and conjunction

A product $A\times B$ comes with projections

Given arrows $f:X\to A$ and $g:X\to B$, there is a unique pairing

whose composites with the projections are $f$ and $g$.

In sets, the pairing sends $x$ to $(f(x),g(x))$. In the logical interpretation, evidence for $X$ supplies both $A$ and $B$, hence their conjunction.

The equations

correspond to simplifying a proof that first forms a conjunction and then immediately selects a component.

The product is characterized by this universal property. A particular implementation of ordered pairs is secondary to the role they perform.

Function types and cartesian closure

A cartesian closed category has finite products and suitable exponential objects $B^A$. The exponential represents a function type from $A$ to $B$.

Its characteristic relationship is

A construction using an $X$-input and an $A$-input to produce a $B$ corresponds to a construction that uses the $X$-input to produce a function from $A$ to $B$.

In sets, this is currying:

The relationship makes abstraction and application structural. Lambek's work connects this organization with the simply typed lambda calculus, under the relevant equations on terms.

Cartesian closure does not automatically interpret every feature of a modern programming language. General recursion, state, exceptions, and dependent types require further structure or a different semantic treatment.

Quantifiers as adjoints to substitution

Lawvere's account of quantification provides a particularly concrete example of categorical logic.

Let $f:X\to Y$ be a function. A predicate on $Y$ can be represented by a subset $T\subseteq Y$. Substitution along $f$ produces the inverse image

For a subset $S\subseteq X$, define

and

The key relationships are

and

These are adjunctions between partially ordered sets of predicates. Existential quantification is left adjoint to substitution; universal quantification is right adjoint.

To see the first equivalence directly, every image of an element of $S$ lies in $T$ exactly when every element of $S$ maps into $T$. The equation expresses the logical rule through the behavior of substitution.

A finite calculation

Take $X=\{1,2,3\}$ and $Y=\{a,b,c\}$, with $f(1)=f(2)=a$ and $f(3)=b$. Let $S=\{1,3\}$.

Then

Both $a$ and $b$ have a preimage in $S$.

But

The fiber above $a$ contains $2$, which is not in $S$. The fiber above $b$ contains only $3$, which is in $S$. The fiber above $c$ is empty, so every member of that fiber belongs to $S$ vacuously.

Ordinary quantification over a variable appears by taking $f$ to be a projection, such as $X\times Y\to Y$. Quantifying removes the $X$-coordinate while retaining the parameters in $Y$.

Lawvere's “Adjointness in Foundations” develops the broader structural viewpoint. The elementary calculation here illustrates why the language of adjunctions is mathematically informative.

Toposes and internal logic

An elementary topos has finite limits, exponentials, and a subobject classifier. These structures support an internal logical language with a rich interpretation of predicates and functions.

Lawvere and Myles Tierney developed the elementary account around the end of the 1960s, drawing connections with the geometric toposes arising from Grothendieck's work.

The category of sets is a familiar example, but sheaf and other toposes behave differently. Their internal logic is generally intuitionistic; excluded middle requires additional conditions.

This does not mean that an ordinary mathematical observer has changed the external rules used to study the category. One can reason classically about a topos whose internal language does not validate excluded middle. External metatheory and internal logic occupy different levels.

The distinction parallels the separation between a theory and the mathematics used to study its models, now in a structural setting.

Semantics and foundations

Lawvere's Elementary Theory of the Category of Sets, ETCS, proposes structural axioms for a category behaving like sets and functions.

That foundational proposal differs from merely interpreting an existing type theory in a category. Categorical semantics can be carried out inside set theory without replacing set theory as the surrounding foundation.

Conversely, a categorical foundation must specify its own strength. Questions about natural numbers, choice, replacement-like principles, and large collections cannot be settled by the word “category” alone.

Categorical logic therefore broadens the forms that a foundation or model can take. It does not dissolve the need for precise axioms.

From mathematical functions to executable languages

The categorical and type-theoretic accounts clarify the structure of functions and proofs. Executable languages add recursion, evaluation strategies, data representation, and practical type inference.

The next note follows that development while retaining the distinction between a mathematical function, a potentially partial computation, and a proof.

Sources and further reading

• Samuel Eilenberg and Saunders Mac Lane, “General Theory of Natural Equivalences” (1945).
• F. William Lawvere, “An Elementary Theory of the Category of Sets” (1964).
• Joachim Lambek, “Deductive Systems and Categories,” parts I and II (1968–1969).
• F. William Lawvere, “Adjointness in Foundations” (1969); reprint with later commentary.
• F. William Lawvere, “Quantifiers and Sheaves” (1971).
• Joachim Lambek and Philip J. Scott, Introduction to Higher Order Categorical Logic (1986).