Adjoint of Pushout as Modal Operators in Internal Logic

Regarding the internalization of mathematics to a particular category as in the nLab article: Internal Logic, there is a peculiar table mentioned in the section on Categorical Semantics in which there is a corresponding category-theoretic construction to the regular logical operators in a theory. In particular, $\wedge$ corresponds to a pullback of a cospan, $\top$ corresponds to the top element (A itself), $\wedge$ corresponds to union, $\bot$ corresponds to the bottom element (strict initial object), $\Rightarrow$ corresponds to the Heyting implication, $\exists$ corresponds to the left adjoint to a pullback (I'm not sure which pullback in particular?), and $\forall$ corresponds to the right adjoint to a pullback (what pullback is this also?).

Would it be possible to define the modal operators of $\Box$ and $\Diamond$ as the right adjoint of a pushout (similarly to how $\forall$ is the right adjoint to a pullback) and the left adjoint of a pushout (similarly to how $\exists$ is the left adjoint to a pullback), respectively? Or, if this does not work, could it be possible to define modal operators in internal logic using some other category theoretic construction?

Probably you should get a hold of a textbook on categorical logic for some of these questions. Of the references given in the Wikipedia article, the one by Lambek & Scott and the two with Lawvere as an author might be a good start. A study of these would probably help make the table in the nLab seem less "peculiar".

I see that Wouter Stekelenburg has posted an answer just as I started this, but it wouldn't hurt to amplify. The propositional connectives (on predicates of a given type $A$) are interpreted as operations on the poset of subobjects $Sub(A)$ (e.g., the pullback of two subobjects of $A$ is another subobject of $A$ which corresponds to the meet). Next, each morphism $f: B \to A$ in the category induces an inverse image operation $f^{-1}: Sub(A) \to Sub(B)$, formally defined by taking a pullback: if $i: U \to A$ is a monomorphism, then the pullback of the cospan $(f, i)$ is given by a pair of maps $(g: V \to U, j: V \to B)$ where one may show easily from general properties of pullbacks that $j$ is a monomorphism, thus giving a subobject of $B$. In the classical case where $f$ is a projection map $\pi: X \times A \to A$, you can think of the inverse image $\pi^{-1}: Sub(A) \to Sub(X \times A)$ as interpreting the operation which takes a predicate $\phi$ of type $A$ and forming a predicate of type $X \times A$ by harmlessly adjoining a variable of type $X$, e.g., by taking $\phi \wedge [x = x]$.

Then quantifiers $\exists_f$, $\forall_f$ are operations $Sub(B) \to Sub(A)$ that are left and right adjoint (respectively) to $f^{-1}: Sub(A) \to Sub(B)$. It might help to consider the classical case where $f$ is the projection $\pi: X \times A \to A$. Here the left adjoint $\exists_f$ takes a subobject of $X \times A$ (that interprets a predicate $\phi(x, a)$ of type $X \times A$) to one of type $A$, interpreting the predicate that is usually denoted $\exists_x \phi(x, a)$. (In other words, classical quantification has to do with adjoints to puling back along projection maps $\pi$.) The adjunction between $\exists_{\pi}$ and $\pi^{-1}$ corresponds to the inference rule

$$\exists_x \phi(x, a) \vdash \psi(a) \qquad \mathrm{iff} \qquad \phi(x, a) \vdash \psi(a) \wedge [x = x]$$

where the entailment symbols are interpreted as subobject inclusions in the appropriate posets $Sub(A)$, $Sub(X \times A)$. (Normally one isn't so fussy as to write $\psi(a) \wedge [x = x]$; one usually writes simply $\psi(a)$, but keeping in mind that $\psi$ is here being considered a predicate of type $X \times A$, so that the types match.)

Your guesses about the modalities are a little off. There are lots of places to read about categorical semantics of modal logic; one nice place (for S4 necessity) is in the paper by Awodey and Kishida. It might help first to be familiar with the topological semantics of "necessity" as a topological interior operation on power sets $\Box = \mathrm{int}: P(A) \to P(A)$, due originally to Tarski.

The pullback $\forall$ and $\exists$ are adjoint to the inverse image map of a morphism, which sends a subobject to its pullback along the morphism. I don't know what a pushout of a subobject is, though you could give that name to either $\exists$ or $\forall$. In those cases one of your modalities is simply the pullback, however.

Kripke models of modal logic are related to sheaf models of constructive logic, and the modalities themselves are functors- or even monads-up-to-logical-equivalence depending on the modal logic.

• @Wouter Stekelenburg: I'm confused about how you could "give that name to either $\exists$ or $\forall$ and have your modalities being the pullback." If this is the case, then I would be interested in defining this as I think there are interesting properties that you could prove given that you can category-theoretically describe the modal operators of a theory. Do you have a more thorough description of this, or a reference that I can look at? It's not that your answer is unsatisfactory, but I don't fully understand it and want to find out where you know this from. – Samuel Reid Feb 11 '13 at 16:54
• I said one of your modalities would be the pull back. If $\exists$ is the pushout and that $\Box$ is the right adjoint of the pushout. Then $\Box$ is the inverse image map, because the inverse image map is right adjoint to $\exists$, and adjoints are unique (... up to unique equivalence, but for subobjects, equivalence is equality). – Wouter Stekelenburg Feb 11 '13 at 18:51