Investigations Into Gentzen’s Logical Deduction

Gerhard Gentzen’s inaugural dissertation for the University of Gottingen, "Investigations into Logical Deduction", in which he developed two forms of logic deduction, the "natural deduction" and "sequent calculus". Gentzen introduced his work by starting first from a "natural deduction", which is closing to the the actual reasoning in mathematical proofs, and by then transforming it to a "sequent calculus", in which Gentzen gave a proof of the consistency of this system. Gentzen present his thought of logic deduction in this paper, and made a deeper work on the logic calculus. The purpose of this paper here is to clarify the status, influence and development of Gentzen’s thought of logic deduction by presenting the logical deduction of Gentzen and making a comparative study on his logic calculus systems.The first chapter in this paper introduces the mathematical axiom systems and the formal systems, and describes Frege’s and Hilbert’s logic calculus systems, the "Concept notation" and the "Hilbert style axiom system". This section constitutes the background of Gentzen"s thought of logical deduction.The second chapter and the third chapter are the most important and difficult parts, in which the author systematically introduces the main contents of Gentzen’s logic deduction. The works in second chapter focus on the introduction of natural deduction, and the comparative study on natural deduction and axiom system, then the author clarifies the advantages and disadvantages of natural deduction. The third chapter introduces the sequent calculus and the main idea of the proof of the "cut-elimination" theory. Furthermore, the auther makes a comparative analysis on sequent calculus and natural deduction and dissertates the improvement and consistency of this logic calculus.The fourth part is the summary and outlook of Gentzen’s logic deduction thought. In this part, the author summarizes the formation of Gentzen’s logic caculus, and states the influence and development of Gentzen’s thought. On the basis of the axiom system, Gentzen developed logic calculus and constructed the natural deduction, which is closing to the actual reasoning and contains only inference rules. After this initial attempt, Genzten formed the sequent calculus for proving the consistency of it, and then he proved the cut-elimination theory. Whst’s more, Gentzen discussed the applications of the theory,and proved the equivalence of the sepuent calculus and natural deduction. After Gentzen’s work, many foreign logicians and mathematicians studied and developed his investigations. Consequently, Gentzen’s thought of logic deduction is the milestone in the history of logic, and the study on his theory still has has great theoretical value and significance.