Mathematical Logic: Proof Theory, Type Theory and Constructive Mathematics

Abstract

The workshop Mathematical Logic: Proof Theory, Type Theory and Constructive Mathematics, was held March 20th–March 26th, 2005 and had several aims.

To promote interaction between traditional proof theory and a more structural mathematical proof theory. It is hoped to encourage the application-oriented to consider their tools more abstractedly and those with foundational leaning to focus on possible applications. Questions of feasibility should play an essential role here.

To further develop constructive mathematics. For instance, there has been recent progress in designing some central notions for a constructive treatment of algebraic topology (like that of a scheme, in Peter Schuster's Habilitationsschrift 2003). An essential tool is the so-called formal or point-free topology, developed by Sambin, Coquand and others. Type theory offers some unifying concepts for a useful dicussion of the notions involved.

To explore the relevance of classical mathematics to algorithms. Recent work of Kohlenbach, Lombardi, Roy and others showed, in very different ways, that mathematical proofs that use a priory highly non computational concepts, such as Zorn's lemma or compactness principles, may contain implicitely very interesting computational information. For instance, recent work of Kohlenbach – using a modification of Gödel's Dialectica interpretation – could extract not only algorithmic information but also new theorems, surprising to the expert (here in the field of metric fixed point theory).

To understand in depth mathematical concepts in connection with algorithms and proofs, and also to further develop the notion of a certificate, aimed at unifying attempts to connect proof systems and computer algebra systems.

To develop connections between proof theory and computational complexity. Specifically to understand the connections between the complexity of formal proofs, computational complexity and descriptive complexity.

The variety of these aims is well reflected by the many talks given. As can be seen from their abstracts, presented in chronological order, they cover a broad range of topics – without losing their common theme, that is, mathematical logic and the formal reasoning about proofs and computations.

In order to provide the participants with an overview of some of the recent developments in some of the covered topics two invited lecture series were given. Both highlighted applications of proof theory to other areas of mathematics. Ulrich Kohlenbach presented proof mining as an area of applications of proof theory to analysis; Thierry Coquand's talk on infinite objects in constructive mathematics showed applications of proof theory to algebra.