Aim of the Workshop

The Collegium Logicum 2005: Cut-Elimination is intended as a forum for the exchange of ideas and interaction between researchers working in different areas of cut-elimination. The workshop covers both foundational and computational aspects.

Cut elimination introduced by Gerhard Gentzen is the most prominent form of proof transformation in logic and plays an important role in consistency proofs and in analyzing real mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) from proofs resulting in a proof which is analytic in the sense, that all statements in the proof are subformulas of the result. Therefore, the proof of a combinatorial statement is converted into a purely combinatorial proof. Cut elimination is therefore an essential tool for the analysis of proofs, especially to make implicit parameters explicit. Cut free derivations allow for

• the extraction of Herbrand disjunctions, which can be used to establish bounds on existential quantifiers (e.g. Luckhardt's analysis of the Theorem of Roth).

• the construction of interpolants, which allow for the replacement of implicit definitions by explicit definitions according to Beth's Theorem.

• the calculation of generalized variants of the end formula.

This workshop is intended to bring together the most relevant European scientists from the fields of logic, mathematics and computer science.

Their combined knowledge should lead to the development and standardization of concepts for cut-elimination adequate both from the foundational and applicative point of view.