Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence.
Monday, October 9 2006, 13:15
Favoritenstrasse 9, ground floor
Mathematical Applications of Cut-Elimination
Cut-elimination is an important technique in proof theory. It serves the purpose to eliminate lemmas from proofs and to produce normalized proofs with the subformula property (the material of the whole proof can be obtained by instantiations of subformulas of the theorem to be proved). In proof theory cut-elimination is frequently used to prove consistency of logical systems. Girard (in 1986) gave an interesting mathematical application of cut-elimination: He demonstrated, that the Fürstenberg-Weiss proof of van der Waerden's theorem on partitions (which is based on metric spaces) can be transformed into van der Waerden's original elementary proof via cut-elimination. This shows that cut-elimination can be used as a technique to obtain elementary proofs from others wich apply higher-level concepts. From these elementary proofs algorithms and effective constructions can be extracted.In this seminar, we discuss the cut-elimination theorem by G. Gentzen, Girard's proof transformation on van der Waerden's theorem (which was done by hand), and the recent development of automated cut-elimination methods (CERES) for the transformation of mathematical proofs.