| Popis: |
Publisher Summary The term inferential deduction is used to describe deduction based on inferential rules of G. Gentzen type. This chapter discusses three loosely connected topics. M. Anderson and H. Johnstone presented the Gentzen natural rules in a linear form that was used by S. Jaskowski and B. Fitch. This formulation is, in principle, equivalent to the formulation by proof trees that G. Gentzen used. However, for certain rather technical purposes, it is desirable to have an explicit process or algorithm for transforming either of these forms of proof into the other. The chapter describes this technicality. It also discusses the semantics of Gentzen L-rules. The natural rules of Gentzen have the peculiarity that some of the rules involve discharge of assumptions. |
