Systems of natural deduction as a method of theorem proving
were first developed in detail by Gentzen and Jáskowski. The complex
nature of the rules for quantification in these early systems of natural
deduction, and in particular of the parallel rules of Universal Generalization
(UG) and Existential Instantiation (El) led to an active research
program in the period from the late 1950's to the late 1960's in an effort
by Quine, Suppes, Leblanc, and Copi to develop simplified and correct
rules of inferences for the quantified formulae of first-order functional
logic. We explore the history of these efforts and examine the difficulties
found in the "unnatural" natural deductive systems that were developed
for first-order logic. Our survey covers roughly forty years, from 1929
to 1971, which includes the early work of Hertz on which Gentzen's work
was based through the development of the quantifation rules in Copi's
system of natural deduction as presented in the third edition of his
textbook Symbolic logic. Also considered is the extent to which O. H.
Mitchell made a start at developing a system of natural deduction in his
1883 paper On a new algebra