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.