We discussed annotating proofs with goal statements (which I have already done (anachronistically) in the notes for the last two days. The idea is to signal at the heads of proofs and subproofs where we are trying to go. A goal statement often suggests a proof structure (and further goals) by its top propositional connective. This is analogous to commenting a computer program to tell the reader what it is going to do. For example, Proof structure for implication: Goal: P -> Q | n. P (premise of subproof) | Goal: Q | . | . | . | n+i. Q ??? n+i+1. P->Q (implication introduction, lines n-(n+i)) If we add a derived rule, we can have another proof structure for implication: G, ~Q |- ~P ------------ contrapositive implication introduction P -> Q derivation of this rule: | n. ~Q premise of subproof | . | . | . | n+i. ~P ??? n+i+1. ~Q -> ~P implication introduction, lines n-(n+i) | n+i+2. P premise of subproof | | n+i+3. ~Q premise of subsubproof | | n+i+4. ~P modus ponens, lines n+i+2, n+i+3 | | n+i+5. P & ~P c.i. lines n+i+2, n+i+4 | n+i+6. ~~Q neg. intro, lines n+i+3-n+i+5 | n+i+7. Q d.n.e. line n+i+6 n+i+8. P->Q imp.intro. lines n+i+2-n+i+7 Proof structure for implication (contrapositive): Goal: P -> Q | n. ~Q (premise of subproof) | Goal: ~P | . | . | . | n+i. ~P ??? n+i+1. P->Q (contrapositive implication introduction, lines n-(n+i)) Proof structure for conjunction: Goal: P & Q Goal: P . . . n. P ??? Goal: Q . . . n+i. Q ??? n+i+1. P & Q conj. intro, lines n,n+i Proof structure for negation: Goal: ~P | n. P (premise of subproof) | Goal: contradiction | . | . | . | n+i. Q & ~Q ??? n+i+1. ~P (negation introduction, lines n-(n+i)) Proof structure for disjunction (two kinds): Goal: P | Q | n. ~Q (premise of subproof) | Goal: P | . | . | . | n+i. P ??? n+i+1. P | Q (disj. intro, lines n-(n+i)) OR Goal: P | Q | n. ~P (premise of subproof) | Goal: Q | . | . | . | n+i. Q ??? n+i+1. P | Q (disj. intro, lines n-(n+i)) Proof of anything, by contradiction: Goal: P Goal: ~~P | n. ~P (premise of subproof) | Goal: contradiction | . | . | . | n+i. Q & ~Q ??? n+i+1. ~~P neg. intro. lines n-(n+i) n+i+2. P double negation elimination, line n+i+1. Proof of anything, by cases: Goal: P n. Q & ~Q (excluded middle) Goal: Q -> P . (supply proof structure from above) . . n+i. Q -> P Goal: ~Q -> P . (supply proof structure from above) . . n+i+j. ~Q -> P n+i+j+1. P proof by cases, lines n, n+i, n+i+j. (Grantham's disj. elim.) Notice that the Goal: lines do not have numbers; they are not part of the formal structure of the proof. Goals don't necessarily come from these structures: for example, if one has a premise P | Q and one wants to prove Q, one can adopt ~P as a new goal (planning to apply disjunction elimination to get the desired conclusion Q. n. P | Q ??? Goal: Q Goal: ~P (so that disj.elim. can be applied with line n) . (proof structure for a negation can be supplied from above). . . n+i. ~P ??? n+i+1. Q disj. elim, lines n, n+i A Sample Proof (we did the first half in class): (A & B) | (A & C) |- A & (B | C) 1. (A & B) | (A & C) premise Goal: A & (B | C) because this goal is a conjunction, it breaks naturally into two subgoals, A and B | C. Goal: A We prove this goal by contradiction, which gives a new goal ~~A. Goal: ~~A | 2. ~A Goal: contradiction We have the premise (A & B) | (A & C), which is a disjunction. Our strategy is to disprove A & B, allowing us to prove A & C, (which will also lead to trouble. This motivates Goal: ~(A&B) (so that disj. elim. can be applied with line 1) | | 3. A & B | | Goal: contradiction | | 4. A by c.e. line 3 | | 5. A & ~A by c.i. lines 4,2 | 6. ~(A&B) negation introduction, lines 3-5 | 7. A&C disj.elim. lines 1,6 | 8. A by c.e. line 7 | 9. A & ~A by c.i. lines 8,2 10. ~~A by negation introduction, lines 2-9 11. A by d.n.e. line 10 Goal: B|C (this is the second subgoal from the proof of the overall goal) Use disjunction introduction (either disjunct works -- the problem is symmetrical). | 12. ~B premise of subproof | Goal: C Our strategy uses the disjunctive premise in a similar way to its use in the proof of the first subgoal. | Goal: ~(A&B) (for an application of disj. elim. with line 1) | | 13. A & B premise of subsubproof | | Goal: contradiction | | 14. B by c.e. line 3 | | 15. B & ~B by c.i. lines 14,12 | 16. ~(A&B) negation introduction, lines 13-15 | 17. A&C by disj. elim. lines 1, 16 | 18. C by c.e. line 17. 19. B | C by disj intro, lines 12-18. 20. A & B|C by c.i., lines 11, 19