more on this theme | more from this text
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?
13832 | Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) [Gentzen, by Hacking] |
10067 | Gentzen proved the consistency of arithmetic from assumptions beyond arithmetic [Gentzen, by Musgrave] |
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] |
11213 | Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule [Gentzen] |