categorical interpretation of quantification

Many constructions in intuitionistic and classical logic have relatively simple counterparts in category theory. For instance, conjunctions, disjunctions, and conditionals have analogues in products, coproducts, and exponential objects.

More esoteric concepts still permit reasonably simple categorical interpretations. For instance, the modal operator $\Box$ (necessity) can be described as a monoidal endofunctor (see, for instance, Paiva & Ritter's Basic Constructive Modality (PDF)).

What are the similar constructions that are suitable interpretations for universal and existential quantification in first-order logic?

-
The introduction/elimination rules for quantifiers exhibit them as adjunctions between appropriate categories of formulae. – Zhen Lin Aug 14 '13 at 18:14
I don't know, but if there is such a mapping to category theory, it would be really cool if the quantifiers mapped to dual concepts :) – Thomas Andrews Aug 14 '13 at 18:14
I'm afraid adjunctions require some reasonable understanding of categories and functors. But then again, there's no reason to expect quantifiers to be easy! This is explained briefly in Awodey's Category theory. – Zhen Lin Aug 14 '13 at 18:26
@ZhenLin Thanks for the pointer to Awodey's book. The basic definition of adjunctions (e.g., from Wikipedia) is easy enough to grasp; getting the introduction and elimination rules from them, though, may require some more time at the dry-erase board. :) I'll look at Awodey's book, and the board, and will perhaps have some more luck. – Joshua Taylor Aug 14 '13 at 18:29
@ThomasAndrews The usual universal and existential quantifiers are the right and left adjoints, respectively, of "adding a dummy variable". I'll explain with two variables, but the idea (due to Lawvere) generalizes. Let A be the set of formulas (in a fixed language) with at most $x,y$ free, and let B be the set of formulas with at most $x$ free. A and B are preordered by "provable implication", so they can be viewed as categories. The inclusion functor from B to A has adjoints on both sides. The left adjoint sends $\phi(x,y)$ to $\exists y\,\phi(x,y)$ and the right adjoint uses $\forall$. – Andreas Blass Aug 14 '13 at 19:16

There are two concepts in category theory that correspond to $\land$ and $\lor$:

1. (Binary) categorical products and coproducts, as you mention.
2. Meets and joins as operations on the subobjects of a given object (satisfying the Beck-Chevalley condition).

Similarly, there are two ways to express logical quantifiers as categorical notions. In the following I assume a category $\mathcal{C}$ which has whatever structure is necessary to make sense of what I am saying (I can be more precise if needed).

1. For every arrow $f : A \to B$ there is a pullback functor $f^{*} : \mathcal{C}/B \to \mathcal{C}/A$ which takes an arrow $g : D \to B$ to its pullback $f^{*}(g) : f^{*}(D) \to A$ along $f$. Here $\mathcal{C}/X$ is the slice category over $X$. There is another functor $\Sigma_f : \mathcal{C}/A \to \mathcal{C}/B$ defined on an object $h : E \to A$ as $\Sigma_f(h) = f \circ h$. Then $\Sigma_f$ is left adjoint to $f^{*}$. Sometimes $\mathcal{C}$ is such that $f^{*}$ also has a right adjoint $\Pi_f$ of $f^{*}$. When such structure exists, $\mathcal{C}$ is said to be locally cartesian closed. The existential quantifier corresponds to $\Sigma_f$ and the universal one to $\Pi_f$. More precisely, universal quantification $\forall x \in X . \phi(x, y)$ corresponds to $\Pi_{\pi_1}(\phi)$ where $\pi_1 : X \times Y \to Y$ is the first projection and $\phi : Z \to X \times Y$.

2. There is a subobject functor $\mathsf{Sub} : \mathcal{C}^{\mathrm{op}} \to \mathsf{Poset}$ which takes an object $A$ to the poset of its subobjects and an arrow $f : A \to B$ to the monotone map $f^{*} : \mathsf{Sub}(B) \to \mathsf{Sub}(A)$ which takes a subobject represented by a mono $m : X \to B$ to the subobject represented by $f^{*}(m) : f^{*}(X) \to A$, the pullback of $m$ along $f$. When the posets $\mathsf{Sub}(A)$ are (distributive) lattices, we can interpret $\land$ and $\lor$ as meets and joins. To interpret the quantifiers we again ask for the left and right adjoints of $f^{*}$. The left adjoints exist when $\mathcal{C}$ has stable image factorizations, and these give the existential quantifiers. The right adjoints give the universal quantifiers. There is a little detail called the Beck-Chevalley condition which requires that the adjoints are stable under pullbacks. (In logic the condition corresponds to the fact that substitution commutes with quantifiers.)

We can also express the inference rules for quantifiers in a form that makes it obvious that they are adjoints. Consider the following rule: $$\frac{x : X, y : Y \mid \phi \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ This says: "if $\phi$ entails $\psi$, where $x$ and $y$ are free variables of type $X$ and $Y$ respectively, then $\phi$ entails $\forall x : X . \psi$ with free variable $y : Y$." (Note that $x$ cannot occur free in $\phi$ because $\phi$ appears on the bottom line in a context where only the free variable $y$ is allowed.) This is the introduction rule for $\forall$. But we can turn it around to get the elimination rule: $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid \phi \vdash \psi}$$ This is not the elimination rule as usually stated, which is $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi \qquad a : X}{y : Y \mid \phi \vdash \psi[a/x]},$$ but we can obtain this one from ours by using the rule of substitution: from $\forall x : X . \psi$ first derive $\psi$, and then substiute $a$ for $x$.

