more from this thinker
|
more from this text
Single Idea 13835
[filed under theme 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 Ref
'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]
The
18 ideas
with the same theme
[very useful sequents provable in propositional logic]:
|
9522
|
'Modus ponendo tollens' (MPT) says P, ¬(P ∧ Q) |- ¬Q
[Lemmon]
|
|
9521
|
'Modus tollendo ponens' (MTP) says ¬P, P ∨ Q |- Q
[Lemmon]
|
|
9525
|
We can change conditionals into negated conjunctions with P→Q -||- ¬(P ∧ ¬Q)
[Lemmon]
|
|
9524
|
We can change conditionals into disjunctions with P→Q -||- ¬P ∨ Q
[Lemmon]
|
|
9523
|
De Morgan's Laws make negated conjunctions/disjunctions into non-negated disjunctions/conjunctions
[Lemmon]
|
|
9527
|
The Distributive Laws can rearrange a pair of conjunctions or disjunctions
[Lemmon]
|
|
9526
|
We can change conjunctions into negated conditionals with P→Q -||- ¬(P → ¬Q)
[Lemmon]
|
|
9541
|
The Law of Transposition says (P→Q) → (¬Q→¬P)
[Hughes/Cresswell]
|
|
13833
|
'Thinning' ('dilution') is the key difference between deduction (which allows it) and induction
[Hacking]
|
|
13834
|
Gentzen's Cut Rule (or transitivity of deduction) is 'If A |- B and B |- C, then A |- C'
[Hacking]
|
|
13835
|
Only Cut reduces complexity, so logic is constructive without it, and it can be dispensed with
[Hacking]
|
|
13350
|
'Assumptions' says that a formula entails itself (φ|=φ)
[Bostock]
|
|
13351
|
'Thinning' allows that if premisses entail a conclusion, then adding further premisses makes no difference
[Bostock]
|
|
13352
|
'Cutting' allows that if x is proved, and adding y then proves z, you can go straight to z
[Bostock]
|
|
13353
|
'Negation' says that Γ,¬φ|= iff Γ|=φ
[Bostock]
|
|
13354
|
'Conjunction' says that Γ|=φ∧ψ iff Γ|=φ and Γ|=ψ
[Bostock]
|
|
13355
|
'Disjunction' says that Γ,φ∨ψ|= iff Γ,φ|= and Γ,ψ|=
[Bostock]
|
|
13356
|
The 'conditional' is that Γ|=φ→ψ iff Γ,φ|=ψ
[Bostock]
|