This article is about mathematical logic in the context of category theory. For Aristotle's system of logic, see
term 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 categoryC 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.[2]
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
intuitionistichigher-order logic in a topos enables one to reason about the objects and morphisms of a topos as if they were sets and functions.[3] 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.
— (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.
OCLC217031451.
Zbl0261.18010.
Lambek, J.; Scott, P.J. (1988).
Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics. Vol. 7. Cambridge University Press.
ISBN978-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.
ISBN0-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 category as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types.
This article is about mathematical logic in the context of category theory. For Aristotle's system of logic, see
term 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 categoryC 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.[2]
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
intuitionistichigher-order logic in a topos enables one to reason about the objects and morphisms of a topos as if they were sets and functions.[3] 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.
— (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.
OCLC217031451.
Zbl0261.18010.
Lambek, J.; Scott, P.J. (1988).
Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics. Vol. 7. Cambridge University Press.
ISBN978-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.
ISBN0-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 category as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types.