1935 | Investigations into Logical Deduction |
p.231 | 13832 | Natural deduction shows the heart of reasoning (and sequent calculus is just a tool) |
1938 | works |
p.63 | 11065 | The inferential role of a logical constant constitutes its meaning |
p.126 | 10067 | Gentzen proved the consistency of arithmetic from assumptions beyond arithmetic |
p.228 | 11022 | Gentzen introduced a natural deduction calculus (NK) in 1934 |
p.229 | 11023 | The logical connectives are 'defined' by their introduction rules |
II.5.13 | p.787 | 11213 | Each logical symbol has an 'introduction' rule to define it, and hence an 'elimination' rule |