ABSTRACT

We develop a duality theory for small Boolean pretoposes in which the dual of T is the

groupoid of models of a Boolean pretopos T equipped with additional structure derived from

ultraproducts. The duality theorem says that any small Boolean pretopos is canonically

equivalent to its double dual. We use a strong version of the duality theorem to prove the

so-called descent theorem for Boolean pretoposes which says that category of descent data

derived from a conservative pretopos morphism between Boolean pretoposes is canonically

equivalent to the domain-pretopos. The descent theorem contains the Beth definability theorem

for classical first order logic. Moreover, it gives, via the standard translation from the language

of categories to symbolic logic, a new definability theorem for classical first order logic

concerning set-valued functors on models, expressible in purely syntactical (arithmetical) terms .

Key words and phrases: pretopos, first order logic, duality theory, definability theory,

ultraproduct, category of models, descent theory, 2-category, exactness property.

VI