structure for 'Formal Logic'    |     alphabetical list of themes    |     expand these ideas

### 4. Formal Logic / B. Propositional Logic PL / 2. Tools of Propositional Logic / d. Basic theorems of PL

#### [very useful sequents provable in propositional logic]

18 ideas
 9527 The Distributive Laws can rearrange a pair of conjunctions or disjunctions [Lemmon]
 9523 De Morgan's Laws make negated conjunctions/disjunctions into non-negated disjunctions/conjunctions [Lemmon]
 9526 We can change conjunctions into negated conditionals with P→Q -||- ¬(P → ¬Q) [Lemmon]
 9522 'Modus ponendo tollens' (MPT) says P, ¬(P ∧ Q) |- ¬Q [Lemmon]
 9524 We can change conditionals into disjunctions with P→Q -||- ¬P ∨ Q [Lemmon]
 9525 We can change conditionals into negated conjunctions with P→Q -||- ¬(P ∧ ¬Q) [Lemmon]
 9521 'Modus tollendo ponens' (MTP) says ¬P, P ∨ Q |- 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]