"Gentzen was motivated by a desire to establish the consistency of number theory. He was unable to prove the main result required for the consistency result, the cut elimination theorem - the Hauptsatz - directly for Natural Deduction. For this reason he introduced his alternative system, the sequent calculus for which he proves the Hauptsatz both for classical and intuitionistic logic." http://en.wikipedia.org/wiki/Natural_deduction
Any direct proofs of cut-elimination for natural deduction
around? Whats their underlying substantial idea exactly?