Conceptual completeness for subgeometric logics

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.