Craig Interpolation for Subgeometric Logics
Ivan Di Liberti, Lingyuan Ye
TL;DR
The paper develops a uniform Craig-interpolation framework for subfragments of geometric logic by marrying algebraic logic with categorical logic via doctrines on the 2-category $\mathsf{Lex}$. It defines interpolation for doctrines through cocommas in $\mathsf{alg}(\mathsf{T})$, and shows how slicing preservation reduces first-order interpolation to propositional substructure interpolation. A finitary, slicing-preserving doctrine has interpolation precisely when $t$-conservative maps are closed under cocommas, with localisations and filter quotients providing the structural tools. By connecting doctrines to logics through slicing and étale map classifiers, the authors prove that any finitary fragment between the regular and coherent logics possessing an étale classifier admits interpolation. The results generalize prior coherent-logic interpolation (Pitts) to a broad class of subfragments, offering a modular, categorial pathway to extend algebraic-logic interpolation results to predicate fragments and beyond.
Abstract
We show that a vast class of finitary fragments of geometric logic admit a form of Craig interpolation property. In doing so, we provide a new dictionary to import technology from algebraic logic to categorical logic.