Categorical logic

A branch of mathematics dealing with the interaction between logic (cf. also Mathematical logic) and category theory. Each of these disciplines has profoundly influenced the other. In fact, it may be claimed that, at a very basic level, logic and category theory are the same.

At one time it was customary to divide logic into three parts: proof theory, recursion theory and model theory. To all these, category theory can make some fundamental contributions. Logic has also been used for presenting the foundations of mathematics, and here too category theory has something to say.

Categorical proof theory.

One way of looking at proofs is to see them as deductions. A deduction is a method of inferring from (cf. also Derivation, logical; Natural logical deduction). Evidently, deducibility is reflexive and transitive, and this translates into the identity deduction and into composition of deductions

Originally, logicians were not interested in asking when two deductions are equal; the first to do so was D. Prawitz [a10]. It seems reasonable to demand that

where . Once this is required, the definition of a category is obtained. In such a category the objects are formulas and the arrows are deductions. But this was not the picture S. Eilenberg and S. Mac Lane had in mind when they first introduced categories [a3]. In a more typical concrete category, the objects are structured sets and the arrows (or morphisms) are mappings preserving this structure.

An example of a deductive system is the positive intuitionistic propositional calculus. It deals with a designated formula and two binary connectives and between formulas satisfying the following axioms and rules of inference:

If one introduces appropriate equations, for instance, , one obtains what F.W. Lawvere [a7] calls a Cartesian closed category (cf. also Closed category). These equations will ensure that there is exactly one arrow , making a terminal object, that there is a one-to-one correspondence between pairs of arrows , and arrows , making a Cartesian product, and that there is a one-to-one correspondence between arrows and arrows , making a case of exponentiation. Lawvere threw additional light on this situation by noting, for instance, that and are adjoint functors. Passing to categorical notation, one writes for , for and for .

The categorical point of view offers a unified way of looking at elementary arithmethic and intuitionistic logic. For example, the familiar laws of indices

translate into the following equivalences in the intuitionistic propositional calculus:

It has been assumed here that the propositional calculus has been augmented by the disjunction symbol , which translates into the categorical coproduct.

The traditional deduction theorem admits the following analogue for Lawvere-style deductive systems: If can be inferred from the assumption , then there is a deduction not using this assumption.

Algebraically, one may think of as an indeterminate arrow and of as a polynomial in . Moreover, it turns out that

In the special case when , and upon replacing by , this equation may be written as

and it is customary to write and to think of as application.

One is thus led to the traditional typed -calculus (cf. -calculus) of H.B. Curry and A. Church, although these authors dealt with the proof theory of implication alone, having followed D. Hilbert in applying Occam's razor to eliminate conjunction from the propositional calculus. However, viewing implication as an adjoint to conjunction, some people now (1998) prefer to study the lambda-calculus with surjective pairing, which turns out to be equivalent to a Cartesian closed category, see [a12] and [a6]. Like conjunction and implication, disjunction too can be lifted to the categorical level and turned into the coproduct. Even quantifiers can be presented categorically, as was done in Lawvere's hyperdoctorines [a8].

Multi-categories.

One of the more successful techniques in proof theory was Gentzen's method of cut-elimination (cf. also Gentzen formal system). G. Gentzen dealt with deductions of the form

Composition of deductions must now be replaced by what he called a cut:

Here, capital Greek letters denote strings of formulas. Introducing suitable equations between deductions, one obtains the notion of a multi-category. Gentzen presented the logical connectives with the help of introduction rules which already incorporate some cuts, for example:

He showed that in that case further cuts are no longer necessary, and the same is true for identity deductions of compound formulas. At the multi-category level, every deduction obtained with cut is actually equal to one obtained without.

Gentzen had imposed three structural rules: interchange, contraction and weakening; but the cut-elimination theorem holds even without them, giving rise to what has been called substructural logic [a2]. A multi-category satisfying the structural rules is nothing else than a many-sorted algebraic theory (cf. also Many-valued logic). A multi-category not satisfying them is a context-free recognition grammar (cf. also Grammar, context-free). Thus, multi-categories may be applied in linguistics. More surprisingly, they have recently found applications in theoretical physics.

In the absence of the structural rules, conjunction must be distinguished from the tensor product , which is introduced as follows:

Postulating suitable equations, one ensures that there is a one-to-one correspondence between deductions and . This is essentially how N. Bourbaki defined the tensor product in multi-linear algebra. The usual properties of the tensor product can now be proved, e.g. Mac Lane's pentagonal rule, which says that the compound arrow

is the identity.

Categorical aspect of recursive functions.

According to F.W. Lawvere, a natural numbers object , with and , can be defined in any Cartesian closed category: For any and there exists a unique such that and . In the familiar category of sets (cf. also Sets, category of), this means that for any natural number (cf. also Natural numbers object). The arrows in the free Cartesian closed category with natural numbers object describe those partial recursive functions which can be proved to be universally defined (cf. also Partial recursive function). They include of course all primitive recursive functions (cf. also Primitive recursive function).

