more from this thinker | more from this text
Full Idea
Many books take RAA (reductio) and DNE (double neg) as the natural deduction introduction- and elimination-rules for negation, but RAA is not a natural introduction rule. I prefer TND (tertium) and EFQ (ex falso) for ¬-introduction and -elimination.
Gist of Idea
Excluded middle is an introduction rule for negation, and ex falso quodlibet will eliminate it
Source
David Bostock (Intermediate Logic [1997], 6.2)
Book Ref
Bostock,David: 'Intermediate Logic' [OUP 1997], p.251
Related Ideas
Idea 13754 Natural deduction rules for → are the Deduction Theorem (→I) and Modus Ponens (→E) [Bostock]
Idea 9402 RAA: If assuming A will prove B∧¬B, then derive ¬A [Lemmon]
Idea 9396 DN: Given A, we may derive ¬¬A [Lemmon]
Idea 9024 Excluded middle has three different definitions [Quine]
Idea 13353 'Negation' says that Γ,¬φ|= iff Γ|=φ [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] |