Applications of Categorical Logic to Logic

This is definitely a very open ended question.

I have been studying Categorical Logic for a while now --- I've read Sheaves in Geometry and Logic, Adámek & Rosický's Presentable Categories, Sketches of an Elephant and some other foundational texts, enough to perhaps say I'm acquainted with the fundamental ideas of categorical logic -- and I'm having a small crisis of faith regarding any actual application of categorical logic. Since I come from Model Theory, I originally wished for some new way of understanding old results, but I recognize that Categorical Logic is a different field and so should not be judged as a dictionary to the past.

Still it seems that after at least 60 years -- counting from Lawvere's thesis -- no real theory has been produced. Yes, functors may be seen as models; yes, presentable categories are sketchable and Yes, categories with enough structure have an internal logic. But so what? It seems all results connecting logic to categories are insular factoids. This paragraph is definitely controversial, but I truly do not understand how Category Theory or Topoi help us do understand logic better. Is there any hard logic conjecture that has been proven by using categories?

• One story I was told (I forget by whom) was that the hope is generally to go in the other direction: that categorical logic should let us apply techniques and concepts (if not literal results) from logic to categories of interest, e.g. use logic-y ideas + the internal logic of $\mathcal{C}$ to prove things about $\mathcal{C}$. Commented Mar 7 at 18:45
• For the record, the second paragraph ought to be preempted with "As far as I know". Commented Mar 9 at 13:47

There are plenty of applications of categorical logic to understanding of logic itself, including some which provide unexpected connections and insights. It is just not true that no real theory has been produced, as Makkai-Reyes book "First-order categorical logic" can testify. There are other examples of categories having clarified logic in the sense of having proven things in logic for which no other proofs are known. Since I am sure there are instances of which I am unaware of, in the following I will just cite my own work, leaving perhaps other answers to tell us about some other examples I might not know.

While it's definitely the case that categorical logic can provide new ways of understanding old results, it has also contributed to producing new results in pure logic.

One of them is a series of results on infinitary logic that were possible after a completeness theorem for $$\mathcal{L}_{\kappa^+, \kappa}$$ (see my paper "Infinitary generalizations of Deligne's completeness theorem"). Although Karp had completeness theorems for infinitary logics, the schemata she used were technically outside the fragment $$\mathcal{L}_{\kappa^+, \kappa}$$ since some of them allow $$\kappa$$ many free-variables to occur within them. It turns out that her results are a corollary of the "right" completeness theorem for the fragment with the right rule (transfinite transitivity rule) which is just a manifestation of an infinitary generalization of the transitivity rule for Grothendieck topologies. Had it not been for the topos-theoretic approach I would not have found the right schema to obtain completeness.

This completeness theorem has allowed to obtain an omitting types theorem for infinite quantifier languages, whenever the category of models has directed colimits. In the same way that omitting types theorem for finitary logic and even for $$\mathcal{L}_{\omega_1, \omega}$$ allow applications to, e.g., the theory of atomic and prime models, so the version for $$\mathcal{L}_{\kappa^+, \kappa}$$ has several applications in the model theory of infinitary logic beyond $$\mathcal{L}_{\omega_1, \omega}$$. And yet the proof of this omitting types theorem is topos-theoretic in nature, since the usual proofs of the previously known versions do not generalize, so that a new idea had to be used.

These new completeness theorems have also allowed new versions of Beth definability theorems for infinitary logics, in which the language of the explicit formula defining an implicitly definable predicate is found one level higher in the hierarchy of logics. These are obtained through topos-theoretic techniques, and in turn made possible the analysis of old model-theoretic conjectures (see my preprint "Preservation theorems for strong first-order logics"). I would not say it is a hard conjecture to prove once one has the right topos-theoretic tools, but the truth is that it has remained intractable for a long time when people tried to approach it using descriptive set-theoretic techniques.

Finally, I should also mention my work on both Shelah's eventual categoricity conjecture and Shelah's categoricity conjecture, as well as extensions of the conjecture to more general classes of structures. Although this work is still under review, the key insight that made possible such a topos-theoretic analysis of the conjectures and that has been independently verified is the observation that saturated models are linked to the double negation topology on a category of presheaves, the double negation subtopos being the $$\kappa$$-classifying topos whose $$\kappa$$-point is precisely the $$\kappa$$-saturated model of the theory. The whole strategy to proving eventual categoricity relies on this fact, which is topos-theoretic in nature. Furthermore, some instances of elimination of model-theoretic hypothesis such as amalgamation (which in this setting coincides with the right Ore condition for the category of models) are possible by considering instead the dense topology on the presheaves on that category (which is another presentation of the double negation topology).

• This is very interesting. I'm aware of the connections between topos theory and geometric logic, but do you have any recommendations for where to start learning about connections with other kinds of infinitary logic? Do you think one of your papers would be a good starting point? Commented Mar 9 at 19:21
• @JamesHanson My papers "Infinitary first-order categorical logic" and "Completeness of infinitary heterogeneous logic" started treating respectively the full infinitary fragment ($\mathcal{L}_{\kappa, \kappa}$, $\mathcal{L}_{\kappa^+, \kappa}$) and those fragments with the addition of game quantification. Smaller fragments, like the infinitary regular fragment (no disjunctions) appeared before in Makkai's "A theorem on Barr-exact categories, with an infinitary generalization". For the $\mathcal{L}_{\infty, \omega}$ fragment, in Johnstone/Butz's "Classifying toposes for first-order theories". Commented Mar 9 at 19:47

