Lecture
Categorical logic — is a branch of mathematics in which the tools and concepts of category theory are applied to the study of mathematical logic. It is also notable for its connections with theoretical computer science. Broadly speaking, categorical logic represents both syntax and semantics by means of a category , and interpretation — by means of a functor . Categorical structure provides a rich conceptual framework for logical and type-theoretic constructions. In these terms the subject has been recognizable since around 1970.
Fig. Adjunction between two functors , explicitly defined by their hom-sets. Adjunction — is one of the fundamental notions of categorical logic and of category theory as a whole.
In the categorical approach to logic there are three important themes:
Categorical logic introduces the notion of a structure evaluated in a category C, with the classical model-theoretic notion of structure appearing as the special case where C — is the category of sets and functions . This notion has proven useful when the set-theoretic notion of a model is insufficiently general and/or inconvenient. The modeling of various impredicative theories, such as System F , carried out by R. A. G. Seely , serves as an example of the usefulness of categorical semantics.
It has been found that the connectives of pre-categorical logic are more clearly understood using the concept of an adjoint functor , and that quantifiers are also best understood using adjoint functors.
This can be viewed as a formalization and generalization of proof by diagram chasing . A suitable internal language is defined, naming the corresponding constituents of the category, and categorical semantics is then applied to translate statements in the logic over the internal language into corresponding categorical statements. This has been most successful in topos theory , where the internal language of a topos together with the semantics of intuitionistic higher-order logic in the topos allows one to reason about the objects and morphisms of the topos as if they were sets and functions. This has been successful when dealing with toposes that have «sets» with properties incompatible with classical logic . A striking example is Dana Scott's model of the untyped lambda calculus in terms of objects that fold into their own function space . Another is the Moggi–Hyland model of System F by means of an internal full subcategory of Martin Hyland's effective topos .
In many cases the categorical semantics of a logic serves as the basis for establishing a correspondence between theories in the logic and instances of the corresponding type of category. The classical example is the correspondence between theories of βη-equational logic over the simply typed lambda calculus and cartesian closed categories . Categories arising from theories by means of term-model constructions can usually be characterized up to equivalence by a suitable universal property . This has made it possible to prove metatheoretic properties of certain logics with the aid of a suitable categorical algebra . For example, Freyd in this way proved the disjunction and existence properties of intuitionistic logic .
These three themes are interconnected. The categorical semantics of a logic consists in describing a category of structured categories, which is related to the category of theories in that logic by way of an adjunction, where the two functors in the adjunction give, on the one hand, the internal language of a structured category, and on the other — the term model of a theory.
Categorical logic originates in the works of William Lawvere « Functorial Semantics of Algebraic Theories» (1963) and «An Elementary Theory of the Category of Sets»(1964) . Lawvere recognized the Grothendieck topos , introduced in algebraic topology as a generalized space, as a generalization of the category of sets ( Quantifiers and Sheaves (1970)) . Lawvere then, together with Myles Tierney , developed the notion of an elementary topos, thereby stabilizing 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. André Joyal is credited, in terms of Kripke–Joyal semantics, with the observation that the models of connectives for predicate logic provided by topos theory generalize Kripke semantics . Joyal and others applied these models to the study of higher-order notions, such as real numbers, in intuitionistic forms.
A similar development was the connection between the simply typed lambda calculus and cartesian closed categories (Lawvere, Lambek, Scott), which created an environment for the development of domain theory . Less expressive theories, from the point of view of mathematical logic, have their own analogues in category theory . For example, the concept of an algebraic theory leads to Gabriel–Ulmer duality . The view of categories as a generalization unifying syntax and semantics has proven productive in the study of logic and theories for applications in computer science .
The founders of the elementary theory of toposes were Lawvere and Tierney. In his writings, Lawvere, sometimes expressed in philosophical jargon, singled out certain basic notions as adjoint functors (which he , not without justification, explained as «objective» in the Hegelian sense). The presence of a classifying subobject is a strong property required of a category, since together with cartesian closure and finite limits it yields a topos ( violation of the axiom shows just how strong this assumption is). Lawvere's further work in the 1960s led to the creation of the theory of attributes, which in a sense is a theory of subobjects more in keeping with type theory. Later on, the main influences were Martin-Löf type theory with respect to logic, type polymorphism and the calculus of constructions in the field of functional programming, linear logic in the field of proof theory, game semantics, and the synthetic theory of projectable domains. The abstract idea of a categorical fibration has found wide application.
Looking back, one can say that the greatest irony is that, generally speaking, intuitionistic logic reappeared in mathematics, taking a central place in the Bourbaki–Grothendieck program, a generation after the end of the tangled Brouwer–Hilbert controversy, in which Hilbert turned out to be the apparent victor. Bourbaki, or more precisely Jean Dieudonné, laying claim to the legacy of Hilbert and the Göttingen school, including Emmy Noether, revived confidence in intuitionistic logic (although Dieudonné himself considered intuitionistic logic absurd) as the logic of an arbitrary topos, in which classical logic was the «topos» of sets. This consequence was certainly unexpected from Grothendieck's relative point of view; and it did not escape the notice of Pierre Cartier, one of the most influential figures of the French core of mathematicians surrounding Bourbaki and the IHES. It was Cartier who gave the account of the Bourbaki seminar on intuitionistic logic.
From an even broader point of view, category theory can be considered the mathematics of the second half of the 20th century in the same way that measure theory was for the first half. It was Kolmogorov who applied measure theory to probability theory, proposing the first convincing (if not the only) axiomatic approach. Kolmogorov was also one of the pioneers in the early 1920s, formulating intuitionistic logic in a style fully supported by the later category-logical approach (again, one of the formulations, not the only one; Stephen Kleene's concept of realizability is also a serious candidate). Another path to categorical logic thus ran through Kolmogorov, and this is one way of explaining the Curry–Howard variable isomorphism.
Comments