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