Classifying toposes for first-order theories (Q1382183): Difference between revisions

We say that a (Grothendieck) topos \(\mathcal E\) is a classifying topos for an infinitary first-order theory \(\mathbf T\) if, for any topos \(\mathcal F\), there is an equivalence between the category of \(\mathbf T\)-models in \(\mathcal F\) and the category of open geometric morphisms \({\mathcal F}\to{\mathcal E}\), which is `natural in \(\mathcal F\)' in an appropriate sense. In this paper we characterize the first-order theories which have classifying toposes, as those for which the Lindenbaum algebra of provable-equivalence classes of \({\mathcal L}_{\infty\omega}\) formulae in any context is small; we also show that every Grothendieck topos occurs as a classifying topos in this sense, and that every geometric theory has a canonical geometrically-conservative extension to a first-order theory with this smallness property. We give an explicit presentation of this extension for a couple of simple theories; but we also show, using a result of D. de Jongh, that `most' familiar first-order theories do not satisfy the smallness condition.