Just reading:

"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?

Best Regards


The analogue in the case of natural deduction of cut elimination for sequent calculi is normalization, and normalization for classical logic was proved by Dag Prawitz in his 1965 thesis, Natural Deduction: A Proof-Theoretical Study (now easily and cheaply available as a Dover reprint). See also the lovely book by Sara Negri and Jan von Plato, Stuctural Proof Theory (CUP, 2001).

To put this into historical context, check out von Plato's nice review article, http://plato.stanford.edu/entries/proof-theory-development/

  • $\begingroup$ Do you mean, "the analogue of cut elimination in natural deduction"? $\endgroup$ – Zhen Lin Apr 12 '13 at 11:03
  • 2
    $\begingroup$ The key innovation in Prawitz's treatment that eluded Gentzen was how he handled formulae in rules with indirect elimination rules, which are needed for disjunction and existential elimination. You need to think of paths of formulae through these rules, and add permutations to the system to ensure that introduction and elimination rules can meet up. $\endgroup$ – Charles Stewart Apr 12 '13 at 11:05
  • $\begingroup$ @ZhenLin Yes, clarified $\endgroup$ – Peter Smith Apr 12 '13 at 11:11
  • $\begingroup$ @CharlesStewart is spot on, and clearer than I'd have managed! $\endgroup$ – Peter Smith Apr 12 '13 at 11:12
  • 2
    $\begingroup$ Peter: Thanks; I probably subconsciously "borrowed" from Girard's treatment of the topic in Ch. 10 of Proofs and Types: paultaylor.eu/stable/Proofs+Types.html $\endgroup$ – Charles Stewart Apr 12 '13 at 11:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.