On natural deduction

Publisher Website
Google Scholar
Abstract
For Gentzen's natural deduction, a formalized method of deduction in quantification theory dating from 1934, these important advantages may be claimed: it corresponds more closely than other methods of formalized quantification theory to habitual unformalized modes of reasoning, and it consequently tends to minimize the false moves involved in seeking to construct proofs. The object of this paper is to present and justify a simplification of Gentzen's method, to the end of enhancing the advantages just claimed. No acquaintance with Gentzen's work will be presupposed.A further advantage of Gentzen's method, also somewhat enhanced in my revision of the method, is relative brevity of proofs. In the more usual systematizations of quantification theory, theorems are derived from axiom schemata by proofs which, if rendered in full, would quickly run to unwieldy lengths. Consequently an abbreviative expedient is usually adopted which consists in preserving and numbering theorems for reference in proofs of subsequent theorems. Further brevity is commonly gained by establishing metatheorems, or derived rules, for reference in proving subsequent theorems. In natural deduction, on the other hand, proofs tend to be so short that the abbreviative expedients just now mentioned may conveniently be dispensed with—at least until theorems of extraordinary complexity are embarked upon. In natural deduction accordingly it is customary to start each argument from scratch, without benefit of accumulated theorems or derived rules.

This publication has 2 references indexed in Scilit: