Categorical logic

Categorical logic is a branch of category theory within mathematics, adjacent to mathematical logic but more notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.

Overview

There are three important themes in the categorical approach to logic:

Categorical semantics

Categorical logic introduces the notion of structure valued in a category C with the classical model theoretic notion of a structure appearing in the particular case where C is the category of sets and functions. This notion has proven useful when the set-theoretic notion of a model lacks generality and/or is inconvenient. R.A.G. Seely's modeling of various impredicative theories, such as system F is an example of the usefulness of categorical semantics.

Internal languages

This can be seen as a formalization and generalization of proof by diagram chasing. One defines a suitable internal language naming relevant constituents of a category, and then applies categorical semantics to turn assertions in a logic over the internal language into corresponding categorical statements. This has been most successful in the theory of toposes, where the internal language of a topos together with the semantics of intuitionistic higher-order logic in a topos enables one to reason about the objects and morphisms of a topos "as if they were sets and functions". This has been successful in dealing with toposes that have "sets" with properties incompatible with classical logic. A prime example is Dana Scott's model of untyped lambda calculus in terms of objects that retract onto their own function space. Another is the Moggi-Hyland model of system F by an internal full subcategory of the effective topos of Martin Hyland.

Term-model constructions

In many cases, the categorical semantics of a logic provide a basis for establishing a correspondence between theories in the logic and instances of an appropriate kind of category. A classic example is the correspondence between theories of βη-equational logic over simply typed lambda calculus and cartesian closed categories. Categories arising from theories via term-model constructions can usually be characterized up to equivalence by a suitable universal property. This has enabled proofs of meta-theoretical properties of some logics by means of an appropriate categorical algebra. For instance, Freyd gave a proof of the existence and disjunction properties of intuitionistic logic this way.

Historical perspective

Categorical logic originated with William Lawvere's Functorial Semantics of Algebraic Theories (1963), and Elementary Theory of the Category of Sets (1964).^[1] Lawvere recognised the Grothendieck topos, introduced in algebraic topology as a generalised space, as a generalisation of the category of sets (Quantifiers and Sheaves (1970)).^[2] With Myles Tierney, Lawvere then developed the notion of elementary topos, thus establishing the fruitful field of topos theory, which provides a unified categorical treatment of the syntax and semantics of higher-order predicate logic.^[3] The resulting logic is formally intuitionistic. Andre Joyal is credited, in the term Kripke–Joyal semantics, with the observation that the sheaf models for predicate logic, provided by topos theory, generalise Kripke semantics.^[4] Joyal and others applied these models to study higher-order concepts such as the real numbers in the intuitionistic setting.

An analogous development was the link between the simply typed lambda calculus and cartesian-closed categories (Lawvere, Lambek, Scott), which provided a setting for the development of domain theory. Less expressive theories, from the mathematical logic viewpoint, have their own category theory counterparts. For example the concept of an algebraic theory leads to Gabriel–Ulmer duality. The view of categories as a generalisation unifying syntax and semantics has been productive in the study of logics and type theories for applications in computer science.^[5]

The founders of elementary topos theory were Lawvere and Tierney. Lawvere's writings, sometimes couched in a philosophical jargon, isolated some of the basic concepts as adjoint functors (which he explained as 'objective' in a Hegelian sense, not without some justification). A subobject classifier is a strong property to ask of a category, since with cartesian closure and finite limits it gives a topos (axiom bashing shows how strong the assumption is). Lawvere's further work in the 1960s gave a theory of attributes, which in a sense is a subobject theory more in sympathy with type theory. Major influences subsequently have been Martin-Löf type theory from the direction of logic, type polymorphism and the calculus of constructions from functional programming, linear logic from proof theory, game semantics and the projected synthetic domain theory. The abstract categorical idea of fibration has been much applied.

