Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also 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 disjunction and existence properties of intuitionistic logic this way.
These three themes are related. The categorical semantics of a logic consists in describing a category of structured categories that is related to the category of theories in that logic by an adjunction, where the two functors in the adjunction give the internal language of a structured category on the one hand, and the term model of a theory on the other.
See also
Notes
- Goguen, Joseph; Mossakowski, Till; de Paiva, Valeria; Rabe, Florian; Schroder, Lutz (2007). "An Institutional View on Categorical Logic". International Journal of Software and Informatics. 1 (1): 129–152. CiteSeerX 10.1.1.126.2361.
- Lawvere 1971, Quantifiers and Sheaves
- Aluffi 2009
References
- Books
- Abramsky, Samson; Gabbay, Dov (2001). Logic and algebraic methods. Handbook of Logic in Computer Science. Vol. 5. Oxford University Press. ISBN 0-19-853781-6.
- Aluffi, Paolo (2009). Algebra: Chapter 0 (1st ed.). American Mathematical Society. pp. 18–20. ISBN 978-1-4704-1168-8.
- Gabbay, D.M.; Kanamori, A.; Woods, J., eds. (2012). Sets and Extensions in the Twentieth Century. Handbook of the History of Logic. Vol. 6. North-Holland. ISBN 978-0-444-51621-3.
- Kent, Allen; Williams, James G. (1990). Encyclopedia of Computer Science and Technology. Marcel Dekker. ISBN 0-8247-2272-8.
- Barr, M.; Wells, C. (1996). Category Theory for Computing Science (2nd ed.). Prentice Hall. ISBN 978-0-13-323809-9.
- Lambek, J.; Scott, P.J. (1988). Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics. Vol. 7. Cambridge University Press. ISBN 978-0-521-35653-4.
- Lawvere, F.W.; Rosebrugh, R. (2003). Sets for Mathematics. Cambridge University Press. ISBN 978-0-521-01060-3.
- Lawvere, F.W.; Schanuel, S.H. (2009). Conceptual Mathematics: A First Introduction to Categories (2nd ed.). Cambridge University Press. ISBN 978-1-139-64396-2.
Seminal papers
- Lawvere, F.W. (November 1963). "Functorial Semantics of Algebraic Theories". Proceedings of the National Academy of Sciences. 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi:10.1073/pnas.50.5.869. JSTOR 71935. PMC 221940. PMID 16591125.
- — (December 1964). "Elementary Theory of the Category of Sets". Proceedings of the National Academy of Sciences. 52 (6): 1506–11. Bibcode:1964PNAS...52.1506L. doi:10.1073/pnas.52.6.1506. JSTOR 72513. PMC 300477. PMID 16591243.
- — (1971). "Quantifiers and Sheaves". Actes : Du Congres International Des Mathematiciens Nice 1-10 Septembre 1970. Pub. Sous La Direction Du Comite D'organisation Du Congres. Gauthier-Villars. pp. 1506–11. OCLC 217031451. Zbl 0261.18010.
Further reading
- Makkai, Michael; Reyes, Gonzalo E. (1977). First order categorical logic. Lecture Notes in Mathematics. Vol. 611. Springer. doi:10.1007/BFb0066201. ISBN 978-3-540-08439-6.
- Lambek, J.; Scott, P.J. (1988). Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics. Vol. 7. Cambridge University Press. ISBN 978-0-521-35653-4. 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. Vol. 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.
- Bell, John Lane (2001). "The Development of Categorical Logic". In Gabbay, D.M.; Guenthner, Franz (eds.). Handbook of Philosophical Logic. Vol. 12 (2nd ed.). Springer. pp. 279–361. ISBN 978-1-4020-3091-8. Version available online at John Bell's homepage.
- Marquis, Jean-Pierre; Reyes, Gonzalo E. "The History of Categorical Logic 1963–1977". Gabbay, Kanamori & Woods 2012. pp. 689–800.
A preliminary version. - Awodey, Steve (12 July 2024). "Categorical Logic". lecture notes.
- Lurie, Jacob. "Categorical Logic (278x)". lecture notes.