Fragments of Geometric Logic

Geometric logic occupies a central place in categorical logic because of a fortunate confluence of features. It has substantial expressive power, encompassing many of the structures encountered in ordinary mathematical practice; its natural semantics is provided by Grothendieck topoi; and it supports an intrinsically intuitionistic treatment of those structures, making it suitable for semantic settings in which classical logic is not available. Moreover, its syntactic categories and classifying topoi provide a particularly robust bridge between syntax and semantics.

A number of important fragments of geometric logic have emerged over time. The best known is coherent logic, which may be regarded as a positive counterpart to classical first-order logic. Other examples include regular, disjunctive, and essentially algebraic logic. Each of these fragments comes with its own syntactic categories, completeness and representation theorems, classifying topoi, and characteristic preservation properties. These parallel theories suggest that the fragments belong to a common mathematical landscape. Nevertheless, the notion of a fragment of geometric logic has traditionally remained informal: more a recurring pattern than a general principle. Consequently, results of essentially the same form are often established separately, using arguments tailored to the particular fragment under consideration.

The purpose of this research programme is to make this underlying unity emerge naturally. Its first aim is to develop a general notion of fragment of geometric logic and a common categorical framework in which the familiar examples can be studied. Its second is to reorganise existing constructions and theorems so that their proofs depend modularly on the properties of the fragment, rather than having to be rebuilt in each case. Its third is to use this framework to obtain new results, extending phenomena such as conceptual completeness and Craig interpolation beyond the fragments for which they were originally proved. More broadly, the project seeks to clarify the geography of subgeometric logics and to provide tools for studying their similarities, differences, and interactions.