Carnegie Mellon University
Categorical Logic

Categorical Logic

Categorical logic is a relatively new field arising from the application of the mathematical theory of categories to logic and theoretical computer science. Category theory consists of a characteristic language and collection of methods and results that have become common-place in many mathematics-based disciplines. It is a branch of abstract algebra invented in the tradition of Felix Klein's Erlanger Programm as a way of studying different kinds of mathematical structures in terms of their "admissible transformations". The general notion of a category provides an axiomatization of the notion of a "structure-preserving transformation", and thereby of a species of structure admitting such transformations. As an abstract theory of mappings, with such great generality, it is not surprising that category theory should have wide-spread applications in many types of foundational work.

The applications of category theory in logic often involve the use of topology, sheaf theory, and other ideas imported from geometry, particularly in constructing models. This occurs, for example, in domain theory or topos theory. But as in algebraic topology, where category theory was first invented, extensive use is also made of algebraic techniques, for example in the treatment of logical theories as "generalized algebras". In this way, categorical logic typically treats the classical, logical notions of semantics as "geometry" and syntax as a kind of "algebra", to which general category theory can then be applied, in order to study the connections between the two.

The department's research activities in this area are conducted mainly by Steve Awodey and his graduate students. Emeritus faculty member Dana S. Scott's past and current work in this area has also been very influential. Awodey's current research is mainly concerned homotopy type theory and univalent foundations, a field of which he is one of hte cofounders. This currently very active research program is centerd on developing new foundations of mathematics that will be well-suited to formalization and verification by computerised proof systems. The system of foundations used has intrinsic geometric content, provided by an interpretation into homotopy theory. Awodey also uses category theory and topos theory to investigate various other systems of logic, set theory, and type theory.

Current research in categorical logic by Awodey is centered on the Homotopy Type Theory project. Also see the Project on Logics of Types and Computation and the Algebraic Set Theory project.