DUALITY AND DEFINABILITY IN FIRST ORDER LOGIC
(inductive limits), the bread and butter of category theory. A basic strategy underlying this paper
(in this respect, the paper is certainly not alone!) is the lifting of facts and constructions from
posets to categories.
A further parallel to be exploited, possibly despite our initial disbelief, is one between
the 2-element total ordering 2 , and Set , the category of (small) sets and functions. The fact
that there is a fruitful parallel between those two objects is well-known in category theory; e.g.,
the theory of profunctors is based on such a consideration. However, the way we exploit the
parallel is not along the lines of general category theory: what is happening in this paper is pure
category theory, but not general category theory.
Classical propositional logic may be identified with the study of the properties of 2
endowed with the operations of finite infs and sups, as well as complementation, resulting in the
theory of Boolean algebras. Categorical logic shows (see, e.g., [M/R], also [M3]) that classical
first order predicate logic can be regarded as the study of finite limits and (certain) finite
colimits (along with complementation of subobjects) within Set , resulting in the notion of
(Boolean) pretopos, due to A. Grothendieck [SGA4]. For instance, as the completeness theorem
for propositional logic (Emil Post, 1921) is expressed in the theory of Boolean algebras as the
Stone representation theorem, the Godel(/Malcev) completeness theorem for first order logic is
"translation"-equivalent to the Deligne(/Joyal) representation theorem [SGA4] for pretoposes, a
result of great formal similarity to the Stone result. It is precisely the formal similarities that
interest us in the first place. We will try to guess new results in predicate logic by formally
lifting known situations from the propositional case, via the categorical framework, and in fact,
we will even try to guess the new proofs in this way. It so happens that we can do much along
these lines, and the enterprise takes us on a journey in interesting new mathematics.
Another aspect of our lifting strategy is the passing from categories of the basic
structures involved (category of Boolean algebras, category of Stone spaces) to 2-categories of
the new basic structures (pretoposes, ultracategories). Every time one deals with category-based
structures, those structures will form, most naturally, 2-categories (or possibly bicategories,
which are more complex than 2-categories). The universal algebra of category-based structures
largely overlaps with 2-(bi-)category theory.
Nevertheless, in the concluding section, which contains the finishing touches to the proof
of the descent theorem, I will give a version of the proof that is stripped of the 2-category
theory. Sections 2 and 11 will thus be rendered superfluous, at the expense, however, of losing
the conceptual formulation of the theorem as Theorem 2.2 in Section 2, as well as losing much
of the heuristics underlying the work.
Of course, there is an obligatory disclaimer called for here: I am not sure that the descent
theorem really requires the machinery used and developed here. Even if the answer is "no",
however, I am pleased with the motivation it has given me to look for the duality theorem for
Boolean pretoposes, which I had long thought ought to look something like the theorem here