Single Idea 13834

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

Full Idea

If A |- B and B |- C, then A |- C. This generalises to: If Γ|-A,Θ and Γ,A |- Θ, then Γ |- Θ. Gentzen called this 'cut'. It is the transitivity of a deduction.

Clarification

|- is read as 'proves'

Gist of Idea

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

Source

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

Book Reference

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


A Reaction

I read the generalisation as 'If A can be either a premise or a conclusion, you can bypass it'. The first version is just transitivity (which by-passes the middle step).

Related Idea

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