next up previous
Next: Solution to (part of) Up: Lecture Notes Previous: Friday, March 17, 2000,

Tuesday, March 21, 2000 (continued March 22)

Proof Strategy

I opened the lecture by asking the following question:

Given

Goal:  (Ax.Px) | S

and no special information about the context, write two following lines
of the proof with appropriate goals, opening boxes where necessary.

I suggested that this is the kind of question I might ask on an exam.

Here is my analysis:

Since the statement is a disjunction, and lacking information about
the context, we should expect to prove it by disjunction introduction.

This suggests that the following line should be either ~S or ~(Ax.Px):

Goal:  (Ax.Px) | S
| next line: ~S           subpremise for disj. intro.
| Goal: (Ax.Px)      

OR

Goal:  (Ax.Px) | S
| next line: ~(Ax.Px)          subpremise for disj. intro.
| Goal: S

Of these two alternatives, the second gives us no help on how to write
the next line (we might prefer it if the context contained additional
information, but in our current vacuum of context information it is not
appealing).  Neither the premise ~(Ax.Px) nor the goal S suggest anything
further without information from the context.

However, the goal (Ax.Px) in the first alternative suggests that we should
open a box for univ. intro:


Goal:  (Ax.Px) | S
| next line: ~S           subpremise for disj. intro.
| Goal: (Ax.Px)  
| | another line: a=a     arbitrary object intro
| | Goal: Pa

At this point we are helpless without more information from the context.

Exercise:  Compare this with what is likely to follow (Ax.Px | S).    

For the rest of the period, I discussed proof strategy, connective 
by connective.

For each connective, the ``introduction'' rule tells us how to prove a
goal with that connective as its top-level operation (in the in-class
example, it was important to recognize that the top level operation in
(Ax.Px) | S is NOT the universal quantifier but the disjunction, so it
is NOT appropriate to open a box with arbitrary object intro).  The
``elimination'' rule for a connective tells us how to use a previous
line with that connective.

Conjunction

A conjunctive goal

     Goal: A & B

simply breaks apart into two goals

     Goal: A
     Goal: B

suggesting the following proof pattern:

     Goal: A & B
     Goal: A

     (proof steps)

     line m:  A

     Goal: B

     (proof steps)

     line n: B

     line n+1: A & B   conjunction introduction, lines m,n

The typical method of using a conjunctive premise is very similar:

     line n:  A & B
     line n+1:  A
     line n+2:  B

Of course, the form of the context could suggest a quite different
strategy:

     line n-1: (A & B) -> C
     line n. A & B

suggests the quite different continuation

     line n+1: C     modus ponens lines n-1,n

Disjunction

A disjunctive goal

    Goal:  P | Q

can be proved in one of four ways.

If you can actually prove P or Q, you can prove P | Q this way:

     Goal:  P | Q
     Goal: P

     (proof steps)

     line n: P
     line n+1: P | Q    disj intro (Grantham)

OR

     Goal:  P | Q
     Goal: Q

     (proof steps)

     line n: Q
     line n+1: P | Q    disj intro (Grantham)

Notice that no box is introduced in either of these proof patterns.

A theorem which is a disjunction is unlikely to be proved in this way,
because we won't really be interested in a theorem of the form P | Q
if P itself is a theorem (or Q).  But this kind of proof of a disjunction
is likely to occur inside boxes where one has additional assumptions
available.

A top level proof of a disjunction is more likely to take one of the forms

     Goal:  P | Q

     | line m:  ~P     subpremise for disj. intro.
     | Goal: Q
     |
     | (proof steps)
     | 
     | line n: Q
     line n+1: P | Q   disj. intro. lines m-n

OR

     Goal:  P | Q

     | line m:  ~Q    subpremise for disj. intro.
     | Goal: P
     |
     | (proof steps)
     | 
     | line n: P
     line n+1: P | Q   disj. intro. lines m-n

It is useful to notice (I asked this as a question in class) that a box
like

     | line m:  ~P     subpremise
     | Goal: Q
     |
     | (proof steps)
     | 
     | line n: Q

can be used to prove P | Q by disj. intro, but can also be used to
prove (~P) -> Q by imp. intro.  It can be checked using truth tables
that P | Q is equivalent to (~P) -> Q.

I may ask questions in which I present a piece of a proof (like this
box) and ask what has been proved.

Implication

The picture for implication is fairly simple.

To prove a goal which is an implication we have usually used the
standard implication introduction rule:

     Goal: P -> Q
     | line m: P     subpremise for implication introduction
     | Goal: Q
     | 
     | (proof steps)
     |
     | line n: Q
     line n+1:  P->Q     implication introduction, lines m-n

This corresponds to a pattern in mathematical proofs stated in English:

Theorem:  P -> Q

Assume P.  Our goal is now to prove Q...(body of proof)...We have
proved Q under the assumption that P, so we have established that
P->Q.