Now to be completely precise, we should consider $\phi$ above the line to be different from the one below the line because one appears in the context with variables $x : X$ and $y : Y$, and the other in the context with just $y : Y$. So let us write $[x]^{*}(\phi)$ for the formula $\phi$ considered in the context with the variable $x$ added to it (this is known as weakening in logic, although here we are adding stuff to the typing context, whereas in logic there is also weakening that adds hypotheses). With this notation our rules read as $$\frac{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ and $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}.$$ But this has the form of an adjunction between $[x]^{*}$ and $\forall x : X$! We also see the correspondence between logic and categories clearly now: weakening $[x]^{*}$ corresponds to pullback along the projection $\pi_1 : X \times Y \to X$, and $\forall x : X$ corresponds the functor $\Pi_{\pi_1}$.

I leave it as an exercise for you to figure out how the existential is a left adjoint to weakening. So the moral of the story is that universal and existential quantifiers are rigth and left adjoints of weakening.

References:

• Steve Awodey: Category theory, Oxford University Press. This has a nice and easy explanation of what I wrote above.
• Bart Jacobs: Categorical Logic and Type Theory. This is nuclear weapons, it contains everything and more about the subject, including generalizations that unify the above two views.
-
In “then $\psi$ entails $\forall x \colon X.\psi$ with free variable $y\colon Y$,” should the first $\psi$ be $\phi$? – Joshua Taylor Aug 14 '13 at 19:21
Yes, thanks, I fixed it. – Andrej Bauer Aug 14 '13 at 19:26
They are not called "powerset categories" but "the subobject partial order". For a fixed category $\mathcal{C}$ There is a functor $\mathsf{Sub} : \mathcal{C} \to \mathsf{Poset}$ which maps an object $A$ to the poset of its subobjects (I explained this in my answer). The quantifiers are functors between posets of subobjects, and so that is the same thing as a monotone map. I think you just need to read again and think through these things by yourself. – Andrej Bauer Aug 18 '13 at 22:29
When you pass from propositional logic to predicate logic your category becomes more complicated. In the case of a propositional logic (which is the one you are describing in relation to the modal operator $\Box$), the category itself is just a poset (or something like it), but when you have predicates, you get a poset (or something like it) for each typing context. These posets fit together in what is known as a fibration. Perhaps the point you are missing is this: you must keep very careful track of what free variables are floating around. And then it makes no sense to apply ... – Andrej Bauer Aug 19 '13 at 9:15
... $\forall x$ to a predicate $\phi$ which is formed in a context that does not involve the variable $x$. So we necessarily get an "indexed" or "fibered" variant of the propositional case that you are familiar with. – Andrej Bauer Aug 19 '13 at 9:16

