__NOTOC__
Categorical logic is the branch of
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
in which tools and concepts from
category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
are applied to the study of
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
. It is also notable for its connections to
theoretical computer science
Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumsc ...
.
In broad terms, categorical logic represents both syntax and semantics by a
category
Category, plural categories, may refer to:
Philosophy and general uses
* Categorization, categories in cognitive science, information science and generally
*Category of being
* ''Categories'' (Aristotle)
*Category (Kant)
*Categories (Peirce)
* ...
, and an
interpretation by a
functor
In mathematics, specifically category theory, a functor is a Map (mathematics), mapping between Category (mathematics), categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) ar ...
. The categorical framework provides a rich conceptual background for logical and
type-theoretic
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
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 category'' C with the classical
model theoretic
In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the st ...
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
In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
theories, such as
system F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphis ...
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
350px, The commutative diagram used in the proof of the five lemma.
In mathematics, and especially in category theory, a commutative diagram is a diagram such that all directed paths in the diagram with the same start and endpoints lead to th ...
. 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
In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion ...
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". This has been successful in dealing with toposes that have "sets" with properties incompatible with classical logic. A prime example is
Dana Scott
Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
's model of
untyped lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
in terms of objects that retract onto their own function space. Another is the Moggi–Hyland model of
system F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphis ...
by an internal
full subcategory
In mathematics, specifically category theory, a subcategory of a category ''C'' is a category ''S'' whose objects are objects in ''C'' and whose morphisms are morphisms in ''C'' with the same identities and composition of morphisms. Intuitively, ...
of the
effective topos In mathematics, the effective topos is a topos
In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much ...
of
Martin Hyland
(John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science.
Education
Hy ...
.
;Term-model constructions: In many cases, the categorical semantics of a logic provide a basis for establishing a correspondence between
theories
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be s ...
in the logic and instances of an appropriate kind of category. A classic example is the correspondence between theories of
βη-
equational logic First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into universal algebra by Birkhoff, Grätzer, and Cohn. It was l ...
over
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda cal ...
and
Cartesian closed categories
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in ma ...
. Categories arising from theories via term-model constructions can usually be characterized up to
equivalence
Equivalence or Equivalent may refer to:
Arts and entertainment
*Album-equivalent unit, a measurement unit in the music industry
*Equivalence class (music)
*''Equivalent VIII'', or ''The Bricks'', a minimalist sculpture by Carl Andre
*'' Equival ...
by a suitable
universal property
In mathematics, more specifically in category theory, a universal property is a property that characterizes up to an isomorphism the result of some constructions. Thus, universal properties can be used for defining some objects independently fro ...
. This has enabled proofs of
meta-theoretical properties of some logics by means of an appropriate
categorical algebra
In mathematics, especially ( higher) category theory, higher-dimensional algebra is the study of categorified structures. It has applications in nonabelian algebraic topology, and generalizes abstract algebra.
Higher-dimensional categories
A f ...
. For instance,
Freyd gave a proof of the existence and disjunction properties of
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
this way.
See also
*
History of topos theory
This article gives some very general background to the mathematical idea of topos. This is an aspect of category theory, and has a reputation for being abstruse. The level of abstraction involved cannot be reduced beyond a certain point; but on the ...
Notes
References
;Books
*
*
*
*
*
*
*
Seminal papers
*
*
*
Further reading
*
* 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.
* 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
Fibred categories (or fibered categories) are abstract entities in mathematics used to provide a general framework for descent theory. They formalise the various situations in geometry and algebra in which ''inverse images'' (or ''pull-backs'') of ...
as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types.
* Version availabl
onlinea
John Bell's homepage.*
A preliminar
version
External links
*
*{{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
Systems of formal logic
Theoretical computer science