Gentzenizing Schroeder-Heister's Natural Extension of Natural Deduction
A. AvronAbstract: Our purpose here is to provide an example of how the use of Gentzen-type sequential calculus considerably simplifies a complex Natural Deduction formalism. In this case we deal with Schroeder-Heister's system of [1]. This system is important from both philosophical and practical points of view: Its philosophical importance is due to the characterization which it provides for the intuitionistic connectives, while the practical one is due to the fact that its notion of higher-order rules and its method of treating the elimination rules were incorporated into the Edinburgh LF (A general logical framework for implementing logical formalisms on a computer, which was developed in the Computer Science Department of the University of Edinburgh). We shall show, how the notions of S.H. that are the most difficult to handle (discharge functions and subrules) become redundant in the Gentzen-type version, and that the unusual form of some of the elimination rules of S.H. corresponds to natural, standard form of antecedent rules in sequential calculi. We note also that the complex normalization proof of S.H. can be replaced by a completely standard cut-elimination proof.
Previous | Index | Next