Editing Categorical logic

{{Short description|Branch of logic using category theory to study mathematical structures}}
{{About|mathematical logic in the context of category theory|Aristotle's system of logic|term logic}}
__NOTOC__
'''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]].<ref>
{{cite journal |first1=Joseph |last1=Goguen |first2=Till |last2=Mossakowski |first3=Valeria |last3=de Paiva |first4=Florian |last4=Rabe |first5=Lutz |last5=Schroder |title=An Institutional View on Categorical Logic |journal=[[International Journal of Software and Informatics]] |volume=1 |issue=1 |pages=129–152 |date=2007 |doi= |citeseerx=10.1.1.126.2361 |url=https://kwarc.info/people/frabe/Research/GMPRS_catlog_07.pdf}}</ref> 
In broad terms, categorical logic represents both syntax and semantics by a [[category (mathematics)|category]], and an [[Interpretation (logic)|interpretation]] by a [[functor]].  The categorical framework provides a rich conceptual background for logical and [[type theory|type-theoretic]] constructions. The subject has been recognisable in these terms since around 1970.

== Overview ==

There are three important<!--to computer science --> 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 theory|model theoretic]] notion of a structure appearing in the particular case where '''C''' is the [[Category of sets|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 [[logical connective|connective]]s of pre-categorical logic were more clearly understood using the concept of [[adjoint functor]], and that the [[quantifier (logic)|quantifier]]s were also best understood using adjoint functors.<ref>{{harvnb|Lawvere|1971|loc=Quantifiers and Sheaves}}</ref>

;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 [[topos]]es, 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.<ref>{{harvnb|Aluffi|2009}}</ref> 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 [[section (category theory)|retract]] onto their own [[function space]]. Another is the [[Eugenio Moggi|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 [[Theory (mathematical logic)|theories]] in the logic and instances of an appropriate kind of category. A classic example is the correspondence between theories of [[beta reduction|βη]]-[[equational logic]] over [[simply typed lambda calculus]] and [[Cartesian closed category|Cartesian closed categories]]. Categories arising from theories via term model constructions can usually be characterized up to [[Equivalence of categories|equivalence]] by a suitable [[universal property]]. This has enabled proofs of [[Metalogic|meta-theoretical]] properties of some logics by means of an appropriate [[:Category:monoidal categories|categorical algebra]]<!--no good article-->. For instance, [[Peter J. Freyd|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==
* [[History of topos theory]]
* [[Coherent topos]]
{{Portal|Mathematics}}

== Notes ==
{{reflist}}

==References==
;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}}  <!-- [[Francis William Lawvere|Lawvere, F.W.]], ''Quantifiers and Sheaves''. In ''Proceedings of the International Congress on Mathematics (Nice 1970)'', Gauthier-Villars (1971) 329–334.  (Guessing same as above in the English title volume (3-vols), haven't found in WorldCat) -->
{{refend}}

== Further reading ==
{{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}}<br/>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:Categorical logic| ]]
[[Category:Systems of formal logic]]
[[Category:Theoretical computer science]]