On Natural Deduction
1. General nature of natural deduction. 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 Gentien'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. It will be seen, when we proceed to details, that the rules of natural deduction lack certain traits of elegance which grace the more usual systematizations of quantification theory. Any reader who for this reason inclines to a systematization of the more usual kind may still look upon the rules of natural deduction (hereafter to be set forth) as a set of derived rules, or metatheorems, of his own system. Their derivability, granted the completeness of his own system, is assured by the ensuing proof of soundness (?6). The rules remain notable as metatheorems, in view of the virtues previously urged; and, as we shall see (?5), they are adequate to quantification theory in its entirety. The schemata of quantification theory are built up of atomic schemata 'p', 'q', 'r', 'Fx', 'Fy', 'GOx', 'Hyz', etc., by means of truth-functional connectives ' '.', 'D', etc. and quantifiers '(x)', '(y)', '(3x)', etc. in the familiar ways. A schema is called valid if it comes out true no matter what truth values be assigned to 'p', 'q', etc., and no matter what non-empty universe be adopted as range for the variables 'x', 'y', etc., and no matter what classes and relations of objects in that universe be adopted as interpretations of 'F, 'G', 'H', etc., and no matter what objects in that universe be assigned to the free variables. One