A Brief History of Natural Deduction

HISTORY AND PHILOSOPHY OF LOGIC, 20 (1999), 1± 31 A Brief History of Natural Deduction Fr a n c i s J e f f r y P e l l e t i e r Department of Philosophy, University of Alberta, Edmonton, Alberta, Canada T6G 2E5 Received July 1998 Revised February 1999 Natural deduction is the type of logic most familiar to current philosophers, and indeed is all that many modern philosophers know about logic. Yet natural deduction is a fairly recent innovation in logic, dating fromGentzen and Jas! kowski in 1934. This article traces the development of natural deduction from the view that these founders embraced to the widespread acceptance of the method in the 1960s. I focus especially on the diŒerent choices made by writers of elementary textbooksÐ the standard conduits of the method to a generation of philosophersÐ with an eye to determining what the `essential characteristics ’ of natural deduction are. 1. Introduction In 1934 a most singular event occurred. Two papers were published on a topic that had (apparently) never before been written about, the authors had never been in contact with one another, and they had (apparently) no common intellectual background that would otherwise account for their mutual interest in this topic." These two papers formed the basis for a movement in logic which is by now the most common way of teaching elementary logic by far, and indeed is perhaps all that is known in any detail about logic by a number of philosophers (especially in North America). This manner of proceeding in logic is called `natural deduction.’ And in its own way the instigation of this style of logical proof is as important to the history of logic as the discovery of resolution by Robinson in 1965, or the discovery of the logisticalmethod by Frege in 1879, or even the discovery of the syllogistic by Aristotle in the fourth century BC. # Yet it is a story whose details are not known by those most aŒected: those `ordinary’ philosophers who are not logicians but who learned the standard amount of formal logic taught inNorth American undergraduate and graduate departments of philosophy.Most of these philosophers will have taken some (series of) logic courses that exhibited natural deduction, and may have heard that natural deduction is somehow opposed to various other styles of proof systems in some number of diŒerent ways. But they will not knowwhy `natural deduction’ has come to designate the types of systems that are found in most current elementary logic textbooks, nor will they know why there are certain diŒerences amongst the various textbooks and how these diŒerences can nevertheless all be encompassed under the umbrella term `natural deduction.’ The purpose of this article is to give a history of the development of this method of doing logic and to characterize what sort of thing is meant nowadays by the name. 1 Gerhard Gentzen (1934 } 5) and Stanasøaw Jas! kowski (1934). 2 Some scholars, e.g. Corcoran (1973), think that Aristotle’s syllogism should be counted as a natural deduction system, on the grounds that there are no axioms but there are many rules. Although this might be a reasonable characterization of natural deduction systems, I wish to consider only those natural deduction systems that were developed in direct response to the `logistical’ systems of the late 1800s and early 1900s. History and Philosophy of Logic ISSN 0144 ± 5340 print} ISSN 1464 ± 5149 online ’ 1999 Taylor & Francis Ltd http:} } www.tandf.co.uk } JNLS } hpl.htm http:} } www.taylorandfrancis.com} JNLS } hpl.htm 2 Francis J. Pelletier My view is that the current connotationof the term functions rather like a prototype: there is some exemplar that the term most clearly applies to and which manifests a number of characteristics. But there are other proof systems that diŒer from this prototypical natural deduction system and are nevertheless correctly characterized as being natural deduction. It is not clear to me just how many of the properties that the prototype exempli® es can be omitted and still have a system that is correctly characterized as a natural deduction system, and I will not try to give an answer. Instead I will focus on a number of features that are manifested to diŒerent degrees by the various natural deduction systems. My picture is that if a system ranks `low’ on one of these features, it can `make up for it ’ by ranking high on diŒerent features. And it is somehow an overall rating of the total mount of conformity to the entire range of these diŒerent features that determines whether any speci® c logical system will be called a natural deduction system. Some of these features stem from the initial introduction of natural deduction in 1934; but even more strongly, in my opinion, is the eŒect that elementary textbooks from the 1950s had. There were of course some more technical works that brought the notion of natural deduction into the consciousness of the logical world of the 1950s and 1960s. But I will argue that the `ordinary philosopher’ of the time would have been little in¯ uenced by these works and that the huge sway that natural deductionholds over current philosophy is mostly due to the textbooks of the 1950s. The history of how these textbooks came to contain the material they do is itself an interestingmatter, and I aim to detail this development of what is by now the most universally accepted method (within philosophy) of `doing logic.’ 2. The concept of `natural deduction’ Onemeaning of `natural deduction’ focuses on the notion that systems employing it will retain the `natural form’ of ® rst-order logic and will not restrict itself to any subset of the connectives nor any normal form representation. Although this is clearly a feature of the modern textbooks, we can easily see that such a de® nition is neither necessary nor su cient for a logical system’s being a natural deduction system. For, surely we can give natural deduction accounts for logics that have restricted sets of connectives, so it is not necessary. And we can have non-natural deduction systems (e.g. axiomatic systems) that contain all the usual connectives, so it is not su cient. Another feature of natural deduction systems, at least in the minds of some, is that they will have two rules for each connective: an introduction rule and an elimination rule. But again this can’ t be necessary, because there are many systems we happily call natural deduction which do not have rules organized in this manner. And even if we concocted an axiomatic system that did have rules of this nature, this would not make such a system become a natural deduction system. So it is not su cient either. A third feature in the minds of many is that the inference rules are `natural ’ or `pretheoretically accepted.’ To show how widely accepted this feature is, here is what four elementary natural deduction textbooks across a forty year span have to say. Suppes (1957, viii) says : `The system of inference ¼ has been designed to correspond as closely as possible to the author’ s conception of the most natural techniques of informal proof.’ Kalish and Montague (1964, 38) say that these systems `are said to employ natural deduction and, as this designation indicates, are intended to re¯ ect intuitive forms of reasoning.’ Bonevac (1987, 89) says : `we’ ll develop a system designed to simulate people’ s construction of arguments ¼ it is natural in the sense A Brief History of Natural Deduction 3 that it approaches ¼ the way people argue.’ And Chellas (1997, 134) says `Because the rules of inference closely resemble patterns of reasoning found in natural language discourse, the deductive system is of a kind called natural deduction.’ These authors are echoing Gentzen (1934 } 35, 74), one of the two inventors of natural deduction: `We wish to set up a formalism that re¯ ects as accurately as possible the actual logical reasoning involved in mathematical proofs.’ But this also is neither necessary nor su cient. An axiom system with only modus ponens as a rule of inference obeys the restriction that all the rules of inference are `natural ’ , yet no one wants to call such a system `natural deduction,’ so it is not a su cient condition. And we can invent rules of inference that we would happily call natural deduction even when they do not correspond to particularly normal modes of thought (such as is often done inmodal logics,many-valued logics, relevant logics, and other non-standard logics). As I have said, the notionof a rule of inference `being natural ’ or `pretheoretically accepted’ is often connected with formal systems of natural deduction; but as I also said, the two notions are not synonymous or even co-extensive. This means that there is an interesting area of research open to those who wish to investigate what `natural reasoning ’ is in ordinary, non-trained people. This sort of investigation is being carried out by a group of cognitive scientists, but their results are far from universally accepted (see Johnson-Laird and Byrne, 1991; Rips 1995). There is also a history to the notion of `natural deduction’ , and that history together with the way it was worked out by authors of elementary textbooks will account for our being drawn to mentioning such features of natural deduction systems and will yet also account for our belief that they are not de® nitory of the notion. 3. Jas! kowski and Gentzen In his 1926 seminars, Jan è ukasiewicz raised the issue that mathematicians do not construct their proofs by means of an axiomatic theory (the systems of logic that had been developed at the time) but rather made use of other reasoning methods; especially they allow themselves to make `arbitrary assumptions’ and see where they lead. è ukasiewicz issued the challenge for logicians to develop a logical theory that embodied this insight but which yielded the same set of theorems as the axiomatic system than in existence. The challenge was taken up to Stanisøaw Jas! kowski, culminating in his (1934) paper. This paper develops a methodÐ indeed, two methodsÐ for making `arbitrary assumptions’ and keeping track of where they lead and for how long the assumptions are in eŒect.$ One method is graphical in nature, drawing boxes or rectangles around portions of a proof ; the other method amounts to tracking the assumptions and their consequences by means of a book-keeping annotation alongside the sequence of formulas that constitutes a proof. In both methods the restrictions on completion of subproofs (as we now call them) are enforced by restrictions on how the boxes or book-keeping annotationscan be drawn. We would now say that Jas! kowski’ s system had two subproof-introductionmethods: conditional-proof (conditional-introduction) and reductio ad absurdum (negation- elimination). It also had rules for the direct manipulation of formulas (e.g. Modus Ponens). After formulating his set of rules. Jas! kowski remarks (p. 238) that the system 3 Some results of his had been presented as early as 1927, using the graphical method. 4 Francis J. Pelletier `has the peculiarity of requiring no axioms’ but that he can prove it equivalent to the established axiomatic systems of the time. (He shows this for various axiom systems of è ukasiewicz, Frege and Hilbert). he also remarks (p. 258) that his system is `more suited to the purposes of formalizing practical [mathematical] proofs’ than were the then-accepted system, which are `so burdensome that [they are] avoided even by the authors of logical [axiomatic] systems.’ Furthermore, `in even more complicated theories the use of [the axiomatic method] would be completely unproductive. ’ Given all this, one could say that Jas! kowski was the inventor of natural deduction as a complete logical theory. Working independently of è ukasiewicz and Jas! kowski, Gerhard Gentzen published an amazingly general and amazingly modern-sounding two-part paper in 1934 } 35. Gentzen’ s opening remarks are : My starting point was this: The formalization of logical deduction, especially as it has been developed by Frege, Russell, and Hilbert, is rather far removed from the forms of deduction used in practice in mathematical proofs. Considerable formal advantages are achieved in return. In contrast, I intended ® rst to set up a formal system which comes as close as possible to actual reasoning. The result was a `calculus of natural deduction ’ (`NJ ’ for intuitionist, `NK’ for classical predicate logic) ¼ Like Jas! kowski, Gentzen sees the notion of making an assumption to be the leading idea of his natural deduction systems : ¼ the essential diŒerence betweenNJ-derivations and derivations in the systems of Russell, Hilbert, and Heyting is the following: In the latter systems true formulae are derived from a sequence of `basic logical formulae ’ by means of a few forms of inference. Natural deduction, however, does not, in general, start from basic logical propositions, but rather from assumptions to which logical deductions are applied. By means of a later inference the result is then again made independent of the assumption. These two founding fathers of natural deduction were faced with the question of how this method of `making an arbitrary assumption and seeing where it leads ’ could be represented. As remarked above, Jas! kowski gave two methods. Gentzen also contributed a method, and there is one newer method. All of the representational methods used in today’ s natural deduction system are variants on one of these four. To see the four representations in use let’s look at a simple propositional theorem: (((P [ Q)& ( C R [ C Q)) [ (P [ R)).% Since the main connective is a conditional, the most likely strategy will be to prove it by a rule of conditional introduction.But to apply this rule one must have a subproof that assumes the conditional’ s antecedent and ends with the conditional’s consequent. All the methods will follow this strategy; the diŒerences among them concern only how to represent the strategy. In Jas! kowski’ s graphicalmethod, each time an assumption is made it starts a new portionof the proof 4 Jas! kowski’s language contained only conditional, negation, and universal quanti® er, so the use of & here is a certain liberty. But it is clear what his method would do if & were a primitive. I call the rule of &-elimination `simpli® cation’ . A Brief History of Natural Deduction 5 which is to be enclosed with a rectangle (a `subproof’ ). The ® rst line of this subproof is the assumption ¼ in the case of trying to apply conditional introduction, the assumption will be the antecedent of the conditional to be proved and the remainder of this subproof will be an attempt to generate the consequent of that conditional. If this can be done, then Jas! kowski’ s rule conditionalization says that the conditional can be asserted as proved in the subproof level of the box that surrounds the one just completed. So the present proof will assume the antecedent, ((P [ Q)& ( C R [ C Q)), thereby starting a subproof trying to generate the consequent, (P [ R). But this consequent itself has a conditional as main connective, and so it too should be proved by conditionalization with a yet-further-embedded subproof that assumes its antecedent, P, and tries to generate its consequent, R. As it turns out, this subproof calls for a yet further embedded subproof using Jas! kowski’ s reductio ad absurdum. To make the ebb and ¯ ow of assumptions coming into play and then being `discharged ’ work, one needs restrictions on what formulas are available for use with the various rules of inference. Using the graphical method, Jas! kowski mandated that any `ordinary rule ’ (e.g. Modus Ponens) is to have all the formulas required for the rule’ s applicabilitybe in the same rectangle. If the relevant formulas are not in the right scope level, Jas! kowski has a rule that allows lines to be repeated from one scope level into the next most embedded rectangle, but no such repetitions are allowed using any other con® guration of the rectangles. The `non-ordinary’ rules of Conditionalization and Reductio require that the subproof that is used to justify the rule’ s applicabilitybe immediately embedded one level deeper than the proposed place to use the rule. There are also restrictions that make each rectangle, once started, be completed before any other, more inclusive, rectangles can be completed. We need not go into these details here. A formula is proved only `under certain suppositions’ unless it is outside of any boxes, in which case it is a theoremÐ as the above demonstration proves about line g 13. This graphical method was streamlined somewhat by Fitch (1952), as we will see in more detail below, and proofs done in this manner are now usually called `Fitch diagrams.’ (Fitch does not have the whole rectangle, only the left vertical line; and he draws a line under the ® rst formulae of a subproof to indicate explicitly that it is an assumption for that subproof.) This method, with some slight variations, was then followed by Copi (1954), Anderson and Johnstone (1962), Kalish and Montague (1964), Thomason (1970), Leblanc andWisdom (1972), Kozy (1974), Tapscott (1976), Bergmann et al. (1980), Klenk (1983), Bonevac (1987), Kearns (1988), Wilson (1992), and many others. 6 Francis J. Pelletier Jas! kowski’ s second method (which he had hit upon somewhat later than the graphicalmethod)was to make a numerical annotationon the left-side of the formulas in a proof. This is best seen by example; and so we will re-present the previous proof. but a few things were changed by the time Jas! kowski described this method. First, he changed the statements of various of the rules and he gave them new names : Rule I is now the name for making a supposition, Rule II is the name for conditionalization, Rule III is the name for modus ponens, and Rule IV is the name for reductio ad absurdum. (Rules V, VI, and VII have to do with quanti® er elimination and introduction). & Some of the details of these changes to the rules are such that it is no longer required that all the preconditions for the applicability of a rule of inference must be in the same `scope level ’ (in the new method this means being in the same depth of numerical annotation), and hence there is no longer any requirement for a rule of repetition. To indicate that a formula is a supposition, Jas! kowski now pre® xes it with `S ’ . It can be seen that this second method is very closely related to the method of rectangles. (And much easier to typeset !) Its only real drawback concerns whether we can distinguish diŒerent subproofs which are at the same level of embedding. A confusion can arise when one subproof is completed and then another started, both at the same level of embedding. In the graphical method there will be a closing of one rectangle and the beginning of another, but here it could get confused. Jas! kowski’ s solution is to mark the second such subproof as having `2 ’ as its rightmost numerical pre® x. This makes numerals be superior to using other symbols in this role, such as an asterisk. As we will see in section 5, this representational method was adopted by Quine (1950a), who used asterisks rather than numerals thus leading to the shortcoming just noted. One reason that this book-keeping method of Jas! kowski did not become more common is that Suppes (1957) introduced a method (which could be seen as a variant on the method, but which I think is diŒerent enough in both its appearance and in its metalogical properties that it should be called a distinct method) using the line numbers of the assumptions which any given line in the proof depended upon, rather than asterisks or arbitrary numerals. In this thir