Editing Categorical logic (section)

== 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.