Mathematical Logic: Proof Theory, Constructive Mathematics

Abstract

The workshop Mathematical Logic: Proof Theory, Constructive Mathematics was held April 6-12, 2008 and had the following main aims:

To promote the interaction of proof theory with core areas of mathematics. This, in particular, refers to uses of proof theoretic techniques (most notably various forms of functional and realizability interpretations) to unwind prima facie ineffective proofs in mathematics. For instance a number of talks presented such applications in the areas of fixed point theory, ergodic theory, topological dynamics and symbolic dynamics resulting in new theorems, surprising to the experts in the respective fields (Avigad, Briseid, Gerhardy, Leuştean, Simpson). Another talk addressed uses of analytic number theory in connection with new unprovability results and phase transitions in provability (Bovykin).

To further develop new directions in both the foundations as well as applied forms of constructive mathematics. There were a number of talks focusing on new formal frameworks for constructive mathematics and their proof theoretic properties (Aczel, Iemhoff, J. Moschovakis, Palmgren, Streicher), but also new constructive (and partly computer generated) developments in specific areas such as algebra, analysis, combinatorics and quantum theory (Bauer, Delzell, Lombardi, Paule, Spitters).

To explore further the connections between proof theory and computational complexity (e.g. in connection with the study of systems of so-called bounded arithmetic, Beckmann, Pollett, Thapen). Another topic in this area was the study of implicit computational complexity and the design of functional programming languages corresponding to specific complexity classes (Aehlig, Hofmann, Matthes). Yet another approach to the issue of the intrinsic complexity for general classes of algorithmic problems was developed in a talk by Y. Moschovakis.

In order to provide the participants with an overview over new developments in the study of functional and realizability interpretations (as mentioned above) two invited lecture series were given.

The first one (given by Fernando Ferreira and Paulo Oliva) focussed on novel (so-called monotone and bounded) variants of Gödel's functional interpretation (first published exactly 50 years ago) and its decomposition into an interpretation of linear logic combined with Girard's embedding of intuitionistic logic into linear logic. The second course was delivered by Ulrich Berger and presented a number of proof theoretic approaches for analyzing proofs based on dependent choice (such as Spector's bar recursive solution, the realizability solution by modified bar recursion due to Berger and Oliva and a novel approach based on open induction and its relation to previous work by Berardi, Bezem and Coquand). Moreover, Berger reported on recent experiments (with Schwichtenberg) concerning the automated extraction (based on the MinLog tool) of efficient algorithms from proofs in constructive analysis.