Conceptual completeness for subgeometric logics
2026-07-02 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a specific part of geometric logic and redefine 'conceptual completeness' not just as rebuilding logic from meanings, but as a special relationship between logical theories and mathematical structures called topoi. They prove that these complete fragments fit neatly inside the full version of geometric logic, giving new insights into how proofs work. They also provide new proofs showing that various types of logic, like coherent and regular logic, have this property. Finally, they connect their new idea back to a classic result, showing it matches when looking at standard mathematical models.
geometric logicconceptual completenesstopos theorycoherent logicregular logicultracategoriesconservative embeddingsemantic reconstructionproof theoryset-based models
Authors
Ivan Di Liberti, Umberto Tarantino, Lingyuan Ye
Abstract
We explore the notion of conceptual completeness for a fragment of geometric logic in the framework developed by the first and third author. Unlike its traditional interpretation as a reconstruction of syntax from semantics, in this paper we characterise conceptual completeness of a fixed fragment in terms of a duality between theories and topoi. We then show that conceptually complete fragments are conservatively embedded in full geometric logic, thus casting conceptual completeness in a new proof-theoretic light. We give a new proof of conceptual completeness for coherent logic, and we also show that regular, disjunctive, and essentially algebraic logic with falsum are conceptually complete. Finally, we show that our notion is equivalent to a traditional reconstruction result under the assumption of completeness with respect to set-based models: in the coherent case, we thus recover Makkai's original reconstruction theorem via ultracategories.