Logic vs doctrines, a mirror symmetry

Abstract

This paper studies doctrines in categorical logic and their relations to fragments of geometric logic. After a brief account of the historical context for the notion of doctrine in categorical logic, we propose our working definition. We then show that there is a Galois connection between the poset of doctrines and the poset of fragments of geometric logic as defined in the framework of Kan injectivity in the 2-category of topoi, recently developed by the first and third authors. Concretely, the connection is realised by a general construction of syntactic categories and classifying topoi which encompasses all well-known examples in categorical logic. This yields a mirror symmetry, between the algebraic world of doctrines and the geometric world of topoi: to provide evidence of this phenomenon, we prove a few symmetric results relating doctrines and logics by means of syntactic categories and classifying topoi. We conclude with a discussion on the theme of conceptual completeness.