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.