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
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