# Compactness theorem and topos theory

The theory of classifying topoi due to Makkai, Reyes, Hakim, and Grothendieck supplies a bijection between geometric theories (up to Morita equivalence) and Grothendieck topoi, by assigning to each geometric theory $$\mathbb T$$ the unique Grothendieck topos $$\mathcal E$$ such that $$\hom(\mathcal F, \mathcal E)\cong \text{models of \mathbb T in \mathcal F}$$ natural in $$\mathcal F$$. In particular, the points of the Grothendieck topos associated to $$\mathbb T$$ are precisely the models of $$\mathbb T$$ in the category of sets.

This correspondence identifies Deligne's theorem (SGA4, Exposé VI, Section 9), which gives a sufficient condition for a topos to have points, with Gödel's completeness theorem from mathematical logic. A great explanation of that phenomenon has been given by Torsten Ekedahl (MO/68335).

Question: Another fundamental theorem from mathematical logic is the compactness theorem. Can the compactness theorem be phrased as a statement about Grothendieck topoi, similar to how Gödel's completeness theorem can be phrased as a statement about Grothendieck topoi?

• I have absolutely no competence in category theory, but I wolud start from the reasons in logic to say that compactness and completeness are equivalent, and then translate them in topos language. Jan 12, 2022 at 15:09
• Compactness is included in the coherence requirement of Deligne's Theorem. Or did you have something else in mind? Jan 12, 2022 at 18:24
• Anyway, there is a "semantic" formulation of compactness for propositional logic that amounts to saying that a certain topological space – you could call it the classifying space if you like – is compact / has the finite intersection property. Coherency is one of the analogues of compactness for Grothendieck toposes (there are others!) so if you want to extend the analogy you would be looking for a theorem that tells you classifying toposes for certain theories are coherent. But as François points out, Deligne's theorem is about coherent topos, so this is already implicitly in the analogy. Jan 12, 2022 at 23:06
• Morleyisation is a non-trivial transformation! Here is what I would consider a categorical logic formulation of Gödel's completeness theorem: given a consistent first-order theory, there is a Heyting functor from the syntactic category of the theory to the category of sets. If I recall correctly there is a topos-theoretic formulation involving open geometric morphisms. Jan 13, 2022 at 13:24
• Since Gödel's completeness is about classical logic, one should ask the functor to be Boolean (in particular Heyting). Such a Boolean functor corresponds indeed to a geometric morphism from the classifying topos of the Morleyized theory. The formulation with open geometric morphisms is for first-order intuitionistic theories, and they do not always exist (the theory needs to be locally small). Jan 13, 2022 at 14:25

The localic coherent toposes are those toposes of the form $$\mathbf{Sh}(X)$$ for $$X$$ a spectral space. Take a coherent theory with $$\mathbf{Sh}(X)$$ as classifying topos. Adding axioms changes the classifying topos, more precisely the new classifying topos is a subtopos $$\mathbf{Sh}(Y) \subseteq \mathbf{Sh}(X)$$ corresponding to a sublocale $$Y \subseteq X$$. If you added only finitary/coherent axioms, then $$\mathbf{Sh}(Y) \subseteq \mathbf{Sh}(X)$$ is a coherent subtopos, and these correspond precisely to the subsets $$Y \subseteq X$$ that are closed sets for the "patch topology".
So adding a sequence of coherent axioms corresponds to a chain of closed sets $$X \supseteq Y_1 \supseteq Y_2 \supseteq Y_3 \supseteq \dots$$ for the patch topology. The compactness theorem can then be seen as the statement: $$\forall i \in I,~ Y_i \neq \varnothing ~\Rightarrow~ \bigcap_{i \in \mathbb{N}} Y_i \neq \varnothing$$ This statement follows from the fact that $$X$$ is compact for the patch topology (by looking at the complements of these closed sets).
So an analogue of the compactness theorem for toposes would be: if $$\mathcal{E}$$ is a coherent topos, and $$\mathcal{E} \supseteq \mathcal{E}_1 \supseteq \mathcal{E}_2 \supseteq \mathcal{E}_3 \supseteq \dots$$ is a sequence of non-empty coherent subtoposes, then the intersection is again non-empty coherent. I don't know a proof of this in the non-localic case.