Single Idea 13835

[catalogued under 4. Formal Logic / B. Propositional Logic PL / 2. Tools of Propositional Logic / d. Basic theorems of PL]

Full Idea

Only the cut rule can have a conclusion that is less complex than its premises. Hence when cut is not used, a derivation is quite literally constructive, building up from components. Any theorem obtained by cut can be obtained without it.

Gist of Idea

Only Cut reduces complexity, so logic is constructive without it, and it can be dispensed with

Source

Ian Hacking (What is Logic? [1979], §08)

Book Reference

'A Philosophical Companion to First-Order Logic', ed/tr. Hughes,R.I.G. [Hackett 1993], p.235


Related Ideas

Idea 13834 Gentzen's Cut Rule (or transitivity of deduction) is 'If A |- B and B |- C, then A |- C' [Hacking]

Idea 13352 'Cutting' allows that if x is proved, and adding y then proves z, you can go straight to z [Bostock]