Vll l

MICHAEL MAKKAI

theorem for pretoposes; see also [Z2]. Against my initial skepticism, he started out on his way

to the proof with a plan of applying my duality theory [Ml]. He successfully completed his

plan, and contributed, among others, a highly surprising and beautiful argument, which, suitably

transformed, plays a crucial role in this paper as well.

This paper is the result of trying to repeat Zawadowski's feat for the Boolean descent

theorem. The proof, in fact, follows Zawadowski's outline quite faithfully. On the other hand,

there are two essentially new features.

One is that my original duality theory, serving Zawadowski's purposes, had to be

replaced by another one. The new duality theory for Boolean pretoposes is given in sections 4 -

8. It builds on the old theory for pretoposes in general, but it also involves further complexities,

most visible in Section 6 on the "syntax of special ultramorphisms". It turns out that the

technical notions of "cell-system" and the like, brought out explicitly in [M2], but appearing

implicitly in [Ml] already, are useful in the context of this paper too. They are subjected to a

manipulation which is the main technical contribution in this paper.

The other feature is the "preparation of functor specifications" (Section 9) for the

treatment which is the analog of Zawadowski's main argument. This preparation reduces, in

Zawadowski's proof, to an essentially trivial, although important fact (pointed out by Pitts). The

main point in Section 9 is Lemma 1, a forcing argument, "forcing with generic automorphisms",

which, in a somewhat different form, formed a part of an unpublished piece of work done by M.

Ajtai and myself in 1979. The argument seems to be quite fundamental, and I would not be

surprised if in the meantime it had appeared in the literature in some form.

It is well-known that the Beth definability theorem can be proved in an elementary way;

more precisely, within (first order, even recursive) arithmetic. The question remains whether the

descent theorems (the one for pretoposes, and the one for Boolean pretoposes) can be so proved.

Let us mention that Pitts' third conjecture, the descent theorem for Heyting pretoposes, is still

open.

In the first section, we will go through a thoroughly model-theoretical (in the sense of

the model theory of propositional logic, in the style of Section 1.2 of [C/K]), and at the same

time categorical, proof of the Beth definability theorem for classical propositional logic. The

very statement of our main theorem, and later its proof as well, will be obtained by guessing

proper generalizations of the propositional situation. The result will not be the classical Beth

definability theorem for predicate logic, but something considerably (it seems) stronger.

The basis for the possibility of such a generalization is the fundamental, and not

sufficiently appreciated, fact that the notion of category is a generalization of the notion of

partial order, or even preorder: in fact, a preorder is nothing but a category in which every

hom-set is of cardinality at most 1 (" 2-enriched category"). The fundamental notions for the

theory of lattices and Boolean algebras, infs (greatest lower bounds) and sups (least upper

bounds) of families of elements are generalized in the notions of (projective) limits, and colimits