The Road To Natural Deduction —A Comparison Between G.Gentzen And S.Jaskowski

The idea of natural deduction for logic was derived from Jan Lukasiewicz. Jan Lukasiewicz had posed the problem in his 1926 seminars that mathematicians do not construct their proofs by means of an axiomatic theory, but rather make use of other method of reasoning, especially they allow themselves to make "arbitrary assumption-s" and see where they lead. In 1934, two groundbreaking works on natural deduction were published by G.Gentzen and S.Jaskowski, which marking the beginning of natural deduction formally. Although they worked out their results independently, there is no doubt that both of them realized the same idea-the formalization of the "natural " ways of reasoning in mathematics. Additionally, the systems they provided differ significantly, including the rule for logical constants and proof style. In the present dissertation, begin with the investigation into G.Gentzen and S.Jaskowski’s approach to natural deduction, we focus on show the difference of both authors.Chapter 1 contains an introduction into backgrounds of natural deduction.Chapter 2 introduced the three stage of G.Gentzen’s approach to natural deduction: five forms of natural calculi in 1932; the calculus NJ, NK and LJ, LK in 1936; natural deduction in sequent calculus style in 1936.Chapter 3 discussed S.Jaskowski’s method to natural deduction:natural deduction for propositional logic, intutionist logic and predicate logic.Chapter 4 investigated the difference between the two authors’road to natural de-duction.Chapter 5 is conclusion. G.Gentzen’s thought of natural deduction was originated from the GOttingen School, his starting point and goal was to prove the consistency of arithmetic. In this way, the method of presenting proofs in G.Gentzen’s ND systems was by the means of trees. In addition, the tree format can be used to investigate the structural property of proof, thus leading to a new direction of proof theory-Structural Proof The-ory. What’s more, the requirements for the rules for the logical connectives must come in pairs of "introduce a connective" and "eliminate that connective" hastened the birth of proof-theoretic semantics and inferentialism. In contrast, the thought of S.Jaskowski came from Warsaw School. In order to solve the problem presented by Jan Lukasiewicz, S.Jaskowski developed a system that what we now recognise as natural deduction, call-ing it a "method of suppositions". And with the influence by the guiding principle of many logical investigations in the Warsaw School of logic, the logical constants and it’s rules in S.Jaskowski’s system was as little as possible and the method of presenting proofs was as intuitive as possible. As a result, S.Jaskowski’s system has great effect on the logic textbooks and logic teaching.