Abstract

Recently discovered documents have shown how Gentzen had arrived at the final form of natural deduction, namely by trying out a great number of alternative formulations. What led him to natural deduction in the first place, other than the general idea of studying “mathematical inference as it appears in practice,” is not indicated anywhere in his publications or preserved manuscripts. It is suggested that formal work in axiomatic logic lies behind the birth of Gentzen’s natural deduction, rather than any single decisive influence in the work of others. Various axiomatizations are explored in turn, from the classical axioms of Hilbert and Ackermann to the intuitionistic axiomatization of Heyting.