Ein Syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die Intuitionistische Typenlogik

In 1] Girard gives a procedure, by which all derivations in the calculus of natural deductions of Prawitz 4] are transformed into normal derivations. Exploiting his idea we give a syntactical proof of the admissibility of the cut rule in Schütte's formal system of intuitionistic type theory. We obtain a normal form theorem but not a normalization theorem. Our Berechnungsprädikate are different from the candidats de reductibilite of Girard. In the case of second order logic Berechnungsprädikate für Terme t^(O) are not defined for derivations ending with r^O e t^(O) which are normalizable, but for finite formula sets with the property, that r^O e t^(O) is derivable without cut.