Duality and Definability in First Order Logic

Book excerpt: We develop a duality theory for small Boolean pretoposes in which the dual of the [italic capital]T is the groupoid of models of a Boolean pretopos [italic capital]T equipped with additional structure derived from ultraproducts. The duality theorem states 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.