Categorical logic reveals symmetry between logic and geometry
Logic vs doctrines, a mirror symmetry
Logic in Computer Science
Summary
This paper explores a deep connection between two ways of thinking in mathematics: logical rules and geometric structures. The authors study a concept called doctrines, which organize logical systems, and show how these doctrines mirror fragments of geometric logic. They find a precise mathematical relationship, called a Galois connection, linking these logical and geometric worlds. This symmetry helps unify understanding of logic and geometry, and the authors provide examples to illustrate their findings.
What this means in practice
- •For logic system designers: Use the Galois connection framework to design logical systems with clear geometric interpretations.
- •For formal methods engineers: Apply the symmetry between doctrines and topoi to structure and verify specification languages in software correctness tools.
A theory result. No direct application yet.
Authors
Ivan Di Liberti, Umberto Tarantino, Lingyuan Ye
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.