The main aim of this paper is to prove the so-called descent theorem for Boolean
pretoposes. In section 2, the theorem will be stated in categorical terms, and in section 3, in the
language of symbolic logic. In its symbolic-logical form, the theorem is an apparently new
result for pure first order logic. In fact, it is a statement on the syntax of first order logic, whose
arithmetic complexity is fu , similarly to the Beth definability theorem (see [C/K]), and to
many other model-theoretical results (syntactic characterizations, preservation theorems) that
may be stated in a purely syntactical manner. (The fu-form comes from the fact that the results
in question, including the theorem of this paper, are of the general form: "for all deductions of a
certain kind, there is another deduction of a certain other kind", where the "kinds" in question
are given by recursive conditions).
The descent theorem contains the Beth definability theorem as a part, and it may be
considered as a definability theorem for implicitly definable new primitives that are not
necessarily subsets of the basic universe, but may be added on the outside, on new sorts.
(H. Gaifman's theorem (see e.g.[M3]), which is a definability theorem of a similar general
character, is not the same as the descent theorem. As we will see, Gaifman's result can be
deduced from the present work; I do not see how to obtain the main theorem of this paper from
Gaifman's theorem, or his methods.) The descent theorem is a statement concerning the
definability properties of set-valued functors on certain categories of models.
Let me give the main points of the history of the result. The theorem is, in the first
place, inspired by, and formally analogous to, the descent theorem for open geometric
morphisms established by A. Joyal and M. Tierney in [J/T] , a paper of fundamental importance
for, among others, categorical logic. That paper contains the discovery of a far-reaching analogy
between the "algebra" of (infinitary) first order logic, and "Abelian" algebra. In fact, the descent
theorems of [J/T] are analogous to A. Grothendieck's descent theorem [G] for modules, and
sheaves of modules.
It was A. M. Pitts who conjectured the theorem of this paper in the first place, alongside
others to be mentioned below, in the context of his work involving a transfer of results and
"spirit" from [J/T] to finitary logic (see [PI], [P2], [P3], [P4]). The mechanism of the transfer,
taking the shape of functorial constructions, is Pitts' main discovery; it leads him to new results
on finitary logic, as well as to the most satisfactory treatment available of interpolation and
definability in the usual sense for intuitionistic logic.
In his thesis [Zl], M. Zawadowski proved one of Pitts' conjectures, the lax descent