I hesitated a lot before writing this answer, because I feel that the current question ("Is there any hard logic conjecture that has been proven by using categories?") hinges on how one defines hard logic. Ideally, the question would have defined the term, or at least delineated it via some examples/non-examples of what count as "hard logic" conjectures.

In the end, I chose to bring my own definition, which may not sit well with everyone. But that's okay: everyone is welcome to share their definitions in their own responses.

In my interpretation, hard logic primarily concerns foundational theories, i.e. theories which can serve as a foundation for mathematics, but not questions about tame theories, the realm of classical model theory. E.g. looking at whether certain formal reasoning systems (like second-order propositional sequent calculi, forms of linear logic, dependent type theory, etc.) or foundational-strength axiomatic theories (e.g. HA, PA, CZF, IZF, various extensions, etc.) have key algorithmic and metatheoretical properties (ranging from consistency, not proving certain bad principles, existence properties, canonicity, projective existence, parametricity, etc.) would be considered hard logic; definitely outside the scope would be things like tame first-order theories (like ACF0, DCF0, the theory of the Farey graph, etc.) and tame properties (like quantifier elimination, stability, distality, o-minimality, etc.).

Resolving questions of interest in mathematics tends to require a combination of ad-hoc insights with general theory. A very simple example: one can prove consistency of PA in ZFC by producing a good old Tarskian model (reusable general theory), but actually producing this model requires constructing $$(\mathbb{N},+,\cdot)$$ and checking that it satisfies PA (a problem-specific insight).

Mathematics has managed to isolate some general, reusable theory about foundational systems, under broad umbrellas such as set theory and categorical logic. These are not entirely independent umbrellas, of course, e.g. the correspondence between forcing and categories of sheaves is widely known.

I wish to argue that for foundational-type questions, the general results of categorical logic are in fact fantastic reusable tools (even though, as always, ad-hoc insights and ideas are also required to solve difficult problems). And in response to your specific inquiry, categorical logic has indeed featured in solutions to important conjectures. Let me mention one recent example.

Normalization for cubical type theory is as "hard" as a logic question can get: it is literally an algorithmic question about a formal system of reasoning that can serve as a foundation for mathematics. First conjectured in 2016 and established by Sterling and Angiuli in 2021, the proof of normalization for cubical type theory relies essentially on Artin gluing, a major technique of categorical logic, done in the setting of locally Cartesian closed categories.

There are many more examples of course, hopefully to be mentioned in other answers by other people.

Now, when questioning the impact of categorical logic, it's not sufficient to be unimpressed by the standard results of the subject. One is free to argue that, even despite the contributions mentioned above, the general results of categorical logic are still somehow too shallow to count. Mayhap so. But it's crucial to confront the reality that the contributions are nonetheless unparalleled: bringing in a few key results from categorical logic does seem to help in many situations, and in those specific situations no other general body of results seems to help more, or even comparably.

Admittedly, not all logicians will find the sorts of questions mentioned above to be in alignment with their research interests (for example, if your main focus is stable theories, then you'll probably have better, more powerful alternatives to any tools that categorical logic might offer for the questions you care about). But a lot of logicians are interested specifically about questions of this type, and further interest is bolstered by continuous developments in logic-adjacent areas of computer science.

Finally, it's important to recognize not only the conjectures solved using tools from categorical logic, but also the applications that preempt potential conjectures entirely, i.e. the proactive use of categorical tools in recent research. For example, the system of this recent preprint would have been interesting enough by itself to become the subject of conjectures; fortunately, tools coming primarily from categorical logic allowed the authors to construct a model of the system and prove the theorems of interest about the theory right as it was introduced. This happens with much higher frequency in low-stakes environments: numerous "is X derivable in a weak foundational theory T" type questions have been rendered unnecessary in my own work and teaching when I could construct topos models to refute them outright. A lot of us have practical need for e.g. constructive semantics at least occasionally, and it would be a lot less pleasant if we don't know the basic result that topos models do exist, or that categories with enough structure have an internal logic. Likewise, we don't even need particularly deep results in categorical logic (like subtle existence theorems) to construct a model of, say, Synthetic Differential Geometry: nonetheless, I doubt they know whether it's consistent in the parallel universe in which categorical logic never came to exist.

• I feel like 'relies' is a slightly strong word for the result in our paper. It's not that hard to write down an ad hoc modification of the original definition of the realizability topos (or of the standard realizability model of IZF) to produce the counterexample. The tripos-to-topos construction is useful for providing a clean general account of the construction of a parameterized realizability topos from a parameterized partial combinatory algebra (a notion that we've developed in the paper). Commented Mar 9 at 17:20
• Grateful for your input, @JamesHanson. After rewatching Andrej's talk, and reflecting on your point, I decided to excise this example from my answer entirely, lest individuals sympathetic to DeadRingerAmbassador's viewpoint find in your comment some semblance of endorsement for their "all results connecting logic to categories are insular factoids" theory. Commented Mar 10 at 7:17