more on this theme | more from this text
Full Idea
Gentzen thought that his natural deduction gets at the heart of logical reasoning, and used the sequent calculus only as a convenient tool for proving his chief results.
Gist of Idea
Natural deduction shows the heart of reasoning (and sequent calculus is just a tool)
Source
report of Gerhard Gentzen (Investigations into Logical Deduction [1935]) by Ian Hacking - What is Logic? §05
Book Ref
'A Philosophical Companion to First-Order Logic', ed/tr. Hughes,R.I.G. [Hackett 1993], p.231
| 13832 | Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) [Gentzen, by Hacking] |
| 10067 | Gentzen proved the consistency of arithmetic from assumptions beyond arithmetic [Gentzen, by Musgrave] |
| 11022 | Gentzen introduced a natural deduction calculus (NK) in 1934 [Gentzen, by Read] |
| 11065 | The inferential role of a logical constant constitutes its meaning [Gentzen, by Hanna] |
| 11023 | The logical connectives are 'defined' by their introduction rules [Gentzen] |
| 11213 | Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule [Gentzen] |