If one is interested in partial recursive functions, say in a single variable, one should pass to the monoid of binary relations on , the usual set of natural numbers. This is an ordered monoid with involution (involution is given by taking the converse). A recursively enumerable relation has the form , where and are primitive recursive functions and is the converse of . It will be a partial recursive function if and only if and a total recursive function if and only if also .

Instead of postulating a natural numbers object, one may define such an object, provided one passes to the categorical analogue of propositional logic with variable formulas and quantification over such. The proof theory of the latter is also known as the polymorphic lambda-calculus. Already D. Prawitz had defined as

Passing to categorical notation, one may similarly define the natural numbers object with the help of

following L. Wittgenstein and A. Church. The second expression also shows that the natural numbers object is the least fixpoint of the functor , which recaptures Lawvere's definition. Here, one works in a Cartesian closed category with formal products, a framework for which has been provided by R.A.G. Seely [a11]. Computer scientists are interested in finding other such fixpoints working with , where is a definable endo-functor of the category.

Categorical model theory.

To present the model theory of first order languages categorically, M. Makkai and R. Paré [a14] argue that one may as well assume the logic to be infinitary, allowing not only infinite conjunctions and disjunctions, but also quantification over infinite sets of variables. The language itself may be replaced by a sketch, a concept due to Ch. Ehresmann, namely a small category with distinguished cones and co-cones. A model is a set-valued functor from this category which turns cones into limits and co-cones into co-limits. The category of models, whose arrows are natural transformations, was characterized abstractly by C. Lair, and again independently by M. Makkai and R. Paré [a14], as what the latter call an "accessible" category. A category is said to be accessible if there is an infinite regular cardinal number and a small full subcategory consisting of -presentable objects of such that every object of is a -filtered co-limit of -filtered diagrams in (cf. also Diagram; Category; Object in a category). As a special case one obtains the result for locally presentable categories [a1]: these are accessible and complete.

For the model theory of higher-order logic one now has recourse to the elementary toposes of F.W. Lawvere and M. Tierney. An (elementary) topos is a Cartesian closed category with a subobject classifier , accompanied by a distinguished arrow such that, for each object , there is a one-to-one correspondence between subobjects of and morphisms (cf. also Topos). This correspondence may be expressed in categorical language, but in the familiar category of sets, where , it means that if and only if . Usually, and in the present context, it is also assumed that the topos has a natural numbers object.

An intuitionistic higher-order language, or type theory (cf. also Types, theory of), has basic types and , from which other types are constructed as Cartesian products and by exponentiation, although it suffices to consider exponentiation with base . In addition to variables of each type, one also has terms:

where and are of type , is of type , is of type , is of type , being a variable of type , and is of type . Logical operations may now be defined; for example, is short for

With any topos there is associated an internal language , whose types are the objects of and whose closed terms of type are arrows . Conversely, any language generates a topos , whose objects are closed terms of type , up to provable equality, and whose arrows are binary relations that can be proved to be functions, also up to provable equality. It turns out that is equivalent to , hence every topos may be assumed to be generated by a language, and that is a conservative extension of .

It is tempting to view as models of all logical functors or, equivalently, all translations , but the tradition of Henkin's non-standard models suggest that be a local topos. This means that

is not true in ;

holds in only if either or holds;

holds in only if holds for some term of type , that is, some arrow in . As P. Freyd observed, these conditions assert algebraically that is not initial and that it is an indecomposable projective. For Boolean toposes , that is, when is classical, being local means that is a generator: two arrows are equal if for all [a9].

It is a non-trivial fact that the so-called free topos generated by pure intuitionistic type theory , the initial object in the category of all toposes and logical functors, is local. This fact may be exploited to justify a number of intuitionistic principles. For example, a closed formula of is true in if and only if it is provable, that is, its truth can be checked. Moreover, the existential quantifier of allows a substitutional interpretation: if is true in , then is true in for some closed term in its internal language, that is, for some arrow . Another topos used for illustrating intuitionistic principles is Hyland's effective topos [a9].

Categorical completeness theorems.

Completeness theorems in logic assert that certain theories have enough models (cf. also Gödel completeness theorem). For classical first-order logic such a result is due to K. Gödel and A.I. Mal'tsev, and a generalization to intuitionistic systems was given by S. Kripke. For classical higher-order logic, completeness was established by L.A. Henkin; for the intuitionistic version see [a6].

The first to formulate a categorical version of first-order completeness was A. Joyal, who proved that any small coherent category admits an isomorphism-reflecting coherent functor into a power of the category of sets.

A category is said to be coherent if it has finite limits, the poset of subobjects of any object is a lattice and, for any , the induced mapping has a left adjoint which is stable under substitution. The last property is a categorical translation of saying that the application of to commutes with substituting for . If, furthermore, has a right adjoint , the coherent category is said to be a Heyting category.

Joyal's theorem is equivalent to that of Gödel and Mal'tsev [a13], and it implies Deligne's theorem on the existence of enough points in a coherent topos. Joyal also proved that every small Heyting category has an isomorphism-reflecting Heyting functor to a category of the form , where is a small category.

