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.

  • $\begingroup$ @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. $\endgroup$ – Samuel Reid Feb 11 '13 at 16:54
  • $\begingroup$ 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). $\endgroup$ – Wouter Stekelenburg Feb 11 '13 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.