structure for 'Theory of Logic'    |     alphabetical list of themes    |     expand these ideas

5. Theory of Logic / H. Proof Systems / 4. Natural Deduction

[proofs built from introduction and elimination rules]

14 ideas
Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) [Gentzen, by Hacking]
Natural deduction takes proof from assumptions (with its rules) as basic, and axioms play no part [Bostock]
Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E) [Bostock]
Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it [Bostock]
In natural deduction we work from the premisses and the conclusion, hoping to meet in the middle [Bostock]
The Deduction Theorem is what licenses a system of natural deduction [Bostock]
In natural deduction, inferences are atomic steps involving just one logical constant [Prawitz]
A 'natural deduction system' has no axioms but many rules [Smith,P]
Or-elimination is 'Argument by Cases'; it shows how to derive C from 'A or B' [Williamson]
Natural deduction helpfully allows reasoning with assumptions [Sider]
Unlike axiom proofs, natural deduction proofs needn't focus on logical truths and theorems [Hale]
Many-valued logics lack a natural deduction system [Mares]
'Tonk' is supposed to follow the elimination and introduction rules, but it can't be so interpreted [Sider]
Introduction rules give deduction conditions, and Elimination says what can be deduced [Rumfitt]