more on this theme | more from this thinker
Full Idea
The introduction rules represent, as it were, the 'definitions' of the symbols concerned, and the elimination rules are no more, in the final analysis, than the consequences of these definitions.
Gist of Idea
The logical connectives are 'defined' by their introduction rules
Source
Gerhard Gentzen (works [1938]), quoted by Stephen Read - Thinking About Logic Ch.8
Book Ref
Read,Stephen: 'Thinking About Logic' [OUP 1995], p.229
A Reaction
If an introduction-rule (or a truth table) were taken as fixed and beyond dispute, then it would have the status of a definition, since there would be nothing else to appeal to. So is there anything else to appeal to here?
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] |