Craig Interpolation for Subgeometric Logics

In 1957 Craig proved his interpolation theorem. Roughly speaking, it means if there is a deduction between two first-order formulas $\phi ⊢\psi$, then one can find an interpolant $\theta$, which belongs to the common language of $\phi ,\psi$, that $\phi ⊢\theta$ and $\theta ⊢\psi$. Since then, interpolation proved to be extremely influential in several areas of logic. Among the most prominent variations of Craig’s theorem, Pitts’ works [3, 4] delivered an algebraically flavoured version of Craig interpolation for first-order intuitionistic logic as well as coherent logic, from a categorical logic perspective. The definition of interpolation in categorical logic terms is a generalisation of the original interpolation in its syntactic form, and also of the one used in algebraic logic, which primarily applies to propositional fragments.

In our paper [1], we explore a cluster of fragments of geometric logic and assess to what extent these fragments admit a form of Craig interpolation theorem. The main difference of our approach is that, instead of trying to prove interpolation for specific fragment of logic, we establish uniformly a Craig-interpolation-type theorem for a wide class of subfragments of geometric logic.

In our investigation, we have identified a property of logic that plays a key role in establishing interpolation results. In the language of doctrine (a.k.a lax-idempotent monads on $\mathrm{𝖫𝖾𝗑}$), the property states that it should preserve slicing. This implies the 2-category of algebras are closed under taking slices, which is indeed such a fundamental property of doctrines associated with logic and type theory that perhaps has not been paid enough attention to in the literature. We provide a classification of the interpolation property for doctrines preserving slicing as an exactness property. In particular, we introduce a notion of t-conservative maps of lex categories, and show that it belongs to an orthogonal factorisation system for any finitary doctrine on $\mathrm{𝖫𝖾𝗑}$. Using this, we are able to provide a classification as below:

For a working notion of fragment of geometric logic, we follow the authors’ previous work [2]. From loc. cit. every logic $\mathscr{H}$ induces a doctrine ${𝖳}^{\mathscr{H}}$, and the existence of an étale map classifier for the logic $\mathscr{H}$ is tightly connected to the associated doctrine ${𝖳}^{\mathscr{H}}$ preserving slicing:

Using the techniques presented in [2], especially the classifying topos construction for $\mathscr{H}$, we are able to obtain our main theorem: