Computational Proof Theory
This is a joint research project of the TIL group and the Department of Mathematical Logic and Theory of Algorithms in Moscow. Both groups have a strong background in mathematical logic - in particular proof theory, provability logic and general modal logics - and expertise in applying concepts and techniques of mathematical logic in connection with recent developments in (theoretical) computer science. Among the interests of both groups are the attempts to analyze existing formal systems in order to classify their expressive as well as proof-theoretic powers and to design new and more flexible formal frameworks. In doing this, interesting results about computational and logical complexities (lower and upper bounds) of algorithms developed within these frameworks can be obtained frequently. Although working towards similar aims, the research traditions of Moscow and Bern are quite distinct.
Bern’s approach is rooted in traditional Gentzen- and Schütte-style (infinitary) proof theory and the proof-theoretic analysis of subsystems of second order arithmetic, set theory, explicit mathematics and type systems and still pursuing this line. Moscow school of logic has its roots in the works of Kolmogorov, Novikov and Markov. It is traditionally strong in constructive logic and mathematics, algorithmic problems in algebra, various non-classical logics and their semantical and computational aspects, and in descriptive complexity and complexity of algorithms.
The following three research streams address topics of mutual interests:
- Provability algebras, metapredicativity and impredicativity
- Functionality and common knowledge in justification logic
- Structurally enhanced proof-theory for modal and substructural logics
It is expected that the combination and integration of the conceptual approaches and methods of both groups will allow to clarify the general landscape and to solve some long-standing open problems.