There's a detailed discussion of quantifiers-as-adjunctions in Chapter 15 ("Adjointness and Quantifiers") of Goldblatt's book Topoi: the Categorial Analysis of Logic.

The earlier part of the book contains an explanation of category theory from the ground up, with particular attention to how it relates to logic, so might be a good thing to read if you are interested in logic and trying to understand how category theory relates to it, or are learning about adjunctions for the first time for the purpose of understanding the category-theoretic modeling of quantifiers.

-

Here's a simple-minded version of the basic point here, put in terms of Galois connections.

Let $L$ be a first-order language, and $\mathit{Form}(\vec{x})$ be the set of $L$-wffs with at most the variables $\vec{x}$ free.

Write $\phi(\vec{x})$ for a formula in $Form(\vec{x})$, $|\phi(\vec{x})|$ for the class of formulae logically interderivable with $\phi(\vec{x})$, and $E_{\vec{x}}$ for the set of such equivalence classes of formulae from $\mathit{Form}(\vec{x})$.

Put $|\phi(\vec{x})| \Rightarrow |\psi(\vec{x})|$ iff $|\phi(\vec{x})| \vdash |\psi(\vec{x})|$. Then $\Rightarrow$ is a partial order on $E_{\vec{x}}$.

Now we'll consider two maps between the posets $(E_{\vec{x}}, \Rightarrow)$ and $(E_{\vec{x}, y}, \Rightarrow)$. In other words, we are going to be moving between (classes of) formulae with at most $\vec{x}$ free, and formulae with at most $\vec{x}, y$ free (where $y$ isn't among the $\vec{x}$).

First, since every wff with at most the variables $\vec{x}$ free also has at most the variables $\vec{x}, y$ free, there is a trivial map $f_*$ that sends $|\phi(\vec{x})| \in E_{\vec{x}}$ to the same element $|\phi(\vec{x})| \in E_{\vec{x}, y}$.

Second, we define the companion map $f^*$ that sends $|\phi(\vec{x}, y)| \in E_{\vec{x}, y}$ to $|\forall y\,\phi(\vec{x}, y)| \in E_{\vec{x}}$.

Then $(f_*, f^*)$ is a Galois connection between $E_{\vec{x}}$ and $E_{\vec{x}, y}$. That is to say

$f_*(|\phi(\vec{x})|) = |\psi(\vec{x},y)|\quad$ if and only if $\quad|\,\phi(\vec{x})\,| = f^*(|\psi(\vec{x},y)|)$

For that just restates the familiar logical rule

$\phi(\vec{x}) \vdash \psi(\vec{x},y)\quad$ iff $\quad\phi(\vec{x}) \vdash \forall y\,\psi(\vec{x},y)$

Hence universal quantification is right-adjoint to a certain quite trivial operation. (There's an analogous result for existentials.)

-
Users that like this presentation will appreciate Awodey's presentation in Categorical Logic (which Andrej Bauer mentioned). The presentations are quite similar. – Joshua Taylor Aug 15 '13 at 18:56

The analogue of existential quantification is the dependent sum, and the analogue of universal quantification is the dependent product. The analogy itself passes through the Curry-Howard correspondence.

A simple categorical description of quantification is the following. In a category with pullbacks, any morphism $f : x \to y$ induces a functor $f^{\ast} : \text{Sub}(y) \to \text{Sub}(x)$ from the category of subobjects of $y$ to the category of subobjects of $x$ by taking pullbacks. In a category with finite products, and when they exist, the existential quantifier is the left adjoint to the functor $\text{Sub}(x) \to \text{Sub}(x \times y)$ induced by a projection map $\pi_x : x \times y \to x$, and the universal quantifier is the right adjoint, thinking of $\text{Sub}(x)$ as being described by predicates over $x$ (although strictly speaking we need a subobject classifier to do this).