slideshow 3

Logic seminar

Elementary cut-elimination for prenex cuts in disjunction free LJ

Matthias Baaz
Vienna University of Technology


Wednesday, 11. February 2015 - 13:30
IM, rear building, ground floor
The elimination of cuts (lemmas) from given sequent calculus proofs has remained in the focus of proof theory ever since Gentzen's seminal paper from 1934/35. It is well known that the worst case complexity of cut-elimination is non-elementary for first-order intuitionistic as well as classical logic. No elementary upper bound for cut-elimination seems to be known for non-trivial genuine first-order fragments of intuitionistic logics. The purpose of this paper is to show that one can in fact eliminate cuts involving only prenex cut-formulas from disjunction-free intuitionistic sequent proofs without non-elementary increase in the size of proofs. The result is sharp in several respects. As we will show, in all of the following cases there exist non-elementary lower bounds for cut-elimination: (1) classical disjunction-free proofs with quantified atomic cuts (2) intuitionistic disjunction-free proofs with infix cuts, (3) intuitionistic proofs with prenex cuts in the presence of disjunction. (joint work with Chris Fermüller, Vienna University of Technology)