more on this theme | more from this thinker
Full Idea
To every logical symbol there belongs precisely one inference figure which 'introduces' the symbol ..and one which 'eliminates' it. The introductions represent the 'definitions' of the symbols concerned, and eliminations are consequences of these.
Gist of Idea
Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule
Source
Gerhard Gentzen (works [1938], II.5.13), quoted by Ian Rumfitt - "Yes" and "No" III
Book Ref
-: 'Mind' [-], p.787
A Reaction
[1935 paper] This passage is famous, in laying down the basics of natural deduction systems of logic (ones using only rules, and avoiding axioms). Rumfitt questions whether Gentzen's account gives the sense of the connectives.
| 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] |
| 10067 | Gentzen proved the consistency of arithmetic from assumptions beyond arithmetic [Gentzen, by Musgrave] |
| 11213 | Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule [Gentzen] |