Gentzenizing Schroeder-Heister's natural extension of natural deduction.
Arnon Avron · Notre Dame Journal of Formal Logic · 1989
Our purpose here is to provide an example of how the use of the Gentzen-type sequential calculus considerably simplifies a complex Natural Deduction formalism.The formalism is that of Schroeder-Heister's system of higher-order rules.We show that the notions of Schroeder-Heister's that are the most difficult to handle (discharge functions and subrules) become redundant in the Gentzen-type version.The complex normalization proof given by Schroeder-Heister can be replaced therefore by a standard cutelimination proof.It turns out also that the unusual form of some of the elimination rules of Schroeder-Heister corresponds to the natural, standard form of antecedent rules in sequential calculi.