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