Categorical logic
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.[1] 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 impredicative theories, such as System F, is an example of the usefulness of categorical semantics.
- It was found that the adjoint functor, and that the quantifiers were also best understood using adjoint functors.[2]
- Internal languages
- This can be seen as a formalization and generalization of proof by 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 βη-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 logicthis way.
See also
Notes
- ^
Goguen, Joseph; Mossakowski, Till; de Paiva, Valeria; Rabe, Florian; Schroder, Lutz (2007). "An Institutional View on Categorical Logic". CiteSeerX 10.1.1.126.2361.
- ^ Lawvere 1971, Quantifiers and Sheaves
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.
- 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.
- ISBN 978-0-13-323809-9.
- ISBN 978-0-521-35653-4.
- ISBN 978-0-521-01060-3.
- Lawvere, F.W.; ISBN 978-1-139-64396-2.
Seminal papers
- PMID 16591125.
- — (December 1964). "Elementary Theory of the Category of Sets". Proceedings of the National Academy of Sciences. 52 (6): 1506–11. 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. Zbl 0261.18010.
Further reading
- 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 categoryas universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types.
- Marquis, Jean-Pierre; Reyes, Gonzalo E. "The History of Categorical Logic 1963–1977". Gabbay, Kanamori & Woods 2012. pp. 689–800.
A preliminary version.
External links
- Awodey, Steve (9 July 2022). "Categorical Logic". lecture notes.
- Lurie, Jacob. "Categorical Logic (278x)". lecture notes.