Classifying Topoi and Model Theory

Abstract

Every geometric theory has a classifying topos, but when trying to extend this to full first-order theories one may run into trouble. Such a first-order classifying topos for a first-order theory T, is a topos F such that for every topos E, the models of T in E correspond to open geometric morphisms from E to F. The trouble is that not every first-order theory may have such a first-order classifying topos, as was pointed out by Carsten Butz and Peter Johnstone in 1998. They characterized which theories do admit such a first-order classifying topos, and show how to construct such a first-order classifying topos.

The work of Butz and Johnstone is the main subject of this thesis. The construction of a classifying topos for both geometric theories and first-order theories is worked out in detail. We will also study the characterization of which theories admit a first-order classifying topos. In doing so, we obtain certain completeness results that are interesting in their own right. These are completeness results for deduction-systems for various kinds of infinitary logic, with respect to models in topoi. Building on top of those results, we also obtain a completeness result for classical infinitary logic, with respect to Boolean topoi.

One of the first goals of this thesis was to form a link between Topos Theory and Model Theory, via the first-order classifying topos. In order to bridge the gap between the intuitionistic logic of topoi and the classical logic of Model Theory, we introduce the concept of a Boolean classifying topos. We provide a characterization of which first-order theories admit such a Boolean classifying topos, much like the one for first-order classifying topoi. Then we give a simple example of how to link Boolean classifying topoi to Model Theory, by characterizing complete theories in terms of their Boolean classifying topos.