more from this thinker     |     more from this text

Single Idea 18800

[filed under theme 5. Theory of Logic / H. Proof Systems / 4. Natural Deduction ]

Full Idea

'Introduction rules' state the conditions under which one may deduce a conclusion whose dominant logical operator is the connective. 'Elimination rules' state what may be deduced from some premises, where the major premise is dominated by the connective.

Gist of Idea

Introduction rules give deduction conditions, and Elimination says what can be deduced

Source

Ian Rumfitt (The Boundary Stones of Thought [2015], 1.1)

Book Ref

Rumfitt,Ian: 'The Boundary Stones of Thought' [OUP 2015], p.4

A Reaction

So Introduction gives conditions for deduction, and Elimination says what can actually be deduced. If my magic wand can turn you into a frog (introduction), and so I turn you into a frog, how does that 'eliminate' the wand?

The 14 ideas with the same theme [proofs built from introduction and elimination rules]:

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]