Recitation 18: Examples of proof. Here are the proof rules we have so far: /\ intro: if F |- f1 and F |- f2 then F |- f1 /\ f2 /\ elim L: if F |- f1 /\ f2 then F |- f1 /\ elim R: if F |- f1 /\ f2 then F |- f2 => elim: if F |- f and F |- f => g then F |- g => intro: if F,f |- g then F |- f => g assump: f |- f weak: if F |- f then F,g |- f EXAMPLE 1. Prove (A /\ B) => A. 1. A /\ B |- A /\ B by assump. 2. A /\ B |- A by (1) and /\ elim. L 3. |- (A /\ B) => A by (2) and => intro. EXAMPLE 2. Prove (A /\ B) => (B /\ A). 1. A /\ B |- A /\ B by assump. 2. A /\ B |- B by (1) and /\ elim. R 3. A /\ B |- A by (1) and /\ elim. L 4. A /\ B |- B /\ A by (2), (3) and /\ intro. 5. |- (A /\ B) => (B /\ A) by (4) and => intro. EXAMPLE 3. Prove (A => B) => ((B=>C) => (A => C)). 1. A |- A by assump. 2. A => B, B => C, A |- A by (1) and weak. 3. A => B |- A => B by assump. 4. A => B, B => C, A |- A => B by (3) and weak. 5. A => B, B => C, A |- B by (2), (4) and => elim. 6. B => C |- B => C by assump. 7. A => B, B => C, A |- B => C by (6) and weak. 8. A => B, B => C, A |- C by (5), (7) and => elim. 9. A => B, B => C |- A => C by (8) and => intro. 10. A => B |- (B=>C) => (A => C) by (9) and => intro. 11. |- (A => B) => ((B=>C) => (A => C)) by (10) and => intro. That proof got kind of long, because we kept having to use assumption then weakening. It turns out we could introduce a new rule that combines the two: set assumption: F, f |- f This is an _admissible rule_, because it follows from the combination of some other rules. Let F = {f1, f2, ... fn}. 1. f |- f by assump. 2. f1, f |- f by (1) and weak. 3. f1, f2, f |- f by (2) and weak. ... n+1. f1, f2, ..., fn, f |- f by (n) and weak. Using this rule, we could shorten the above proof: 1. A => B, B => C, A |- A by set assump. 2. A => B, B => C, A |- A => B by set assump. 3. A => B, B => C, A |- B by (1), (2) and => elim. 4. A => B, B => C, A |- B => C by set assump. 5. A => B, B => C, A |- C by (3), (4) and => elim. 6. A => B, B => C |- A => C by (5) and => intro. 7. A => B |- (B=>C) => (A => C) by (6) and => intro. 8. |- (A => B) => ((B=>C) => (A => C)) by (7) and => intro. EXAMPLE 4. Prove ((S=>C) /\ O /\ ((O=>~C) /\ (C=>~O))) => ~S. Let F = (S=>C) /\ O /\ ((O=>(C=>false)) /\ (C=>(O=>false))), S 1. S |- S by assump. 2. F |- S by (1) and weak. 3. S=>C |- S=>C by assump. 4. F |- S=>C by (3) and weak. 5. F |- C by (2), (4) and => elim. 6. O |- O by assump. 7. F |- O by (6) and weak. 8. (O=>(C=>false)) /\ (C=>(O=>false)) |- (O=>(C=>false)) /\ (C=>(O=>false)) by assump. 9. F |- (O=>(C=>false)) /\ (C=>(O=>false)) by (8) and weak. 10. F |- O=>(C=>false) by (9) and /\ elim. L 11. F |- C=>false by (7), (10), and => elim. 12. F |- false by (5), (11), and => elim. 13. |- ((S=>C) /\ O /\ ((O=>(C=>false)) /\ (C=>(O=>false)))) => (S=>false) by (12) and => intro. twice 14. |- ((S=>C) /\ O /\ ((O=>~C) /\ (C=>~O))) => ~S by (13) and rewriting syntactic sugar for ~ MORE EXAMPLES * P => ~(~P) * P => (~P => Q) For the second of those, we need a new proof rule, which will be discussed in lecture next week: false elim: false |- f