Ideas from 'works' by Gerhard Gentzen [1938], by Theme Structure

Click on the Idea Number for the full details    |     back to texts     |     expand these ideas

5. Theory of Logic / A. Overview of Logic / 2. History of Logic
Gentzen introduced a natural deduction calculus (NK) in 1934
5. Theory of Logic / E. Structures of Logic / 2. Logical Connectives / a. Logical connectives
The inferential role of a logical constant constitutes its meaning
The logical connectives are 'defined' by their introduction rules
Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule
6. Mathematics / B. Foundations for Mathematics / 3. Axioms for Number / g. Incompleteness of Arithmetic
Gentzen proved the consistency of arithmetic from assumptions beyond arithmetic