Ivan di Liberti: Craig interpolation for fragments of geometric logic

We provide a definition of a fragment of geometric logic H, this is a collection of semantic prescriptions that we expect categories of models to enjoy.

Our notion includes many known fragments: regular, coherent, essentially algebraic, disjunctive.

Each fragment induces a lax-idempotent “monad of H-symbols” over Lex, the 2-category of categories with finite limits. We say that a fragment is finitary when its associated monad of symbols is finitary. All the fragments we listed above are finitary in this sense.

We show that a vast class of finitary fragments of geometric logic enjoy Craig interpolation. Our discussion offers many insights on the structure of fragments, bridging usual techniques from topos theory to many ideas coming from algebraic logic. We also simplify Pitts’ proof that coherent logic has Craig interpolation to a much more elementary topos theoretic argument.

Time permitting we will mention some work in progress concerning Lindström theorem for fragments of geometric logic.