To use a previous line which is an implication, we have implication
elimination, also called modus ponens:

P 

P -> Q

-------

Q

We have variations on both introduction and elimination based on the
equivalence of an implication P->Q with its contrapositive (~Q) ->
(~P):

the derived rule of modus tollens

~Q

P -> Q

--------

~P

has been used fairly often, and the following pattern of reasoning
does appear in the notes above, though we have not used it (or not often):

     Goal:  P->Q
     | line m: ~Q         subpremise for contrapositive introduction
     | Goal: ~P
     |
     | (Proof steps)
     |
     | line n: ~P
     line n+1:  P -> Q     contrapositive introduction, lines m-n

Finally, there are some ``trivial'' implication introduction rules:

~P
-------
P -> Q

Q
-------
P -> Q

These suggest that if one has 

     Goal: P->Q

it might sometimes be useful (especially if one is inside boxes with
additional hypotheses) to continue with

     Goal: ~P (for an application of false hypothesis)

or 

     Goal: Q (for an application of true conclusion)

But these are NOT the rules which are usually used to prove implications.

Existential Quantifier

It is very important to understand the difference between the strategy
to follow when one has an existential _premise_:

     line n:  (Ex.Px)

and the strategy to follow when one has an existential _goal_:

     Goal:  (Ex.Px)

When one has a goal (Ex.Px) one has to produce an object t, already
declared in the current environment, and prove Pt.  For example, if one
can prove P0, one can prove (Ex.Px) in arithmetic.

Proof pattern:

	Goal:  (Ex.Px)
        Goal: Pt  (where t is some specific already defined object)

        (proof steps)

        line n: Pt
        (Ex.Px)   existential introduction, line n

Notice that no box is introduced in this proof; t is not a ``locally
declared'' object, but a specific already definable object.  (One has
to come up with the right object somehow -- this is not always easy!)

