Portal:Philosophy/Selected article/2006-15

In mathematical logic, natural deduction is any of a class of foundational approaches for two key concepts in logic, propositions and proofs. There is no universal agreement on the proper foundation of these concepts; natural deduction takes the approach of mimicking the mental picture of logical reasoning as closely as possible, though in much greater detail than is usual in published mathematics.

Natural deduction grew out of a context of dissatisfaction with sentential axiomatizations common to the systems of Hilbert, Frege and Russell, most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica. Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, Jaśkowski made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935. His proposals, though, did not prove to be popular, and natural deduction in its modern form was independently proposed by the German mathematician Gentzen in 1935, in a dissertation delivered to the faculty of mathematical sciences of the university of Göttingen. The term natural deduction (rather, its German form) was coined in that paper:

Gentzen was motivated by a desire to establish the consistency of number theory, and he found immediate use for his natural deduction calculus. He was nevertheless dissatisfied with the complexity of his proofs, and in 1938 gave a new consistency proof using his sequent calculus. In a series of seminars in 1961 and 1962 Prawitz gave a comprehensive summary of natural deduction calculi, and transported much of Gentzen's work with sequent calculi into the natural deduction framework. His 1965 monograph Natural deduction: a proof-theoretical study was to become the definitive work on natural deduction, and included applications for modal and second-order logic.

...Archive

Read more...