INTRODUCTION

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

vn