next up previous
Next: Friday, February 11 Up: Lecture Notes Previous: Monday, February 7 and

Wednesday, February 9

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



Randall Holmes
2000-05-05