Research Areas
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 by Dana S. Scott and Steve Awodey (and their recent graduate students). Scott's (past and) current work in categorical logic falls roughly into three main areas: semantics for lambda-calculi and type theories, topos models of (intuitionistic) set theory, and the category-theoretic treatment of realizability semantics. In each of these areas, his work forms the basis of currently active research of central importance to categorical logic. Awodey's research is mainly concerned with using topos theory to investigate various systems of logic, set theory, and type theory. Using the same methods, he has begun working on realizability in collaboration with Scott.
Current research in categorical logic by Scott and Awodey is centered on the Project on Logics of Types and Computation and the Algebraic Set Theory project.