## Gentzenizing Schroeder-Heister's Natural Extension of Natural
Deduction

**A. Avron**
*Abstract:* 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.

*LFCS report ECS-LFCS-87-20*

Previous |

Index |

Next