categorical logic

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.{{harvnb|Lawvere|1971|loc=Quantifiers and Sheaves}}

;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.{{harvnb|Aluffi|2009}} 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.

• History of topos theory
• Coherent topos

{{Portal|Mathematics}}

{{reflist}}

;Books

{{refbegin}}

• {{cite book

|last1=Abramsky

|first1=Samson

|last2=Gabbay

|first2=Dov

|series=Handbook of Logic in Computer Science |volume=5

|title=Logic and algebraic methods

|publisher=Oxford University Press

|year=2001

|isbn=0-19-853781-6

}}

• {{Cite book |last=Aluffi |first=Paolo |title=Algebra: Chapter 0 |publisher=American Mathematical Society |year=2009 |isbn=978-1-4704-1168-8 |edition=1st |pages=18–20}}
• {{cite book |editor1-first=D.M. |editor1-last=Gabbay |editor2-first=A. |editor2-last=Kanamori |editor3-first=J. |editor3-last=Woods |title=Sets and Extensions in the Twentieth Century |publisher=North-Holland |series=Handbook of the History of Logic |volume=6 |date=2012 |isbn=978-0-444-51621-3 |url={{GBurl|ZF_QckMFy-oC|pg=PR5}}}}

• {{cite book

|last1=Kent

|first1=Allen

|last2=Williams

|first2=James G.

|title=Encyclopedia of Computer Science and Technology

|publisher=Marcel Dekker

|year=1990

|isbn=0-8247-2272-8

}}

• {{cite book |author1-link=Michael Barr (mathematician) |author2-link=Charles Wells (mathematician) |last1=Barr |first1=M. |last2=Wells |first2=C. |title=Category Theory for Computing Science |publisher=Prentice Hall |edition=2nd |date=1996 |isbn=978-0-13-323809-9 }}
• {{cite book |author1-link=Joachim Lambek |author2-link=P.J. Scott |last1=Lambek |first1=J. |last2=Scott |first2=P.J. |title=Introduction to Higher Order Categorical Logic |publisher=Cambridge University Press |series=Cambridge studies in advanced mathematics |volume=7 |date=1988 |isbn=978-0-521-35653-4 |url={{GBurl|6PY_emBeGjUC|pg=PR5}}}}
• {{cite book |author1-link=Francis William Lawvere |author2-link=Robert Rosebrugh |last1=Lawvere |first1=F.W. |last2=Rosebrugh |first2=R. |title=Sets for Mathematics |publisher=Cambridge University Press |date=2003 |isbn=978-0-521-01060-3 |url={{GBurl|h3_7aZz9ZMoC|pg=PP1}}}}
• {{cite book |last1=Lawvere |first1=F.W. |author2-link=Stephen H. Schanuel |last2=Schanuel |first2=S.H. |title=Conceptual Mathematics: A First Introduction to Categories |publisher=Cambridge University Press |edition=2nd |date=2009 |isbn=978-1-139-64396-2 |url={{GBurl|6G0gAwAAQBAJ|pg=PR7}}}}

Seminal papers

• {{cite journal |author-link=Francis William Lawvere |first=F.W. |last=Lawvere |title=Functorial Semantics of Algebraic Theories |journal=Proceedings of the National Academy of Sciences |volume=50 |issue=5 |pages=869–872 |date=November 1963 |doi=10.1073/pnas.50.5.869 |jstor=71935 |pmid=16591125 |pmc=221940|bibcode=1963PNAS...50..869L |doi-access=free }}
• {{cite journal |author-mask=1 |first=F.W. |last=Lawvere |title=Elementary Theory of the Category of Sets |journal=Proceedings of the National Academy of Sciences |volume=52 |issue=6 |pages=1506–11 |date=December 1964 |doi=10.1073/pnas.52.6.1506 |jstor=72513 |pmid=16591243 |pmc=300477|bibcode=1964PNAS...52.1506L |doi-access=free }}
• {{cite book |author-mask=1 |first=F. William |last=Lawvere |chapter=Quantifiers and Sheaves |chapter-url= |title=Actes : Du Congres International Des Mathematiciens Nice 1-10 Septembre 1970. Pub. Sous La Direction Du Comite D'organisation Du Congres |publisher=Gauthier-Villars |oclc=217031451 |date=1971 |isbn= |pages=1506–11 |zbl=0261.18010}}

{{refend}}

{{refbegin}}

• {{cite book |author1-link=Michael Makkai |first1=Michael |last1=Makkai |first2=Gonzalo E. |last2=Reyes |title=First Order Categorical Logic |publisher=Springer |date=1977 |isbn=978-3-540-08439-6 |doi=10.1007/BFb0066201 |url=https://link.springer.com/book/10.1007/BFb0066201 |series=Lecture Notes in Mathematics |volume=611}}
• {{cite book |last1=Lambek |first1=J. |last2=Scott |first2=P.J. |title=Introduction to Higher Order Categorical Logic |publisher=Cambridge University Press |series=Cambridge studies in advanced mathematics |volume=7 |date=1988 |isbn=978-0-521-35653-4 |url={{GBurl|6PY_emBeGjUC|pg=PR5}}}} 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.
• {{cite book

| first = Bart

| last = Jacobs

| title = Categorical Logic and Type Theory

| year = 1999

| publisher = North Holland, Elsevier

| isbn = 0-444-50170-3

| series = Studies in Logic and the Foundations of Mathematics |volume=141

| url = https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html }} 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.

• {{cite book |author-link=John Lane Bell |first=John Lane |last=Bell |chapter=The Development of Categorical Logic |chapter-url={{GBurl|yObMqG9EcCEC|p=279}} |editor1-first=D.M. |editor1-last=Gabbay |editor2-first=Franz |editor2-last=Guenthner |title=Handbook of Philosophical Logic |publisher=Springer |volume=12|edition=2nd |date=2001 |isbn=978-1-4020-3091-8 |pages=279–361 |url=}} Version available [http://publish.uwo.ca/~jbell/catlogprime.pdf online] at [http://publish.uwo.ca/~jbell/ John Bell's homepage.]
• {{cite book |first1=Jean-Pierre |last1=Marquis |first2=Gonzalo E. |last2=Reyes |chapter=The History of Categorical Logic 1963–1977 |chapter-url={{GBurl|ZF_QckMFy-oC|p=689}} |title={{harvnb|Gabbay|Kanamori|Woods|2012}} |pages=689–800}}
  A preliminary [http://www.webdepot.umontreal.ca/Usagers/marquisj/MonDepotPublic/HistofCatLog.pdf version].
• {{cite web |author-link=Steve Awodey |first=Steve |last=Awodey |title=Categorical Logic |date= 12 July 2024|work=lecture notes |publisher= |url=https://awodey.github.io/catlog/notes/ }}
• {{cite web |author-link=Jacob Lurie |first=Jacob |last=Lurie |title=Categorical Logic (278x) |date= |work=lecture notes |publisher= |url=http://www.math.harvard.edu/~lurie/278x.html }}

{{refend}}

Category:Systems of formal logic

Category:Theoretical computer science