Categorical logic
Encyclopedia
Categorical logic is a branch of category theory
within mathematics
, adjacent to mathematical logic
but more notable for its connections to theoretical computer science
. 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.
's Functorial Semantics of Algebraic Theories (1963), and Elementary Theory of the Category of Sets (1964). Lawvere recognised the Grothendieck topos, introduced in algebraic topology as a generalised space, as a generalisation of the category of sets (Quantifiers and Sheaves (1970)). With Myles Tierney, Lawvere then developed the notion of elementary topos, thus establishing the fruitful field of topos theory, which provides a unified categorical treatment of the syntax and semantics of higher-order predicate logic. The resulting logic is formally intuitionistic. Andre Joyal is credited, in the term Kripke–Joyal semantics, with the observation that the sheaf models for predicate logic, provided by topos theory, generalise Kripke semantics
. Joyal and others applied these models to study higher-order concepts such as the real number
s in the intuitionistic setting.
An analogous development was the link between the simply typed lambda calculus
and cartesian-closed categories
(Lawvere, Lambek, Scott), which provided a setting for the development of domain theory
.
Less expressive theories, from the mathematical logic viewpoint, have their own category theory counterparts. For example the concept of an algebraic theory
leads to Gabriel–Ulmer duality. The view of categories as a generalisation unifying syntax and semantics has been productive in the study of logics and type theories for applications in computer science.
The founders of elementary topos theory were Lawvere and Tierney. Lawvere's writings, sometimes couched in a philosophical jargon, isolated some of the basic concepts as adjoint functors
(which he explained as 'objective' in a Hegelian sense, not without some justification). A subobject classifier
is a strong property to ask of a category, since with cartesian closure and finite limit
s it gives a topos (axiom bashing shows how strong the assumption is). Lawvere's further work in the 1960s gave a theory of attributes, which in a sense is a subobject
theory more in sympathy with type theory. Major influences subsequently have been Martin-Löf type theory
from the direction of logic, type polymorphism
and the calculus of constructions
from functional programming, linear logic
from proof theory
, game semantics
and the projected synthetic domain theory. The abstract categorical idea of fibration
has been much applied.
To go back historically, the major irony here is that in large-scale terms, intuitionistic logic
had reappeared in mathematics, in a central place in the Bourbaki
–Grothendieck
program, a generation after the messy Hilbert
–Brouwer
controversy had ended, with Hilbert the apparent winner. Bourbaki, or more accurately Jean Dieudonné
, having laid claim to the legacy of Hilbert and the Göttingen school including Emmy Noether
, had revived intuitionistic logic's credibility (although Dieudonné himself found Intuitionistic Logic ludicrous), as the logic of an arbitrary topos, where classical logic was that of 'the' topos of sets. This was one consequence, certainly unanticipated, of Grothendieck's relative point of view
; and not lost on Pierre Cartier
, one of the broadest of the core group of French mathematicians around Bourbaki and IHES. Cartier was to give a Séminaire Bourbaki exposition of intuitionistic logic.
In an even broader perspective, one might take category theory to be to the mathematics of the second half of the twentieth century, what measure theory was to the first half. It was Kolmogorov who applied measure theory to probability theory
, the first convincing (if not the only) axiomatic approach. Kolmogorov was also a pioneer writer in the early 1920s on the formulation of intuitionistic logic, in a style entirely supported by the later categorical logic approach (again, one of the formulations, not the only one; the realizability
concept of Stephen Kleene is also a serious contender here). Another route to categorical logic would therefore have been through Kolmogorov, and this is one way to explain the protean Curry–Howard isomorphism
.
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
within mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, adjacent to mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
but more notable for its connections to theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
. In broad terms, categorical logic represents both syntax and semantics by a category
Category (mathematics)
In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
, and an interpretation
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
by a functor
Functor
In category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
. 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 category C with the classical model theoreticModel theoryIn mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
notion of a structure appearing in the particular case where C is the category of sets and functionsCategory of setsIn the mathematical field of category theory, the category of sets, denoted as Set, is the category whose objects are sets. The arrows or morphisms between sets A and B are all functions from A to B...
. 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 impredicativeImpredicativeIn mathematics and logic, impredicativity is the property of a self-referencing definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined.Russell's paradox is a famous example of an impredicative...
theories, such as system FSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
is an example of the usefulness of categorical semantics. - 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 toposToposIn mathematics, a topos is a type of category that behaves like the category of sheaves of sets on a topological space...
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 ScottDana ScottDana Stewart Scott 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, California...
'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 FSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
by an internal full subcategory of the effective toposEffective toposIn mathematics, the effective topos is a topos introduced by , based on Kleene's notion of recursive realizability, that captures the idea of effectivity in mathematics....
of Martin HylandMartin HylandJohn Martin Elliott Hyland is professor of mathematics at King's College in the University of Cambridge, England where he is currently head of the Department of Pure Mathematics and Mathematical Statistics...
. - Term-model constructions. In many cases, the categorical semantics of a logic provide a basis for establishing a correspondence between theoriesTheory (mathematical logic)In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
in the logic and instances of an appropriate kind of category. A classic example is the correspondence between theories of βη-equational logicEquational logicFirst-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 et al. [Birkhoff, Gratzer, Cohn]...
over simply typed lambda calculusSimply typed lambda calculusThe simply typed lambda calculus , a formof 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 calculus...
and cartesian closed categories. Categories arising from theories via term-model constructions can usually be characterized up to equivalenceEquivalence of categoriesIn category theory, an abstract branch of mathematics, an equivalence of categories is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics...
by a suitable universal propertyUniversal propertyIn various branches of mathematics, a useful construction is often viewed as the “most efficient solution” to a certain problem. The definition of a universal property uses the language of category theory to make this notion precise and to study it abstractly.This article gives a general treatment...
. This has enabled proofs of meta-theoreticalMetalogicMetalogic is the study of the metatheory of logic. While logic is the study of the manner in which logical systems can be used to decide the correctness of arguments, metalogic studies the properties of the logical systems themselves...
properties of some logics by means of an appropriate categorical algebra. For instance, FreydPeter J. FreydPeter J. Freyd is an American mathematician, a professor at the University of Pennsylvania, known for work in category theory and for founding the False Memory Syndrome Foundation.- Mathematical work :...
gave a proof of the existence and disjunction properties of intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
this way.
Historical perspective
Categorical logic originated with Bill LawvereWilliam Lawvere
Francis William Lawvere is a mathematician known for his work in category theory, topos theory and the philosophy of mathematics.-Biography:...
's Functorial Semantics of Algebraic Theories (1963), and Elementary Theory of the Category of Sets (1964). Lawvere recognised the Grothendieck topos, introduced in algebraic topology as a generalised space, as a generalisation of the category of sets (Quantifiers and Sheaves (1970)). With Myles Tierney, Lawvere then developed the notion of elementary topos, thus establishing the fruitful field of topos theory, which provides a unified categorical treatment of the syntax and semantics of higher-order predicate logic. The resulting logic is formally intuitionistic. Andre Joyal is credited, in the term Kripke–Joyal semantics, with the observation that the sheaf models for predicate logic, provided by topos theory, generalise Kripke semantics
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
. Joyal and others applied these models to study higher-order concepts such as the real number
Real number
In mathematics, a real number is a value that represents a quantity along a continuum, such as -5 , 4/3 , 8.6 , √2 and π...
s in the intuitionistic setting.
An analogous development was the link between the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof 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 calculus...
and cartesian-closed categories
Cartesian closed category
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 mathematical logic and the theory of programming, in...
(Lawvere, Lambek, Scott), which provided a setting for the development of domain theory
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
.
Less expressive theories, from the mathematical logic viewpoint, have their own category theory counterparts. For example the concept of an algebraic theory
Algebraic theory
In mathematical logic, an algebraic theory is one that uses axioms stated entirely in terms of equations between terms with free variables. Inequalities and quantifiers are specifically disallowed. Sentential logic is the subset of first-order logic involving only algebraic sentences.Saying that...
leads to Gabriel–Ulmer duality. The view of categories as a generalisation unifying syntax and semantics has been productive in the study of logics and type theories for applications in computer science.
The founders of elementary topos theory were Lawvere and Tierney. Lawvere's writings, sometimes couched in a philosophical jargon, isolated some of the basic concepts as adjoint functors
Adjoint functors
In mathematics, adjoint functors are pairs of functors which stand in a particular relationship with one another, called an adjunction. The relationship of adjunction is ubiquitous in mathematics, as it rigorously reflects the intuitive notions of optimization and efficiency...
(which he explained as 'objective' in a Hegelian sense, not without some justification). A subobject classifier
Subobject classifier
In category theory, a subobject classifier is a special object Ω of a category; intuitively, the subobjects of an object X correspond to the morphisms from X to Ω. As the name suggests, what a subobject classifier does is to identify/classify subobjects of a given object according to which elements...
is a strong property to ask of a category, since with cartesian closure and finite limit
Limit (category theory)
In category theory, a branch of mathematics, the abstract notion of a limit captures the essential properties of universal constructions such as products and inverse limits....
s it gives a topos (axiom bashing shows how strong the assumption is). Lawvere's further work in the 1960s gave a theory of attributes, which in a sense is a subobject
Subobject
In category theory, a branch of mathematics, a subobject is, roughly speaking, an object which sits inside another object in the same category. The notion is a generalization of the older concepts of subset from set theory and subgroup from group theory...
theory more in sympathy with type theory. Major influences subsequently have been Martin-Löf type theory
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
from the direction of logic, type polymorphism
Type polymorphism
In computer science, polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface. The concept of parametric polymorphism applies to both data types and functions...
and the calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
from functional programming, linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
from proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, game semantics
Game semantics
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
and the projected synthetic domain theory. The abstract categorical idea of fibration
Fibred category
Fibred 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 of objects such as vector bundles can be defined...
has been much applied.
To go back historically, the major irony here is that in large-scale terms, intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
had reappeared in mathematics, in a central place in the Bourbaki
Nicolas Bourbaki
Nicolas Bourbaki is the collective pseudonym under which a group of 20th-century mathematicians wrote a series of books presenting an exposition of modern advanced mathematics, beginning in 1935. With the goal of founding all of mathematics on set theory, the group strove for rigour and generality...
–Grothendieck
Alexander Grothendieck
Alexander Grothendieck is a mathematician and the central figure behind the creation of the modern theory of algebraic geometry. His research program vastly extended the scope of the field, incorporating major elements of commutative algebra, homological algebra, sheaf theory, and category theory...
program, a generation after the messy Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
–Brouwer
Luitzen Egbertus Jan Brouwer
Luitzen Egbertus Jan Brouwer FRS , usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, a graduate of the University of Amsterdam, who worked in topology, set theory, measure theory and complex analysis.-Biography:Early in his career,...
controversy had ended, with Hilbert the apparent winner. Bourbaki, or more accurately Jean Dieudonné
Jean Dieudonné
Jean Alexandre Eugène Dieudonné was a French mathematician, notable for research in abstract algebra and functional analysis, for close involvement with the Nicolas Bourbaki pseudonymous group and the Éléments de géométrie algébrique project of Alexander Grothendieck, and as a historian of...
, having laid claim to the legacy of Hilbert and the Göttingen school including Emmy Noether
Emmy Noether
Amalie Emmy Noether was an influential German mathematician known for her groundbreaking contributions to abstract algebra and theoretical physics. Described by David Hilbert, Albert Einstein and others as the most important woman in the history of mathematics, she revolutionized the theories of...
, had revived intuitionistic logic's credibility (although Dieudonné himself found Intuitionistic Logic ludicrous), as the logic of an arbitrary topos, where classical logic was that of 'the' topos of sets. This was one consequence, certainly unanticipated, of Grothendieck's relative point of view
Grothendieck's relative point of view
Grothendieck's relative point of view is a heuristic applied in certain abstract mathematical situations, with a rough meaning of taking for consideration families of 'objects' explicitly depending on parameters, as the basic field of study, rather than a single such object...
; and not lost on Pierre Cartier
Pierre Cartier (mathematician)
Pierre Cartier is a mathematician. An associate of the Bourbaki group and at one time a colleague of Alexander Grothendieck, his interests have ranged over algebraic geometry, representation theory, mathematical physics, and category theory....
, one of the broadest of the core group of French mathematicians around Bourbaki and IHES. Cartier was to give a Séminaire Bourbaki exposition of intuitionistic logic.
In an even broader perspective, one might take category theory to be to the mathematics of the second half of the twentieth century, what measure theory was to the first half. It was Kolmogorov who applied measure theory to probability theory
Probability theory
Probability theory is the branch of mathematics concerned with analysis of random phenomena. The central objects of probability theory are random variables, stochastic processes, and events: mathematical abstractions of non-deterministic events or measured quantities that may either be single...
, the first convincing (if not the only) axiomatic approach. Kolmogorov was also a pioneer writer in the early 1920s on the formulation of intuitionistic logic, in a style entirely supported by the later categorical logic approach (again, one of the formulations, not the only one; the realizability
Realizability
Realizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
concept of Stephen Kleene is also a serious contender here). Another route to categorical logic would therefore have been through Kolmogorov, and this is one way to explain the protean Curry–Howard isomorphism
Curry–Howard
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and proofs...
.
Further reading
- Michael MakkaiMichael MakkaiMichael Makkai is a Canadian mathematician, specializing in mathematical logic. He works in model theory, category theory, algebraic logic, and in the theory of topoi. He graduated from the Eötvös Loránd University, Budapest, then worked at the Mathematical Institute of the Hungarian Academy of...
and Gonzalo E. Reyes, 1977, First order categorical logic - Lambek, J.Joachim LambekJoachim Lambek is Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Julius Zassenhaus as advisor. He is called Jim by his friends.- Scholarly work :...
and Scott, P. J., 1986. Introduction to Higher OrderHigher-order logicIn mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
Categorical Logic. 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 categoryFibred categoryFibred 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 of objects such as vector bundles can be defined...
as universal tool in categorical logic, which is necessary in dealing with polymorphic and dependent types. According to P.T. Johnstone, this approach is unwieldy for simple types. - P.T. Johnstone, 2002, Sketches of an Elephant, part D (vol 2) covers both first-order and higher-order logics, but not dependent or polymorphic types, considered by the author of interest mainly to computer science. Because it avoids polymorphic and dependent types, the categorical approach is easier to present in therms of a syntactic categorySyntactic categoryA syntactic category is either a phrasal category, such as noun phrase or verb phrase, which can be decomposed into smaller syntactic categories, or a lexical category, such as noun or verb, which cannot be further decomposed....
just as in Lambek's book, but Sketches includes more recent developments, like .
- John Lane BellJohn Lane BellJohn Bell is Professor of Philosophy at the University of Western Ontario in Canada. He is an outstanding figure in mathematical logic and philosophy...
(2005) The Development of Categorical Logic. Handbook of Philosophical Logic, Volume 12. Springer. Version available online at John Bell's homepage.
- Jean-Pierre Marquis and Gonzalo E. Reyes (2009). The History of Categorical Logic 1963–1977.http://www.webdepot.umontreal.ca/Usagers/marquisj/MonDepotPublic/HistofCatLog.pdf
External links
- Categorical Logic lecture notes by Steve Awodey