This result is closely related to Kripke's completeness theorem for intuitionistic predicate calculus and also to Barr's embedding theorem for regular categories. Actually, M. Barr proved more, since he was able to replace "isomorphism reflecting" by "full" . His theorem generalized earlier embedding theorems for Abelian categories by S. Lubkin, P. Freyd and B. Mitchell.

The intuitionistic generalization of Henkin's completeness theorem can be expressed algebraically thus [a6]: Every small topos can be fully embedded by a logical functor into a product of local toposes.

In fact, more can be said, according to a theorem by S. Awodey, improving an earlier result by J. Lambek and I. Moerdijk: Every small topos is the topos of continuous sections of a topological sheaf of local toposes.

Categorical foundations.

According to the Frege–Russell logicist program, the language of symbolic logic was also to serve for the foundations of mathematics. This is only possible if one adopts at least one non-logical axiom, the axiom of infinity, or, equivalently, if one admits the type of natural numbers (cf. also Infinity, axiom of). Conceivably, it is also possible if one allows quantification over types.

The traditional view, held by the majority of those interested in foundations, is that the foundations of mathematics should be expressed in a first-order language, the language of set theory. While an algebraic treatment of Zermelo–Fraenkel set theory has been given in [a5] (cf. also Set theory), most categorists reject the "theology of the membership relation" . In Lawvere's view, one should concentrate on the ternary relation of composition instead of on the binary relation of membership, which leads one to seeing the world of mathematics as a category, in particular, as an elementary topos. As indicated above, toposes are essentially the same as type theories.

But which topos is "the" category of sets? It should be "a" local topos; but a Platonist would wish to replace the indefinite article by the definite one. An intuitionist, albeit a moderate one, might be happy with the free topos, the topos generated by pure intuitionistic type theory , in which no unnecessary axioms hold and no unnecessary terms are introduced. It so happens that many of the logical connectives have the expected interpretation in , for example, is true in the free topos if and only if is true or is. Even an existential statement is true in the free topos if and only if is true for some term of type in its internal language. Unfortunately, negation, implication and universal quantification do not have the expected interpretation (unless one expects the so-called Brouwer–Heyting–Kolmogerov interpretation). This is so, in view of the Gödel incompleteness theorem or its proof. Although Gödel's original argument was about classical type theory, it remains valid for intuitionistic type theory. For example, Gödel exhibited a formula , with a variable of type , such that is not true in , even though is true for each closed term of type . It so happens that the only closed terms of type in the internal language of the free topos are the standard numerals , , , etc.

Only few mathematicians are intuitionists and most believe in the axiom of the excluded third (cf. Law of the excluded middle). In accordance with the majority view, one should search for a Boolean local topos as the world of mathematics. Unfortunately, it follows from Gödel's incompleteness theorem that the topos generated by pure classical type theory is not local. Still, the completeness theorem ensures a plentitude of Boolean local toposes. Yet it seems difficult to put one's finger on a distinguished Boolean local topos, and some mathematicians have even suggested one should stop looking for one and accept the plurality of mathematical worlds instead.

References

[a1]	P. Gabriel, F. Ulmer, "Lokal präsentierbare Kategorien" , Lecture Notes Math. , 221 , Springer (1971)
[a2]	K. Došen, P. Schroeder-Heister, "Substructural logics" , Oxford Univ. Press (1993)
[a3]	S. Eilenberg, S. Mac Lane, "General theory of natural equivalences" Trans. Amer. Math. Soc. , 58 (1945)
[a4]	W.S. Hatcher, "The logical foundations of mathematics" , Pergamon (1982)
[a5]	A. Joyal, I Moerdijk, "Algebraic set theory" , Cambridge Univ. Press (1995)
[a6]	J. Lambek, P.J. Scott, "Introduction to higher order categorical logic" , Cambridge Univ. Press (1986)
[a7]	F.W. Lawvere, "Adjointness in foundations" Dialectica , 23 (1969) pp. 281–296
[a8]	F.W. Lawvere, "Equality in hyperdoctrines and comprehension schema as an adjoint functor" A. Heller (ed.) , Proc. New York Symp. Appl. Categorical Algebra , Amer. Math. Soc. (1970) pp. 1–14
[a9]	C. McLarty, "Elementary categories, elementary toposes" , Clarendon Press (1992)
[a10]	D. Prawitz, "Natural deduction" , Almquist and Wiksell (1965)
[a11]	R.A.G. Seely, "Categorical semantics for higher order polymorphic lambda calculus" J. Symbolic Logic , 52 (1987) pp. 969–989
[a12]	"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism" J.P. Seldin (ed.) J.R. Hindley (ed.) , Acad. Press (1980)
[a13]	M. Makkai, G.E. Reyes, "First order categorical logic" , Lecture Notes Math. , 611 , Springer (1977)
[a14]	M. Makkai, R. Paré, "Accessible categories: the foundations of catgeorical model theory" , Contemp. Math. Ser. , 104 , Amer. Math. Soc. (1989)
[a15]	K. Došen, "Cut-elimination in categories" , Kluwer Acad. Publ. (1999)