Categorical Logic - Overview

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 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.
• 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 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'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.
• Term-model constructions. In many cases, the categorical semantics of a logic provide a basis for establishing a correspondence between theories in the logic and instances of an appropriate kind of category. A classic example is the correspondence between theories of βη-equational logic over simply typed lambda calculus and cartesian closed categories. Categories arising from theories via term-model constructions can usually be characterized up to equivalence by a suitable universal property. This has enabled proofs of meta-theoretical properties of some logics by means of an appropriate categorical algebra. For instance, Freyd gave a proof of the existence and disjunction properties of intuitionistic logic this way.