• logic
• topos theory
• model theory
• geometric morphism
• classifying topoi

Topoi originated in the 1960's when Grothendieck found a powerful way to study categories related to algebraic geometry; in its idea every topological space gives a topos, namely the category of sheaves on the space. These are now known as ``Grothendieck topoi'' and constitute a particular case of ``elementary topoi'', introduced by Lawvere and Tierney in 1968-69.

The biggest problem of Grothendieck topoi, in Lawvere idea, was their extremely complex constructs; thus he tried to describe the most relevant aspect of topoi in a much more simple way. Essentially, a topos is a category with a terminal object, all finite products, exponential objects and a subobject classifier.

The few properties defining a topos permit us to work with (first and higher order) logic and, in particular, model theory. Given a language L, we define the notion of L-structure in a topos simply miming the usual construction in Sets. Moreover, we can define the interpretation of a formula as a particular subobject of the topos (here we follow ``Sketches of an Elephant''). This allows us to say when a formula is true (i.e. the top element in the Heyting algebra of subobjects) or false (i.e. the bottom element); thus we can introduce the notion of model for a given theory T and hence build the category of T-models in a topos E (with a suitable notion of homomorphism).

In this context, a question arises: which formulas are ``preserved'' by morphism between topoi? Or even: are there some kind of theories whose models are ``preserved'' by geometric morphisms?
First we need to clarify what we mean by preservation; we say that a formula is strongly preserved if for each geometric morphism f and each structure in a topos, the subobjects identified by the formula coincides under the inverse image of f.

A class of strongly preserved first-order formulas is easily identified; it is the smallest containing atomic formulas and closed for conjunction, disjunction and existential quantification; these are known as geometric formulas. Following Blass' paper ``Fixed Point Preservation'', we can consider a new construction and prove that the class of strongly preserved formulas goes beyond first-order. We call the elements of this class EFPL-formulas. As a consequence, we are able to prove the following:

Theorem: Let T be a theory whose axioms are sequents of EFPL-formulas; then for each geometric morphism f, its inverse image induces a functor between the categories of T-models.

Finally, we talk about classifying topoi for theories; initially we get a result for Grothendieck topoi and geometric theories:

Theorem: Let T be a geometric theory; then there exists a Grothendieck topos which classifies T-models.

To talk about classifying topoi for EFPL theories we need a difference approach: the equivalence we want to prove will be no more for Grothendieck topoi, but for elementary ones over a base topos. The only weaker hypothesis we must subsume are some requests of finiteness and the existence of a natural number object in the base topos (i.e. a model of natural numbers):

Theorem: Let L be a first-order language with a finite number of dorts and symbols, T be a finite theory whose axioms are sequents of strongly preserved formulas and E be a topos with a natural number object. Then T has a classifying topos over E.

To conclude, as shown in ``Classifying topoi and the axiom of infinity'', we prove that the request of a natural number object in the last theorem is necessary.