A note on cut-elimination for classical propositional logic (Q2144620)

The article presents a simplification of Schwichtenberg's cut elimination procedure for classical first-order logic when restricted to the propositional case. The method is based on Tait's cut elimination for a one-sided sequent system, which is restricted to conjunction, disjunction, and negation as a complement. The proof of the Hauptsatz is based on a height-preserving permutation argument which lets us assume that the cut formula is principal in each rule deriving the cut premises. The Hauptsatz is then proven through a double induction on the maximal cut complexity, with a side induction on the number of maximal cut-applications, by reducing a topmost maximal cut. The proof does not extend to predicate logic. However, clear bounds on the size of the cut-free derivation can be provided based on the complexity of the conclusion.