Gentzenizing Schroeder-Heister's natural extension of natural deduction.
Open Access
- 1 December 1989
- journal article
- Published by Duke University Press in Notre Dame Journal of Formal Logic
- Vol. 31 (1) , 127-135
- https://doi.org/10.1305/ndjfl/1093635337
Abstract
This paper we provide a Gentzen-type formulation of Schroeder-Heister'ssystem of [1]. This system is important from both philosophical and practicalpoints of view: Its philisophical importance is due to the characterizationwhich it provides for the intuitionistic connectives, while the practical one isdue to the fact that its notion of higher-order rules and its method of treatingthe elimination rules were incorporated into the Edinburgh LF (A generallogical framework for implementing...Keywords
This publication has 0 references indexed in Scilit: