# Grothendieck toposes and logic

I am searching results in which one can extract logic information from a topological (Grothendieck topos) perspective (such as Gödel's Completeness Theorem and Deligne's Theorem ("theorem by P. Deligne about coherent topoi (coherent topoi have enough points) and how this theorem is equivalent to Gödel's completeness theorem for first order logic").

The ideal answer would be a result already contained in SGA IV (as Deligne theorem), a real scenario would be a Grothendieck topos theorem (conjecture) that extract an important aspect of logic.

Barr's classical result (that a Grothendieck topos admits a surjective morphism from the topos of sheaves on a Boolean algebra), besides helping in the proof of Deligne's theorem as mentioned in the link you provided, also has logical importance per se, since the topos of sheaves on a Boolean algebra is not only Boolean, but satisfies the axiom of choice (epis split). This immediately implies a conservativity result for geometric sequents derived from geometric hypothesis with the help of the law of excluded middle or even the axiom of choice: the use of these two can be eliminated.

Moreover, by a theorem of D. Higgs (1973) it follows that sheaves on a Boolean algebra is equivalent to a category in which models of a given theory are essentially the same thing as Boolean-valued models of that theory, hence providing the link with a Boolean-valued completeness theorem.

Another elegant result due to Joyal says that, if $\mathcal{C}oh(\mathcal{E})$ is the category of coherent functors from a coherent topos $\mathcal{E}$ to $\mathcal{S}et$, then the evaluation functor:

$$ev: \mathcal{E} \to \mathcal{S}et^{\mathcal{C}oh(\mathcal{E})}$$

is conservative and preserves universal quantification. This can be readily interpreted as Kripke completeness theorem for intuitionistic logic, where the presheaf topos is a conservative Kripke model. Indeed, by using Diaconescu's theorem (every Grothendieck topos admits an open surjective morphism from a localic one), one can replace the category $\mathcal{C}oh(\mathcal{E})$ by a posetal one, a forest (a collection of trees) for which the usual Kripke completeness theorem is formulated.

Deligne's theorem has in turn an infinitary generalization. In my paper Infinitary first-order categorical logic I introduce an infinitary generalization of coherent logic named $\kappa$-coherent logic and prove a set-valued completeness theorem when, e.g., $\kappa$ is a weakly compact cardinal. This is the core of the proof that every $\kappa$-coherent topos has enough $\kappa$-points (i.e., geometric morphisms where the inverse image preserves not only finite limits but $\kappa$-limits). Then, in the same way that Deligne's theorem is essentially Gödel's completeness theorem, this infinitary Deligne's theorem can be seen to correspond precisely to Karp's completeness theorem for infinitary classical logic.

Finally, my paper deals also with the infinitary version of Joyal's theorem, which similarly corresponds to a completeness theorem for infinitary intuitionistic logic in terms of an infinitary Kripke semantics.

• Could you indicate the good introduction in infinitary intuitionistic logic and infinitary intuitionistic modal logic. – Evgeny Kuznetsov Jun 10 '17 at 7:32
• The system for infinitary intuitionistic logic for $\mathcal{L}_{\kappa, \kappa}$, which is the one I mention in the answer (i.e., for infinite-quantifier languages), was introduced in my PhD thesis in 2016, so the only paper on that is the one I cited, which is still under review. A system for intuitionistic $\mathcal{L}_{\omega_1, \omega}$ is dealt with in Nadel's paper "Infinitary intuitionistic logic from a classical point of view". I'm not familiar with infinitary intuitionistic modal logic, but the papers on that I have seen only treat finite-quantifier languages. – godelian Jun 10 '17 at 10:36

You should look at First order categorical logic, Makkai and Reyes, specially Ch 6 (Existence theorems on geometric morphisms of topoi).