View source for Categorical logic

{{TEX|done}}
A branch of mathematics dealing with the interaction between logic (cf. also [[Mathematical logic|Mathematical logic]]) and [[Category|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|proof theory]], [[Recursion|recursion]] theory and [[Model theory|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 $f\colon A\to B$ is a method of inferring $B$ from $A$ (cf. also [[Derivation, logical|Derivation, logical]]; [[Natural logical deduction|Natural logical deduction]]). Evidently, deducibility is reflexive and transitive, and this translates into the identity deduction $1_A\colon A\to A$ and into composition of deductions

$$\frac{f\colon A\to B\quad g\colon B\to C}{gf\colon A\to C}.$$

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

$$f1_A=f=1_Bf,$$

$$ (hg)f = h(gf)$$

where $h\colon C\to D$. 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 [[#References|[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 $\top$ and two binary connectives $A\land B$ and $A\Rightarrow B$ between formulas satisfying the following axioms and rules of inference:

$$\mathbf p_{AB}\colon A\land B\to A,\quad \mathbf q_{AB}\colon A\land B\to B,$$

$$\mathbf o_A\colon A\to\top,\quad \mathbf e_{AB}\colon A\land (A\Rightarrow B) \to B,$$

$$\frac{f\colon C\to A\quad g\colon C\to B}{\langle f,g\rangle\colon C\to A\land B},$$

$$\frac{f\colon A\land C\to B}{f^*\colon C\to A\Rightarrow B}.$$

If one introduces appropriate equations, for instance, $\mathbf p_{AB}\langle f,g\rangle = f,$ one obtains what F.W. Lawvere [[#References|[a7]]] calls a Cartesian closed category (cf. also [[Closed category|Closed category]]). These equations will ensure that there is exactly one arrow $A\to\top$, making $\top$ a terminal object, that there is a one-to-one correspondence between pairs of arrows $C\to A, C\to B$ and arrows $C\to A\land B$, making $A\land B$ a Cartesian product, and that there is a one-to-one correspondence between arrows $A\land C\to B$ and arrows $C\to A\Rightarrow B,$ making $A\Rightarrow B$ a case of exponentiation. Lawvere threw additional light on this situation by noting, for instance, that $-\land C\to B$ and $C\to -\Rightarrow B$ are adjoint functors. Passing to categorical notation, one writes $1$ for $\top$, $A\times B$ for $A\land B$ and $B^A$ for $A\Rightarrow B$.

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

$$c^{a\times b} = (c^b)^a,$$

$$(a\times b)^c = a^c\times b^c, c^{a+b} = c^a\times c^b,$$

translate into the following equivalences in the intuitionistic propositional calculus:

$$(A\land B)\Rightarrow C \leftrightarrow A\Rightarrow(B\Rightarrow C),$$

$$C\Rightarrow(A\land B) \leftrightarrow (C\Rightarrow A)\land(C\Rightarrow B),
  (A\lor B)\Rightarrow C \leftrightarrow (A\Rightarrow C)\land(B\Rightarrow C).
$$

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

The traditional deduction theorem admits the following analogue for Lawvere-style deductive systems: If $\varphi(x)\colon A\to B$ can be inferred from the assumption $x\colon\top\to C$, then there is a deduction $f\colon C\land A\to B$ not using this assumption.

Algebraically, one may think of $x$ as an indeterminate arrow and of $\varphi(x)$ as a polynomial in $x$. Moreover, it turns out that

$$f\langle x\mathbf o_A, 1_A\rangle = \varphi(x).$$

In the special case when $A=\top$, and upon replacing $f\colon A\to B$ by $g\colon\top\to A\Rightarrow B,$ this equation may be written as

$$\mathbf e_{AB}\langle g, x\rangle = \varphi(x),$$

and it is customary to write $g=\lambda_{x\in C}\varphi(x)$ and to think of $\mathbf e_{AB}$ as application.

One is thus led to the traditional typed $\lambda$-calculus (cf. [[Lambda-calculus|$\lambda$-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 [[#References|[a12]]] and [[#References|[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 [[#References|[a8]]].

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

$$f\colon A_1\dots A_n\to B.$$

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

$$\frac{f\colon\Lambda\to A\quad g\colon\Gamma A\Delta\to B}{g \& f\colon \Gamma\Lambda\Delta\to B}.$$

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:

$$\frac{f\colon\Gamma\to A\quad g\colon \Gamma\to B}{\langle f,g\rangle\colon\Gamma\to A\land B},$$

$$\frac{f\colon\Gamma A\Delta\to C}{f_p\colon\Gamma A\land B\Delta\to C},
  \frac{f\colon\Gamma B\Delta\to C}{f_q\colon\Gamma A\land B\Delta\to C}.
$$

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 [[#References|[a2]]]. A multi-category satisfying the structural rules is nothing else than a many-sorted algebraic theory (cf. also [[Many-valued logic|Many-valued logic]]). A multi-category not satisfying them is a context-free recognition grammar (cf. also [[Grammar, context-free|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 $\land$ must be distinguished from the tensor product $\otimes$, which is introduced as follows:

$$\frac{f\colon\Gamma\to A\quad g\colon\Delta\to B}{\{f,g\}\colon\Gamma\Delta\to A\otimes B},$$

$$\frac{f\colon\Gamma AB\Delta\to C}{f^S\colon\Gamma A\otimes B\Delta\to C}.$$

Postulating suitable equations, one ensures that there is a one-to-one correspondence between deductions $\Gamma AB\Delta\to C$ and $\Gamma A\otimes B\Delta\to C$. This is essentially how N. Bourbaki defined the [[Tensor product|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

$$
((A\otimes B)\otimes C)\otimes D \to
(A\otimes B)\otimes (C \otimes D) \to
A\otimes (B\otimes (C \otimes D)) \to
A\otimes ((B\otimes C) \otimes D) \to
(A\otimes (B\otimes C)) \otimes D \to
((A\otimes B)\otimes C) \otimes D
$$

is the identity.

==Categorical aspect of recursive functions.==
According to F.W. Lawvere, a natural numbers object $(N,0,S)$, with $0\colon 1\to N$ and $S\colon N\to N$, can be defined in any Cartesian closed category: For any $a\colon 1\to A$ and $h\colon A\to A$ there exists a unique $f\colon N\to A$ such that $f0 = a$ and $fS = hf$. In the familiar category of sets (cf. also [[Sets, category of|Sets, category of]]), this means that $f(n)=h^n(a)$ for any natural number $n$ (cf. also [[Natural numbers object|Natural numbers object]]). The arrows $N^k\to N$ 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|Partial recursive function]]). They include of course all primitive recursive functions (cf. also [[Primitive recursive function|Primitive recursive function]]).

If one is interested in partial recursive functions, say in a single variable, one should pass to the [[Monoid|monoid]] of binary relations on $\N$, 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 $fg^\wedge$, where $f$ and $g$ are primitive recursive functions and $g^\wedge$ is the converse of $g$. It will be a partial recursive function if and only if $g^\wedge g\leq f^\wedge f$ and a total recursive function if and only if also $1\leq gg^\wedge$.

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 $A\lor B$ as

$$\forall X (((A\Rightarrow X)\land (B\Rightarrow X))\Rightarrow X)$$

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

$$\prod_X (X^X)^{X^X} \cong \prod_X X^{X^{X+1}},$$

following L. Wittgenstein and A. Church. The second expression also shows that the natural numbers object is the least fixpoint of the functor $X\mapsto X+1$, 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 [[#References|[a11]]]. Computer scientists are interested in finding other such fixpoints working with $\prod_X X^{X^{T(X)}}$, where $T$ 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é [[#References|[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|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é [[#References|[a14]]], as what the latter call an  "accessible"  category. A category $\mathcal A$ is said to be accessible if there is an infinite regular cardinal number $\kappa$ and a small full subcategory $\mathcal B$ consisting of $\kappa$-presentable objects of $\mathcal A$ such that every object of $\mathcal A$ is a $\kappa$-filtered co-limit of $\kappa$-filtered diagrams in $\mathcal B$ (cf. also [[Diagram|Diagram]]; [[Category|Category]]; [[Object in a category|Object in a category]]). As a special case one obtains the result for locally presentable categories [[#References|[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 $\Omega$, accompanied by a distinguished arrow $\operatorname{true}\colon 1\to\Omega$ such that, for each object $A$, there is a one-to-one correspondence between subobjects $B$ of $A$ and morphisms $\chi\colon A\to B$ (cf. also [[Topos|Topos]]). This correspondence may be expressed in categorical language, but in the familiar category of sets, where $\Omega = \{\operatorname{true}, \operatorname{false}\}$, it means that $a\in B$ if and only if $\chi(a)=\operatorname{true}$. 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|Types, theory of]]), has basic types $\Omega$ and $N$, from which other types are constructed as Cartesian products and by exponentiation, although it suffices to consider exponentiation with base $\Omega$. In addition to variables of each type, one also has terms:

$$a=a'\text{ and } a\in\alpha \quad \text{ of type }\Omega,$$

$$\langle a,b\rangle\text{ of type } A\times B, \{x\in A\colon\varphi(x)\}\text{ of type } \Omega^A,$$

$$0\text{ and }Sn\quad\text{ of type } N,$$

where $a$ and $a'$ are of type $A$, $\alpha$ is of type $\Omega^A$, $b$ is of type $B$, $\varphi(x)$ is of type $\Omega^A$, $x$ being a variable of type $A$, and $n$ is of type $N$. Logical operations may now be defined; for example, $\forall x\in A, \phi(x)$ is short for

$$\{x\in A\colon \varphi(x)\} = \{x\in A\colon x=x\}.$$

With any topos $\mathcal T$ there is associated an internal language $L(\mathcal T)$, whose types are the objects of $\mathcal T$ and whose closed terms of type $A$ are arrows $1\to A$. Conversely, any language $\mathcal L$ generates a topos $T(\mathcal L)$, whose objects are closed terms of type $\Omega^A$, 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 $TL(\mathcal T)$ is equivalent to $\mathcal T$, hence every topos may be assumed to be generated by a language, and that $LT(\mathcal L)$ is a conservative extension of $\mathcal L$.

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

$\bot$ ist not true in $L(\mathcal T)$;

$p\lor q$ holds in $L(\mathcal T)$ only if either $p$ or $q$ holds;

$\exists x\in A, \varphi(x)$ holds in $L(\mathcal T)$ only if $\varphi(a)$ holds for some term $a$ of type $A$, that is, some arrow $a\colon 1\to A$ in $\mathcal T$. As P. Freyd observed, these conditions assert algebraically that $1$ is not initial and that it is an indecomposable projective. For Boolean toposes $\mathcal T$, that is, when $L(\mathcal T)$ is classical, $\mathcal T$ being local means that $1$ is a generator: two arrows $f,g\colon A\to B$ are equal if $fa=ga$ for all $a\colon 1\to A$ [[#References|[a9]]].

It is a non-trivial fact that the so-called free topos $T(\mathcal L_0)$ generated by pure intuitionistic type theory $\mathcal L_0$, 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 $p$ of $\mathcal L_0$ is true in $T(\mathcal L_0)$ if and only if it is provable, that is, its truth can be checked. Moreover, the existential quantifier of $LT(\mathcal L_0)$ allows a substitutional interpretation: if $\exists x\in A, \varphi(x)$ is true in $T(\mathcal L_0)$, then $\varphi(a)$ is true in $T(\mathcal L_0)$ for some closed term in its internal language, that is, for some arrow $a\colon 1\to A$. Another topos used for illustrating intuitionistic principles is Hyland's effective topos [[#References|[a9]]].

==Categorical completeness theorems.==
Completeness theorems in logic assert that certain theories have enough models (cf. also [[Gödel completeness theorem|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 [[#References|[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 $S(A)$ of subobjects of any object $A$ is a [[Lattice|lattice]] and, for any $f\colon A\to B$, the induced mapping $f^*\colon S(B)\to S(A)$ has a left adjoint $\exists_f$ which is stable under substitution. The last property is a categorical translation of saying that the application of $\exists_z$ to $\varphi(y,z)$ commutes with substituting $\psi(y')$ for $y$. If, furthermore, $f^*$ has a right adjoint $\forall_f$, the coherent category is said to be a Heyting category.

Joyal's theorem is equivalent to that of Gödel and Mal'tsev [[#References|[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 $\mathbf{Set}^{\mathcal P}$, where $\mathcal P$ 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 [[#References|[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|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|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 [[#References|[a5]]] (cf. also [[Set theory|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 $\mathcal L_0$, 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 $T(\mathcal L_0)$, for example, $p\lor q$ is true in the free topos if and only if $p$ is true or $q$ is. Even an existential statement $\exists x\in A, \varphi(x)$ is true in the free topos if and only if $\varphi(a)$ is true for some term $a$ of type $A$ 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|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 $\varphi(x)$, with $x$ a variable of type $N$, such that $\forall x\in N, \varphi(x)$ is not true in $T(\mathcal L_0)$, even though $\varphi(a)$ is true for each closed term $a$ of type $N$. It so happens that the only closed terms of type $N$ in the internal language of the free topos are the standard numerals $0,S0,SS0$, etc.

Only few mathematicians are intuitionists and most believe in the axiom of the excluded third (cf. [[Law of the excluded middle|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====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  P. Gabriel,   F. Ulmer,   "Lokal präsentierbare Kategorien" , ''Lecture Notes Math.'' , '''221''' , Springer  (1971)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  K. Došen,   P. Schroeder-Heister,   "Substructural logics" , Oxford Univ. Press  (1993)</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  S. Eilenberg,   S. Mac Lane,   "General theory of natural equivalences"  ''Trans. Amer. Math. Soc.'' , '''58'''  (1945)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  W.S. Hatcher,   "The logical foundations of mathematics" , Pergamon  (1982)</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  A. Joyal,   I Moerdijk,   "Algebraic set theory" , Cambridge Univ. Press  (1995)</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  J. Lambek,   P.J. Scott,   "Introduction to higher order categorical logic" , Cambridge Univ. Press  (1986)</TD></TR><TR><TD valign="top">[a7]</TD> <TD valign="top">  F.W. Lawvere,   "Adjointness in foundations"  ''Dialectica'' , '''23'''  (1969)  pp. 281–296</TD></TR><TR><TD valign="top">[a8]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[a9]</TD> <TD valign="top">  C. McLarty,   "Elementary categories, elementary toposes" , Clarendon Press  (1992)</TD></TR><TR><TD valign="top">[a10]</TD> <TD valign="top">  D. Prawitz,   "Natural deduction" , Almquist and Wiksell  (1965)</TD></TR><TR><TD valign="top">[a11]</TD> <TD valign="top">  R.A.G. Seely,   "Categorical semantics for higher order polymorphic lambda calculus"  ''J. Symbolic Logic'' , '''52'''  (1987)  pp. 969–989</TD></TR><TR><TD valign="top">[a12]</TD> <TD valign="top">  "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism"  J.P. Seldin (ed.)  J.R. Hindley (ed.) , Acad. Press  (1980)</TD></TR><TR><TD valign="top">[a13]</TD> <TD valign="top">  M. Makkai,   G.E. Reyes,   "First order categorical logic" , ''Lecture Notes Math.'' , '''611''' , Springer  (1977)</TD></TR><TR><TD valign="top">[a14]</TD> <TD valign="top">  M. Makkai,   R. Paré,   "Accessible categories: the foundations of catgeorical model theory" , ''Contemp. Math. Ser.'' , '''104''' , Amer. Math. Soc.  (1989)</TD></TR><TR><TD valign="top">[a15]</TD> <TD valign="top">  K. Došen,   "Cut-elimination in categories" , Kluwer Acad. Publ.  (1999)</TD></TR></table>