nLab conceptual completeness

Idea

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

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

2. strong conceptual completeness, instead, corresponds to the isomorphism $B \cong \mathbf{StoneSp}(X_B, 2)$ for each Boolean algebra $B$, expressing how the Stone topology on the set $X_B$ of models of $B$ allows to reconstruct $B$ up to isomorphism, or in other words to the fully-faithfulness of the functor $\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 $\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 ${\mathbf{Pretop}}(-,{Set}) : \mathbf{Pretop}^{op} \to \mathbf{CAT}$, for the 2-category $\mathbf{Pretop}$ of (small) pretoposes, reflects equivalences.

Theorem

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

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

is an equivalence of categories, then so is $F$.

Recall indeed that pretoposes can be identified with (syntactic categories of) coherent theories up to elimination of imaginaries, so that a pretopos morphism $P_1 \to P_2$ corresponds to an interpretation of the theory $P_1$ into the theory $P_2$, or equivalently to a model of the theory $P_1$ inside the category $P_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_1 \to T_2$ between two coherent theories induces an equivalence $\operatorname{Mod}(T_2) \to \operatorname{Mod}(T_1)$ between the categories of models, then $T_1$ and $T_2$ are bi-interpretable up to elimination of imaginaries, that is, $T_1^{eq}$ and $T_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 \colon P \to C$ is a coherent functor from a pretopos $P$ to a coherent category $C$ such that $F^* \colon \operatorname{Mod}(C) \to \operatorname{Mod}(P)$ is an equivalence of categories, then $F$ is an equivalence itself. Call now a coherent functor $C \to C'$ an extension of $C$. An extension $I \colon C \to C'$ of a coherent category $C$ is:

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

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

We then say that a coherent category $C$ is conceptually complete if every tight extension of $C$ 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 $\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 $\mathbf{Pretop}$ and let $r \in R$. Consider subobjects $s \rightarrowtail I(r)$ in $S$ and $t \rightarrowtail J(r)$ in $T$ such that $\exists_{h_r} ( M(s) ) \leq N(t)$ as subobjects of $NJ(r)$. Then, there exists a subobject $r' \rightarrowtail r$ in $R$ such that $s \leq I(r')$ as subobjects of $I(r)$ and $J(r') \leq t$ as subobjects of $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 $\operatorname{Mod}(P)= \mathbf{Pretop}(P, Set)$ of a (small) pretopos $P$ can be endowed with the structure of an ultracategory by considering the usual notion of ultraproducts of models; this way, the pretopos $P$ can be reconstructed up to equivalence by considering ultrafunctors $\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 $P$, the evaluation functor

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

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

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

Remark

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

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 $T$. 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.

Related concepts

• ultraproduct
• Makkai duality
• Stone duality

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^{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]

• Ivan Di Liberti, Towards Higher Topology [arXiv:2009.14145].

For continuous logic:

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

For $\mathcal{L}_{\omega_1,\omega}$:

• Ruiyuan Chen, Borel functors, interpretations, and strong conceptual completeness for $\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

• Spencer Breiner, Scheme representation for first-order logic, [arXiv:1402.2600] .

For the $(\infty, 1)$-analog of conceptual completeness, see section A.9 of

• Jacob Lurie, Spectral Algebraic Geometry