If one has an existential hypothesis, one has quite a different pattern:

        line m:  (Ex.Px)

        Goal: X  (the structure of the goal isn't important here)
        | line n:  Pa      witness intro line n
        | Goal: X (the goal does not change)
        |
        | (proof steps)
        |
        | line p:  X
        line p+1: X      exist. elim. lines n-p

Here the object a is a ``lucky charm'', a witness to an existential statement.
It is locally declared inside the box (and does not occur in the goal X!)
Here the logical issue is that one is given an existential premise
(Ex.Px) but one is not told how to actually produce t such that Pt; the
existential elimination rule (with its witness intro subrule) allows us
to temporarily introduce such a t -- but we have to get rid of all mention
of it when we leave the box.

In English, there are proof patterns corresponding to these.

For existential introduction:  

Our aim is to prove (Ex.Px).  We set x=t... (body of proof) ... so we have
proved Px for the particular value t of x, establishing our goal (Ex.Px).

For existential elimination (with witness introduction):

Since we are given the hypothesis (Ex.P(x)), we may introduce an object
K  such that P(K) ...(body of proof)... having drawn the conclusion X
(not mentioning K) from the existence of K such that P(K), we conclude
that X follows from the hypothesis (Ex.Px).

You might want to look at the proof of the Division Theorem for examples
of both of these patterns of reasoning presented in English.

If one is proving an existential goal, one will not introduce a
``lucky charm'' related to that goal, but one _might_ want to
introduce a lucky charm related to some existential hypothesis.

line m:  (Ex.Qx)

Goal: (Ex.Px)

| line n:  Qa         witness intro line m
|
| (proof steps)
|
| line p: Pa            
| line p+1: (Ex.Px)   exist. intro. line p
line p+2: (Ex.Px)     exist. elim. line p+1

is a possible pattern of proof, in which we are somehow (using assumptions
not shown) able to prove that any witness to the hypothesis (Ex.Qx) that
we introduce will also turn out to be a witness to (Ex.Px).

(these notes aren't finished yet -- more to come on Universal
Quantifier and Negation, with final comments on indirect proof (proof
by contradiction)).

Universal Quantifier

The universal quantifier, like conjunction, usually seems to present
few difficulties.  It is important not to get confused by formulas
like (Ax.Px) | S in the class example -- this is not a universal
quantified statement at top level, so one should apply disjunction
introduction rules first.

Proof of a universal goal:

Goal: (Ax.Px)

| line m:  a = a     arbitrary object intro
| Goal: Pa
|
| (proof steps)
|
| line n:  Pa
line n+1: (Ax.Px)    univ. intro. lines m-n

This corresponds to the pattern of reasoning in English:

Our aim is to prove (Ax.Px).  Let x be arbitrary.  ...(body of
proof)...thus Px.  Since x was chosen arbitrarily, we can conclude
(Ax.Px).

On the other hand,

line m:  (Ax.Px)

(proof steps)

line n:  Pa

illustrates use of a universal premise.

In standard mathematical practice, explicit universal quantifiers are
often omitted: we usually express the commutative law of addition as
x+y = y+x rather than (Axy. x+y = y+x).

Negation

To prove a negated goal, we reason to a contradiction:

Goal: ~P

| line n:  P   subpremise for negation introduction
| Goal: contradiction
|
| (proof steps)
|
| Q & ~Q

Notice that the formula Q can be anything.

The use of negated premises is a more difficult matter.

The ``negation elimination'' rule (the ``official'' way to use
negative premises) looks like this:

P 

~P

----

Q

so we can deduce anything at all from a contradiction.  One thing we
can do with negation elimination is simplify the contradictions in
proofs by negation introduction.

Suppose we have a proof

Goal: ~P

| line m:  P   subpremise for negation introduction
| Goal: contradiction
|
| (proof steps)
| line x: Q
|
| line y: ~Q
|
| line n: Q & ~Q  c.i. lines x,y

~P neg. intro. lines m-n

Notice that we can use neg. elim. instead of c.i. in the last line
of the box to replace Q & ~Q with any contradiction Z & ~Z, and the proof
will still be valid:

Goal: ~P

| line m:  P   subpremise for negation introduction
| Goal: contradiction
|
| (proof steps)
| line x: Q
|
| line y: ~Q
|
| line n: Z & ~Z  neg. elim.  lines x,y

~P neg. intro. lines m-n

This can be useful if Q is very long.

A similar maneuver can be essential in this situation:

earlier line:  (Ex.Qx)

Goal: ~P

| line m:  P   subpremise for neg intro
| Goal: contradiction:
| | line m+1:  Qa  witness intro earlier line
| | Goal: contradiction
| | 
| | (proof steps)
| | 
| | line x:  Ra
| | 
| | (proof steps)
| | 
| | line y: ~Ra
| | line y+1:  Z & ~Z (Z just a propositional letter) neg. elim. lines x,y
| line y+2: Z&~Z       exist. elim. line y+1
line y+3: ~P           neg intro lines m-(y+2)

The problem with putting the obvious contradiction Ra & ~Ra on line y+1
is that you cannot copy it out of the ``witness box'' using exist elim,
because it mentions the lucky charm.

This is not a feature of mathematical reasoning in English, because we
simply say there is a contradiction rather than citing a specific one
in English.  This is purely a technical issue in the formal system
(and could be avoided -- for example, if we had ``false'' or
``contradiction'' as a formula we could use it as the conclusion in
neg. intro. boxes).

Hints for Using Negative Premises

The ``official'' ways to use negative premises are in negation
elimination (where along with ~P you also need P) and disjunction
elimination (where along with ~P you need P | Q).  A derived rule
which involves negation is modus tollens.

A common situation where a negative premise can be used is in 
a proof by negation introduction

earlier line:  ~Q

Goal: ~P
| n. P            premise for neg. intro.
| Goal: contradiction
| Goal: Q         (which will give a contradiction with the earlier line)
 etc.

Indirect Proof

When all else fails in the proof of a goal Q, we can resort to indirect
proof.  The proof strategy is easily summarized:

Goal: Q  (and we have no help from the structure of Q or earlier premises)
Goal: ~~Q  (attempt indirect proof of Q)
| m. ~Q     subpremise for negation introduction
| Goal: contradiction
| 
| (proof steps)
|
| n. R & ~R

n+1.  ~~Q     neg intro lines m-n
n+2.  Q       d.n.e. lines m-n

In general, we go for indirect proof where the internal structure of
the goal gives us no help.  In practice, this tends to mean that the
goals we prove indirectly will either be atomic sentences (with no
top-level connective to guide use of an introduction rule) or
existentially quantified sentences (Ex.Px) where we cannot produce a
goal Pt (there might be no objects t we know how to describe in the
environment, as in the first problem in Homework 7) In the latter
case, the informal approach (or the formal approach if we add a
suitable rule) would be to prove (Ex.Px) by introducing (Ax. ~Px) as a
hypothesis and reasoning to a contradiction (this uses the
``deMorgan'' equivalence between (Ax. ~Px) and ~(Ex.Px) as well as
double negation).

Anonymous Objects

A final point: it is permissible to introduce free variables into
proofs which are not arbitrary objects (``Greek curveballs'') or
witnesses (``lucky charms'').  We give an example:

1. (Ax.Px)     premise
2. Py          univ. elim. line 1
3. (Ex.Px)     exist. intro. line 2.

When we do this, we are appealing to the fact that our logic proves
that the universe is inhabited.  We had a discussion in class as to
whether such anonymous objects are more like ``Greek curveballs'' or
``lucky charms''; they are probably a bit more like lucky charms, but
they have universal scope (they do not live in a box).

I don't think that any proof requires anonymous objects, but some 
proofs can be shortened by using them.



Randall Holmes
2000-05-05