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?
Best Answer
There are two concepts in category theory that correspond to $\land$ and $\lor$:
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).
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$.
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: