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