nLab conceptual completeness




In any context it is interesting to ask when a contravariant hom-functor Hom(,X)\operatorname{Hom}(-,X) reflects isomorphisms, i.e. if homming into an object is enough to distinguish isomorphism classes. In a 22-categorical setting, the analogous question is if homming into an object reflects equivalences.


Conceptual completeness refers to the result of Makkai and Reyes that in the 22-category Pretop\mathbf{Pretop} of pretoposes, homming into the pretopos Set Hom Pretop(,Set):PretopCat\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) : \mathbf{Pretop} \to \mathbf{Cat} reflects equivalences.

That is, if f:T 1T 2f : T_1 \to T_2 is a pretopos morphism and f:Hom Pretop(T 2,Set)Hom Pretop(T 1,Set)- \circ f : \operatorname{Hom}_{\mathbf{Pretop}}(T_2, \mathbf{Set}) \to \operatorname{Hom}_{\mathbf{Pretop}}(T_1,\mathbf{Set}) is an equivalence, then ff was also. Pretopos morphisms are just interpretations of theories; a pretopos morphism into Set is an interpretion of the source theory into the internal logic of Set, and is therefore a model.

Since pretoposes are just effectivizations of syntactic categories of first-order theories, this means: if a functor between the categories of models of T 1T_1 and T 2T_2 is an equivalence and is induced by an interpretation T 1T 2T_1 \to T_2, then that interpretation must be part of a bi-interpretation, i.e. T 1T_1 and T 2T_2 are equivalent as syntactic categories via pretopos morphisms.

Makkai duality states that Hom Pretop(,X)\operatorname{Hom}_{\mathbf{Pretop}}(-,X) factors through the 22-category of ultracategories (categories equipped with ultraproduct functors?) (which also contains Set\mathbf{Set}) and that Hom Pretop(,Set)\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) is left-adjoint to Hom Ult(,Set)\mathbf{Hom}_{\mathbf{Ult}}(-,\mathbf{Set}).

Furthermore, the unit of this adjunction is an equivalence, so that a pretopos TT is equivalent to the category of ultrafunctors (ultraproduct-preserving functors) from Mod(T)\mathbf{Mod}(T) to Set\mathbf{Set}, i.e. any ultrafunctor Mod(T)Set\mathbf{Mod}(T) \to \mathbf{Set} is induced by taking points in models of some definable set XTX \in T.

This means: when viewed as a functor to the 22-category of ultracategories instead, Hom Pretop(,Set)\operatorname{Hom}_{\mathbf{Pretop}}(-,\mathbf{Set}) creates equivalences also, so that the pretopos/theory TT can be reconstructed up to bi-interpretability from its ultracategory of models. This is what is known as strong conceptual completeness.


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


(Maybe I’ll add some explicit computations later.)


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 January 8, 2019 at 13:52:52. See the history of this page for a list of all contributions to it.