Categorical models of logics

A few days ago I wrote about topological models of modal logic. If you find general topology more familiar than modal logic, this correspondence could be helpful. If you think the motivation for general topology is evident but the motivation for modal logic is suspect, the correspondence between the two fields might relieve some of your suspicion of the latter. Topological models, however, are quite limited. You can’t model provability logic, for example, by the usual approach to constructing topological models, though there is an alternative construction. Categorical models are less limited. You can model a wide variety of logics using categories via the Curry-Howard-Lambek correspondence. This may be cold comfort if you find category theory and logic equally mysterious. Even so, there’s something intriguing about a correspondence between two things you find mysterious. Categorical semantics is deep and broad, but I’ll keep this post brief. The correspondence between logic [1] and…