To go back historically, the major irony here is that in large-scale terms, intuitionistic logic had reappeared in mathematics, in a central place in the Bourbaki–Grothendieck program, a generation after the messy Brouwer–Hilbert controversy had ended, with Hilbert the apparent winner. Bourbaki, or more accurately Jean Dieudonné, having laid claim to the legacy of Hilbert and the Göttingen school including Emmy Noether, had revived intuitionistic logic's credibility (although Dieudonné himself found Intuitionistic Logic ludicrous), as the logic of an arbitrary topos, where classical logic was that of 'the' topos of sets. This was one consequence, certainly unanticipated, of Grothendieck's relative point of view; and not lost on Pierre Cartier, one of the broadest of the core group of French mathematicians around Bourbaki and IHES. Cartier was to give a Séminaire Bourbaki exposition of intuitionistic logic.

In an even broader perspective, one might take category theory to be to the mathematics of the second half of the twentieth century, what measure theory was to the first half. It was Kolmogorov who applied measure theory to probability theory, the first convincing (if not the only) axiomatic approach. Kolmogorov was also a pioneer writer in the early 1920s on the formulation of intuitionistic logic, in a style entirely supported by the later categorical logic approach (again, one of the formulations, not the only one; the realizability concept of Stephen Kleene is also a serious contender here). Another route to categorical logic would therefore have been through Kolmogorov, and this is one way to explain the protean Curry–Howard isomorphism.

See also

• History of topos theory

References

Books

• Abramsky, Samson; Gabbay, Dov (2001). Handbook of Logic in Computer Science: Logic and algebraic methods. Oxford: Oxford University Press. ISBN 0-19-853781-6. 

• Gabbay, Dov (2012). Handbook of the History of Logic: Sets and extensions in the twentieth century. Oxford: Elsevier. ISBN 978-0-444-51621-3. 

• Kent, Allen; Williams, James G. (1990). Encyclopedia of Computer Science and Technology. New York: Marcel Dekker Inc. ISBN 0-8247-2272-8. 

• Barr, M. and Wells, C. (1990), Category Theory for Computing Science. Hemel Hempstead, UK.
• Lambek, J. and Scott, P.J. (1986), Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, UK.
• Lawvere, F.W., and Rosebrugh, R. (2003), Sets for Mathematics. Cambridge University Press, Cambridge, UK.
• Lawvere, F.W. (2000), and Schanuel, S.H., Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press, Cambridge, UK, 1997. Reprinted with corrections, 2000.

Seminal papers

• Lawvere, F.W., Functorial Semantics of Algebraic Theories. In Proceedings of the National Academy of Science 50, No. 5 (November 1963), 869-872.
• Lawvere, F.W., Elementary Theory of the Category of Sets. In Proceedings of the National Academy of Science 52, No. 6 (December 1964), 1506-1511.
• Lawvere, F.W., Quantifiers and Sheaves. In Proceedings of the International Congress on Mathematics (Nice 1970), Gauthier-Villars (1971) 329-334.

Notes

Further reading

• Michael Makkai and Gonzalo E. Reyes, 1977, First order categorical logic, Springer-Verlag.
• Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic. Fairly accessible introduction, but somewhat dated. The categorical approach to higher-order logics over polymorphic and dependent types was developed largely after this book was published.
• Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.  A comprehensive monograph written by a computer scientist; it covers both first-order and higher-order logics, and also polymorphic and dependent types. The focus is on fibred category as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types. According to P.T. Johnstone, this approach is unwieldy for simple types.
• P.T. Johnstone, 2002, Sketches of an Elephant, part D (vol 2) covers both first-order and higher-order logics, but not dependent or polymorphic types, considered by the author of interest mainly to computer science. Because it avoids polymorphic and dependent types, the categorical approach is easier to present in therms of a syntactic category just as in Lambek's book, but Sketches includes more recent developments, like .

• John Lane Bell (2005) The Development of Categorical Logic. Handbook of Philosophical Logic, Volume 12. Springer. Version available online at John Bell's homepage.

• Jean-Pierre Marquis and Gonzalo E. Reyes (2012). The History of Categorical Logic 1963–1977. Handbook of the History of Logic: Sets and Extensions in the Twentieth Century, Volume 6, D. M. Gabbay, A. Kanamori & J. Woods, eds., North-Holland, pp. 689-800. A preliminary version is available at .

External links

• Categorical Logic lecture notes by Steve Awodey