more from this thinker | more from this text
Full Idea
Natural deduction adopts for → as rules the Deduction Theorem and Modus Ponens, here called →I and →E. If ψ follows φ in the proof, we can write φ→ψ (→I). φ and φ→ψ permit ψ (→E).
Clarification
'I' means introduction, and 'E' means elimination
Gist of Idea
Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E)
Source
David Bostock (Intermediate Logic [1997], 6.2)
Book Ref
Bostock,David: 'Intermediate Logic' [OUP 1997], p.248
A Reaction
Natural deduction has this neat and appealing way of formally introducing or eliminating each connective, so that you know where you are, and you know what each one means.
Related Idea
Idea 13755 Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it [Bostock]
| 13832 | Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) [Gentzen, by Hacking] |
| 13753 | Natural deduction takes proof from assumptions (with its rules) as basic, and axioms play no part [Bostock] |
| 13755 | Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it [Bostock] |
| 13754 | Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E) [Bostock] |
| 13758 | In natural deduction we work from the premisses and the conclusion, hoping to meet in the middle [Bostock] |
| 18120 | The Deduction Theorem is what licenses a system of natural deduction [Bostock] |
| 13823 | In natural deduction, inferences are atomic steps involving just one logical constant [Prawitz] |
| 10602 | A 'natural deduction system' has no axioms but many rules [Smith,P] |
| 21612 | Or-elimination is 'Argument by Cases'; it shows how to derive C from 'A or B' [Williamson] |
| 13685 | Natural deduction helpfully allows reasoning with assumptions [Sider] |
| 19298 | Unlike axiom proofs, natural deduction proofs needn't focus on logical truths and theorems [Hale] |
| 18783 | Many-valued logics lack a natural deduction system [Mares] |
| 15001 | 'Tonk' is supposed to follow the elimination and introduction rules, but it can't be so interpreted [Sider] |
| 18800 | Introduction rules give deduction conditions, and Elimination says what can be deduced [Rumfitt] |