more from Gerhard Gentzen

Single Idea 11213

[catalogued under 5. Theory of Logic / E. Structures of Logic / 2. Logical Connectives / a. Logical connectives]

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


Gerhard Gentzen (works [1938], II.5.13), quoted by Ian Rumfitt - "Yes" and "No" III

Book Reference

-: '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.