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.
It was found that the connectives of pre-categorical logic were more clearly understood using the concept of adjoint functor, and that the quantifiers were also best understood using adjoint functors.
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.

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 Sciences 50, No. 5 (November 1963), 869-872.
• Lawvere, F.W., Elementary Theory of the Category of Sets. In Proceedings of the National Academy of Sciences 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

1. Lawvere, Quantifiers and Sheaves