Projet de Recherche — ANR Programme Blanc International 2010

STRUCTURAL — Structural and Computational Proof Theory


Overview

Proof theory is one of the central pillars of mathematical logic. In the early 20th century, Hilbert's programme proposed to establish the consistency of mathematics by finitary means. Proof-theoretic investigations in this tradition were largely concerned with questions of provability. However, it became clear that in order to answer questions about provability a more detailed study of the structure of proofs is necessary. These investigations led to the development of the field of structural proof theory that studies proofs as combinatorial objects in their own right, and is therefore concerned with questions about the form and structure of proofs. The earliest result of this field is Gentzen's seminal cut-elimination theorem that led to the construction of analytic calculi for classical and intuitionistic logics. (An analytic calculus is one where a proof uses only subformulas, in a sense adapted to the particular logical calculus, of the proved theorem.) The existence of such a calculus for a logic has many important implications, primary among them the consistency of the logic, and analyticity is indispensable for proof search.

In structural proof theory we can distinguish two traditions. The first, with mathematical roots, is concerned with first-order logic, and encompasses such methods as Herbrand's theorem, Hilbert's epsilon-calculus or Gödel's Dialectica interpretation. The other tradition derives its motivations from computer science, therefore coming later than the first tradition, and is concerned with the propositional structure of proofs. It uses methods such as the Curry-Howard isomorphism, algebraic semantics, linear logic, proof nets and deep inference. The French project partners are situated primarily in the latter tradition, and the Austrian project partners in the former tradition. The proposed project will thus play an important role in the cross-fertilization of these different subfields of structural proof theory.

In both traditions, analytic proofs and procedures for obtaining such proofs play a paramount role. The aim of the proposed project is to further deepen the understanding of the structural properties of analytic proofs. More specifically, we plan to investigate extensions of the classical notion of analyticity, by using deep-inference calculi, and by investigating analyticity-properties in non-classical logics. Furthermore, we will treat questions about the complexity of transformations between analytic and non-analytic proofs. We also plan to compare such procedures in terms of the proofs they generate.

Structural proof theory plays a crucial role in the foundations of programming language. At the propositional level, computational interpretations of propositional deduction systems provide the basic instructions of programming languages. The classic example is of intuitionistic propositional natural deduction, whose computational interpretation leads to environment machines for functional languages. Changing the logic or the deduction system changes the computational model. Several computational models have been constructed by playing with possibilities, in particular along the lines of proof nets. At the first-order level, structural proof theory is used to extract correct programs from proofs, and to extract concrete bounds from abstract mathematical proofs. One of the original elements of the present project is to connect these two lines of research, which are often kept separate.

The present project is, from the French side, a prolongation of the ANR INFER project "Theory and Application of Deep Inference" between LIX (Palaiseau), LORIA (Nancy), and PPS (Paris). INFER has provided the theoretical basis on deep inference that is needed for our proposed research in STRUCTURAL.

The collaboration between the Austrian and French teams has been preceded by two ÖAD/PHC exchange projects, which have precisely the aim of initiating collaborations: the ÖAD-PHC Amadeus project "Logic-Based Analysis of Computation" FR 10/2009 between PPS and Universität Innsbruck, and the ÖAD-PHC Amadeus on "The Realm of Cut Elimination" between LIX, PPS, and TU Wien (Austria).

Participating Laboratories

Preuves, Programmes, Systèmes (PPS)
Responsible: Michel Parigot

Laboratoire d'Informatique d'Ecole Polytechnique (LIX)
Responsible: Lutz Straßburger

Universität Innsbruck
Responsible: Georg Moser

TU Vienna
Responsible: Matthias Baaz

Project description (scientific part only)

Pdf document

Events

Open Positions

There is an open 12-month postdoc position at LIX financed by the ANR within this project.

Applicants must have a Ph.D. or equivalent in computer science or mathematics, and should have a strong background in proof theory and/or related topics.

Applications should be sent via email to Lutz Straßburger and should include a CV, a short research statement (1-2 pages), and one or two recommendation letters.

Deadline: January 31, 2013


  Last update:  January 10, 2013            Lutz Straßburger