DUALITY AND DEFINABILITY IN FIRST ORDER LOGIC

IX

(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