nLab conceptual completeness

Contents

Contents

Idea

Broadly speaking, conceptual completeness for a logical doctrine refers to the following statement: if an interpretation T 1T 2T_1 \to T_2 between two theories of the doctrine induces an equivalence Mod(T 2)Mod(T 1)\operatorname{Mod}(T_2) \to \operatorname{Mod}(T_1) 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 2{2} as a dualizing object and recall that we can identify Boolean algebras with Lindenbaum-Tarski algebras of classical propositional theories. Denote by X BX_B the dual space of a Boolean algebra BB, whose points are then models of BB, i.e. homomorphisms of Boolean algebra B2B \to {2}. In this context:

  1. conceptual completeness amounts to the fact that, for a homomorphism of Boolean algebras f:BBf \colon B \to B', if its dual map f *:X BX Bf^* \colon X_{B'} \to X_{B} is a homeomorphism, then ff is an isomorphism itself;

  2. strong conceptual completeness, instead, corresponds to the isomorphism BStoneSp(X B,2)B \cong \mathbf{StoneSp}(X_B, 2) for each Boolean algebra BB, expressing how the Stone topology on the set X BX_B of models of BB allows to reconstruct BB up to isomorphism, or in other words to the fully-faithfulness of the functor BoolAlg(,2):BoolAlg opStoneSp\mathbf{BoolAlg}(-,2) \colon \mathbf{BoolAlg}^{op} \to \mathbf{StoneSp}.

Remark

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 \mathcal{E} \to \mathcal{F} between toposes (even with enough points) inducing an equivalence of categories Mod()Mod()\operatorname{Mod}(\mathcal{E}) \to \operatorname{Mod}(\mathcal{F}) is an equivalence itself.

Conceptual completeness for coherent logic

In the case of coherent logic, conceptual completeness refers to the result of Makkai and Reyes ‘77 that the hom-2-functor Pretop(,Set):Pretop opCAT{\mathbf{Pretop}}(-,{Set}) : \mathbf{Pretop}^{op} \to \mathbf{CAT}, for the 2-category Pretop\mathbf{Pretop} of (small) pretoposes, reflects equivalences.

Theorem

(Conceptual completeness for pretoposes) Let F:P 1P 2F : P_1 \to P_2 be a pretopos morphism between small pretoposes. If the precomposition functor

F *:Pretop(P 2,Set)Pretop(P 1,Set) F^* : {\mathbf{Pretop}}(P_2, {Set}) \to {\mathbf{Pretop}}(P_1,{Set})

is an equivalence of categories, then so is FF.

Recall indeed that pretoposes can be identified with (syntactic categories of) coherent theories up to elimination of imaginaries, so that a pretopos morphism P 1P 2P_1 \to P_2 corresponds to an interpretation of the theory P 1P_1 into the theory P 2P_2, or equivalently to a model of the theory P 1P_1 inside the category P 2P_2; 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 T 1T 2T_1 \to T_2 between two coherent theories induces an equivalence Mod(T 2)Mod(T 1)\operatorname{Mod}(T_2) \to \operatorname{Mod}(T_1) between the categories of models, then T 1T_1 and T 2T_2 are bi-interpretable up to elimination of imaginaries, that is, T 1 eqT_1^{eq} and T 2 eqT_2^{eq} are bi-interpretable.

Remark

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 F:PCF \colon P \to C is a coherent functor from a pretopos PP to a coherent category CC such that F *:Mod(C)Mod(P)F^* \colon \operatorname{Mod}(C) \to \operatorname{Mod}(P) is an equivalence of categories, then FF is an equivalence itself. Call now a coherent functor CCC \to C' an extension of CC. An extension I:CCI \colon C \to C' of a coherent category CC is:

  1. tight (or strongly conservative in Makkai and Reyes) if I *:Mod(C)Mod(C)I^* \colon \operatorname{Mod}(C') \to \operatorname{Mod}(C) is an equivalence of categories;

  2. significant if I:CCI \colon C \to C' is not an equivalence of categories.

We then say that a coherent category CC is conceptually complete if every tight extension of CC 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 Pretop\mathbf{Pretop}, which he employed in Pitts ‘89 to prove a conceptual completeness theorem for intuitionistic first-order logic by considering Heyting pretoposes.

Theorem

(Pitts’ interpolation theorem for pretoposes)

Consider a cocomma square in Pretop\mathbf{Pretop} and let rRr \in R. Consider subobjects sI(r)s \rightarrowtail I(r) in SS and tJ(r)t \rightarrowtail J(r) in TT such that h r(M(s))N(t)\exists_{h_r} ( M(s) ) \leq N(t) as subobjects of NJ(r)NJ(r). Then, there exists a subobject rrr' \rightarrowtail r in RR such that sI(r)s \leq I(r') as subobjects of I(r)I(r) and J(r)tJ(r') \leq t as subobjects of J(r)J(r).

Strong conceptual completeness for coherent logic

Ultracategories, introduced by Makkai ‘87, allow to improve Theorem to a strong conceptual completeness theorem for coherent logic. Intuitively, the category of models Mod(P)=Pretop(P,Set)\operatorname{Mod}(P)= \mathbf{Pretop}(P, Set) of a (small) pretopos PP can be endowed with the structure of an ultracategory by considering the usual notion of ultraproducts of models; this way, the pretopos PP can be reconstructed up to equivalence by considering ultrafunctors Mod(P)Set\operatorname{Mod}(P) \to Set, that is, functors which preserve ultraproducts in a suitable sense.

Theorem

(Strong conceptual completeness for pretoposes)

For every small pretopos PP, the evaluation functor

ev:PUlt(Mod(P),Set) ev \colon P \to \mathbf{Ult}\big( \operatorname{Mod}(P) , Set \big)

is an equivalence of categories, where Ult\mathbf{Ult} is the 2-category of ultracategories, ultrafunctors, and transformations thereof.

In other words, SetSet is a dualizing object for a dual 2-adjunction, known as Makkai duality: The counit of this 2-adjunction, at a pretopos PP, is given by the equivalence ev:PUlt(Mod(P),Set)ev \colon P \to \mathbf{Ult}\big( \operatorname{Mod}(P) , Set \big) , thus making the hom-2-functor Pretop(,Set):Pretop opUlt{\mathbf{Pretop}}(-,{Set}) : \mathbf{Pretop}^{op} \to \mathbf{Ult} a 2-fully-faithful embedding.

Remark

More precisely, as SetSet is not a small pretopos, the previous 2-adjunction should be considered between Ult\mathbf{Ult} and PRETOP\mathbf{PRETOP}, 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 ev:PUlt(Mod(P),Set)ev : P \to \mathbf{Ult} ( \operatorname{Mod}(P), Set ) is an equivalence for each small pretopos PP.

Remarks

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 TT. 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.

References

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. T eqT^{eq}), 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:

  • Jean-Martin Albert, Bradd Hart. Metric logical categories and conceptual completeness for first order continuous logic, [arXiv:1607.03068] .

For ω 1,ω\mathcal{L}_{\omega_1,\omega}:

  • Ruiyuan Chen, Borel functors, interpretations, and strong conceptual completeness for ω 1,ω\mathcal{L}_{\omega_1,\omega}, Trans. Am. Math. Soc., 372 (2019) pp. 8955-8983 .

An approach which reframes conceptual completeness in terms of logical schemes is adopted in section 4.4 of

For the (,1)(\infty, 1)-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.