indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
Broadly speaking, conceptual completeness for a logical doctrine refers to the following statement: if an interpretation between two theories of the doctrine induces an equivalence between the categories of models, then the two theories are bi-interpretable. Strong conceptual completeness, instead, refers to the possibility of reconstructing a theory of the doctrine from an appropriate structure formed by the models of the theory.
To make this idea more formal, consider Stone duality for Boolean algebras, that is, the dual equivalence between Boolean algebras and Stone spaces realized by as a dualizing object and recall that we can identify Boolean algebras with Lindenbaum-Tarski algebras of classical propositional theories. Denote by the dual space of a Boolean algebra , whose points are then models of , i.e. homomorphisms of Boolean algebra . In this context:
conceptual completeness amounts to the fact that, for a homomorphism of Boolean algebras , if its dual map is a homeomorphism, then is an isomorphism itself;
strong conceptual completeness, instead, corresponds to the isomorphism for each Boolean algebra , expressing how the Stone topology on the set of models of allows to reconstruct up to isomorphism, or in other words to the fully-faithfulness of the functor .
In these terms, it’s not always true that strong conceptual completeness, for a logical doctrine, entails conceptual completeness: for example, virtual ultracategories allow for a strong conceptual completeness theorem for geometric logic, but the latter does not enjoy conceptual completeness. More precisely, it’s not true that a geometric morphism between toposes (even with enough points) inducing an equivalence of categories is an equivalence itself.
In the case of coherent logic, conceptual completeness refers to the result of Makkai and Reyes ‘77 that the hom-2-functor , for the 2-category of (small) pretoposes, reflects equivalences.
(Conceptual completeness for pretoposes) Let be a pretopos morphism between small pretoposes. If the precomposition functor
is an equivalence of categories, then so is .
Recall indeed that pretoposes can be identified with (syntactic categories of) coherent theories up to elimination of imaginaries, so that a pretopos morphism corresponds to an interpretation of the theory into the theory , or equivalently to a model of the theory inside the category ; in particular, a pretopos morphism into Set is therefore a model of the source theory. In these terms, conceptual completeness states that if an interpretation between two coherent theories induces an equivalence between the categories of models, then and are bi-interpretable up to elimination of imaginaries, that is, and are bi-interpretable.
The above theorem can also be interpreted as a “semantic” characterization of pretoposes among coherent categories, instead of their “syntactic” characterization as (syntactic categories of) coherent theories admitting elimination of imaginaries. First note that, as stated in Theorem 7.1.8, Makkai and Reyes ‘77, the theorem above holds also if the target category is merely a coherent category: that is, if is a coherent functor from a pretopos to a coherent category such that is an equivalence of categories, then is an equivalence itself. Call now a coherent functor an extension of . An extension of a coherent category is:
tight (or strongly conservative in Makkai and Reyes) if is an equivalence of categories;
significant if is not an equivalence of categories.
We then say that a coherent category is conceptually complete if every tight extension of is not significant. As the embedding of a coherent category into its pretopos completion is a tight extension, conceptually complete categories are pretoposes; conversely, the conceptual completeness theorem can be rephrased by saying that pretoposes are conceptually complete, thus characterizing pretoposes as the conceptually complete (coherent) categories. Intuitively, this corresponds to the fact that pretoposes admit all the coherently-definable structure that coherent categories may lack but which coherent functors automatically preserve: that is, finite (disjunct) coproducts and quotients of definable equivalence relations.
The conceptual completeness theorem is proved in Makkai and Reyes ‘77 via model-theoretical techniques, such as the compactness theorem, and “syntactical” arguments, exploiting the identification between coherent categories and coherent theories. In Pitts ‘86, Pitts provided a new, constructive, and purely categorical proof rephrasing the theorem in terms of an interpolation property for cocomma squares in , which he employed in Pitts ‘89 to prove a conceptual completeness theorem for intuitionistic first-order logic by considering Heyting pretoposes.
(Pitts’ interpolation theorem for pretoposes)
Consider a cocomma square in and let . Consider subobjects in and in such that as subobjects of . Then, there exists a subobject in such that as subobjects of and as subobjects of .
Ultracategories, introduced by Makkai ‘87, allow to improve Theorem to a strong conceptual completeness theorem for coherent logic. Intuitively, the category of models of a (small) pretopos can be endowed with the structure of an ultracategory by considering the usual notion of ultraproducts of models; this way, the pretopos can be reconstructed up to equivalence by considering ultrafunctors , that is, functors which preserve ultraproducts in a suitable sense.
(Strong conceptual completeness for pretoposes)
For every small pretopos , the evaluation functor
is an equivalence of categories, where is the 2-category of ultracategories, ultrafunctors, and transformations thereof.
In other words, is a dualizing object for a dual 2-adjunction, known as Makkai duality: The counit of this 2-adjunction, at a pretopos , is given by the equivalence , thus making the hom-2-functor a 2-fully-faithful embedding.
More precisely, as is not a small pretopos, the previous 2-adjunction should be considered between and , the 2-category of (potentially not small) pretoposes. As expressed in Theorem 8.2, Makkai, this 2-adjunction is then a reflection in the small, meaning that the counit is an equivalence for each small pretopos .
In his AMS monograph on duality and definability in first-order logic, Makkai refined the above reconstruction result to work with just the (ultra) core of the ultracategory of models of . Awodey and his students replaced the ultracategory structure on this groupoid with a related topology instead; this is the “spectral groupoid” which forms the basis of the logical scheme approach.
For coherent logic:
Michael Makkai and Gonzalo Reyes, First order categorical logic: Model-theoretical methods in the theory of topoi and related categories, Springer-Verlag, 1977 ;
Mihaly Makkai, Stone duality for first-order logic, Adv. Math. 65 2 (1987) 97–170 [doi:10.1016/0001-8708(87)90020-X, MR89h:03067]
Andrew Pitts, Interpolation and Conceptual Completeness for Pretoposes via Category Theory, Mathematical Logic and Theoretical Computer Science, 106 (1987), pp. 301-327 ;
Peter Johnstone, Sketches of an Elephant vol. II , Oxford UP 2002 (sec. D3.5, pp.931-939) ;
Victor Harnik, Model theory vs. categorical logic: two approaches to pretopos completion (a.k.a. ), in: Models, logics, and higher-dimensional categories, 79–106 (Makkai volume), CRM Proc. Lecture Notes 53, Amer. Math. Soc. 2011; gBooks ;
Jacob Lurie, Ultracategories, (pdf) .
For first-order logic:
Michael Makkai, Strong Conceptual Completeness for First-Order Logic , APAL 40 (1988) pp.167-215 (freely available online) ;
Andrew Pitts, Conceptual completeness for first-order Intuitionistic logic: an application of categorical logic, APAL, 41 (1987), pp. 38-81.
For geometric logic:
Gabriel Saadia, Extending conceptual completeness via virtual ultracategories [arXiv:2506.23935] ;
Ali Hamad, Generalised ultracategories and conceptual completeness of geometric logic [arXiv:2507.07922] .
For continuous logic:
For :
An approach which reframes conceptual completeness in terms of logical schemes is adopted in section 4.4 of
For the -analog of conceptual completeness, see section A.9 of
Last revised on July 31, 2025 at 14:09:31. See the history of this page for a list of all contributions to it.