Home > Categorical logic
Categorical logic is a branch of category theory within mathematics, adjacent to mathematical logic but in fact more notable for its connections to theoretical computer science. In broad terms, it is a theory about the transition from a type theory, understood to be within an intuitionistic logic or constructive mathematics setting, to a category, by means of a translation that respects both the syntax and the intended computational meaning of type-theoretic constructions. The subject has been recognisable in these terms since about 1970, when the needs of domain theory started to call on category theory. The earlier history is relatively complex, and contains some ironies.Categorical logic originated within sheaf theory, as a suitable version of Kripke semantics one can say with hindsight, and emerged as a theory with a character of its own only in shedding the necessary connection with sheaves. This can be traced in a number of stages, from 1960 onwards: the formulation of the Grothendieck topos, and then of the elementary topos, giving rise first to topos theory. Topos theory, as would now be understood, is the intuitionistic replacement for set theorySet theory is the mathematical theory of sets, which represent collections of abstract objects. It has a central role in modern mathematical theory, providing the basic language in which most of mathematics is expressed. For more information on set theory. In particular, where L. E. J. Brouwer laboured hard to construct a theory of ' species ', which were to be the real numberIn mathematics, the real numbers are intuitively defined as numbers that are in one-to-one correspondence with the points on an infinite line—the number line. The term "real number" is a retronym coined in response to " imaginary number". Real numbers mays in the intuitionistic setting, there is a theory of real numbers in each topos (which contradicts the idea that there is a single, correct concept). Computationally speaking, real numbers are anyway an idealisation of what one carries out in an actual calculation. Set theory is a universal container for mathematical concepts, but rather a large, baggy syntax if one wants to express computation. Computer science, on the other hand, by intention rations and constrains computations. Less expressive theories, from the mathematical logic viewpoint, have lower-level category theory counterparts. For example the concept of an algebraic theory leads to Gabriel-Ulmer duality .
Actual computation needs recursionIn mathematics and computer science, recursion is a particular way of specifying (or constructing) a class of objects (or an object from a certain class) with the help of a reference to other objects of the class: a recursive definition defines objects in, something isolated in category theory as a natural number objectIn category theory, a natural number object (nno) is an object endowed with a recursive structure similar to natural numbers. More precisely, in a category E with a terminal object (alternately, a topos), an nno N is given by: # a global element z : 1 N a (this corresponds to a minimal theory of recursion). On the other hand functional programmingFunctional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. In contrast to imperative programming, functional programming emphasizes the evaluation of functional expressions, rather than execution is the cleanest model of computation ( computational paradigm ) and was realised to match up with the cartesian closed categoryIn 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 mathematica concept.
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, 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 Seminaire 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
Mathematical logic
Theoretical computer science
Categorical logic
