Preprint:
Samuel R. Buss
"Cut Elimination In Situ"
To appear in
Gentzen's Centenary: The Quest for Consistency
R. Kahle and M. Rathjen, eds.,
Springer Verlag, 2015, pp. 245-277.
Download manuscript: PDF.
Abstract: We present methods for removing top-level cuts from a proof without significantly increasing the space used for storing the proof. For propositional logic, this requires converting a proof from tree-like to dag-like form, but it most doubles the number of lines in the proof. For first-order logic, the proof size can grow exponentially, but the proof has a succinct description and is polynomial-time uniform. We use direct, global constructions that give polynomial time methods for removing all top-level cuts from proofs. By exploiting prenex representations, this extends to removing all cuts, with proof size bounded superexponentially in the alternation of quantifiers in cut formulas.