Gentzenizing Schroeder-Heister's natural extension of natural deduction (Q923083)

The author provides an example of how the use of the Gentzen-type sequential calculus simplifies a complex natural deduction formalism by giving the Gentzen-type version to the natural deduction system of Schroeder-Heister. The notions of the natural deduction system that are difficult to handle become redundant, so that the complex normalization proof can be replaced by a standard cut-elimination proof. The resulting Gentzen system is essentially the same as the intuitionistic one, which therefore sheds new light on the connection between Schroeder-Heister's higher-order rules and intuitionistic implication.