The Journal of Symbolic Logic

Research Article

A natural extension of natural deduction

Peter Schroeder-Heister

Fachgruppe Philosophie, Universität Konstanz, Postfach 5560, 7750 Konstanz, Federal Republic of Germany

One of the main ideas of calculi of natural deduction, as introduced by Jaśkowski and Gentzen, is that assumptions may be discharged in the course of a derivation. As regards sentential logic, this conception will be extended in so far as not only formulas but also rules may serve as assumptions which can be discharged. The resulting calculi and derivations with rules of any finite level are informally introduced in §1, while §§2 and 3 state formal definitions of the concepts involved and basic lemmata. Within this framework, a standard form for introduction and elimination rules for arbitrary n-ary sentential operators is motivated in §4, understood as a contribution to the theory of meaning for logical signs. §5 proves that the set {&, ∨, ⊃, ⋏} of standard intuitionistic connectives is complete, i.e. &, ∨, ⊃, and ⋏ suffice to express each n-ary sentential operator having rules of the standard form given in §4. §6 makes some remarks on related approaches. For an extension of the conception presented here to quantifier logic, see [11].

(Received April 01 1982)

(Revised August 31 1983)


1   I should like to thank Professors G. Hasenjaeger and D. Prawitz for their support and criticism of my dissertation, and the anonymous referee (to whom the title of this paper is also due) for helpful suggestions.