Direct cut-elimination for natural deduction.

Question

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

Answer 1

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/

Answer 2

I guess cut elimination from natural deduction is rather the rule than the exception. If I remember well Gentzens paper itself goes from Hilbert style Hx, to Natural Deduction Nx and then to sequent calculus Lx.

The first step requires to convert each Hilbert style axiom to be converted into a Natural Deduction derivation, using already sequents. Here are some examples, from minimal logic implication fragment only:

Hilbert Style axiom: $A \rightarrow A$
Natural Deduction derivation: $\begin{array}{c} A \vdash A \\ \hline \vdash A \rightarrow A \end{array}$

Hilbert Style axiom: $A \rightarrow (B \rightarrow A)$
Natural Deduction derivation: $\begin{array}{c} A \vdash A \\ \hline A \vdash B \rightarrow A \\ \hline \vdash A \rightarrow (B \rightarrow A) \end{array}$

Hilbert Style axiom: $(A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow B) \rightarrow A \rightarrow C$
Natural Deduction derivation: $\begin{array}{c} \begin{array}{c} \begin{array}{c} \hline A \rightarrow (B \rightarrow C) \vdash A \rightarrow (B \rightarrow C) \\ \end{array} \begin{array}{c} \hline A \vdash A \\ \end{array} \\ \hline A \rightarrow (B \rightarrow C), A \vdash B \rightarrow C \end{array} \begin{array}{c} \begin{array}{c} \hline A \rightarrow B \vdash A \rightarrow B \\ \end{array} \begin{array}{c} \hline A \vdash A \\ \end{array} \\ \hline A \rightarrow B, A \vdash B \end{array} \\ \hline A \rightarrow (B \rightarrow C), A \rightarrow B, A \vdash C \\ \hline A \rightarrow (B \rightarrow C), A \rightarrow B \vdash A \rightarrow C \\ \hline A \rightarrow (B \rightarrow C) \vdash (A \rightarrow B) \rightarrow A \rightarrow C \\ \hline \vdash (A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow B) \rightarrow A \rightarrow C \end{array}$

Since Natural Deduction has also modus ponens, like Hilbert style, we are already done with the transformation from Hx to Nx. The cut elimination can now begin, taking the Nx derivation, converting it to a Lx derivation.

On can put this transformation on the computer, see here.