next up previous
Next: Tuesday, March 7, 2000 Up: Lecture Notes Previous: March 3, 2000

Monday, March 6, 2000

Notes on the in-class conversation:

It is important to remember two little mottoes:

1. A negative hypothesis can be used in two ways:  one either
uses it for disjunction elimination (disjunctive syllogism)
or one uses it as part of a contradiction (in either neg. intro.
or neg. elim.)

2. When in doubt as to how to prove a statement P, try proving ~~P.

I PROMISE to include solutions to the first page of Homework 7
in the notes (after a decent interval to allow stragglers to turn
it in).

Induction, Continued

I decided not to do the formal proof of Theorem 2 above (every nonzero
number has a predecessor) but instead to go ahead and do the more natural
proof of commutativity of addition.  We got as far as proving the
basis step on the 6th, and that's how much I'll write up here.

Here I repeat myself from the part of the March 3 notes not covered in
class:

Since math induction is an important form of proof, we introduce a derived 
rule:

0 E P 

(Ax.x E P -> x' E P)

---------------------  mathematical induction, set form

(Ay.y E P)

which will allow the omission of the tedious (and often rather long!)
lines n+i+1 and n+i+2

or the following form without set notation:

P[0/z]                  

(Ax.P[x/z] -> P[x'/z])

-----------------------  mathematical induction, property form

(Ay.P[y/z])

This is proved by replacing the set P in the set form with the set
notation {x | P[x/z]} and appealing to the definition of set notation.

Although we stated the math induction axiom in terms of sets, we
will initially work with the property-based derived rule.  We will 
come back to what induction has to say about sets when we talk about
such things as the Least Number Principle.  Always remember when
we DO use set notation that (for the time being) sets are just aliases
for predicates.

There is a form of math induction with a box, which I now introduce
(it was also discussed in the out-of-class portion of the March 3 notes):

n. P[0/z]            ???  (basis step proved)

| n+1. P[a/z]             subpremise (inductive hypothesis)
| .
| .
| .
| n+i. P[a'/z]       ???

n+i+1.  (Ax.P[x/z])       math induction, n, (n+i)-(n+i)

where a does not occur outside the box.

The reason that this works is that the box can be replaced by two 
boxes as follows:

n. P[0/z]            ???  (basis step proved)

Goal: (Ax.P[x/z]->P[x'/z])
| n+(1/2). a=a                     arbitrary object intro
| Goal:  P[a/z] -> P[x'z]
| | n+1. P[a/z]             subpremise (inductive hypothesis)
| | .
| | .
| | .
| | n+i. P[a'/z]       ???
| n+i+1. P[a/z]->P[a'/z]    imp. intro. lines (n+1)-(n+i)

n+i+1.  (Ax.P[x/z]->P[x'/z]) univ. intro. lines (n+(1/2))-n+i+1
n+i+2   (Ay.P[y/z])          math induction (property form) lines n, n+i+1

We'll see both forms of the proof of the basis step of the commutative law.

Now for the main event.

Theorem 3:  (Ax.(Ay.x+y = y+x))

Goal: (Ax.(Ay.x+y = y+x))

This breaks into two subgoals, the familiar basis step and induction
step.

Goal: (Ay.0+y=y+0)

Goal: (Az.(Ay.z+y=y+z)->(Ay.z'+y=y+z'))

It is important to recognize that the induction axiom, unlike the basic
rules of the propositional and predicate logic, introduces subgoals
which are actually more complex than the statment to be proved.  This
is a reason for the mathematical power of this axiom, but of course
it also makes proofs using it more complex...

The rest of the notes for Monday are occupied by the proof of the
basis step:

Goal: (Ay.0+y=y+0)

We prove this goal by induction as well!

Goal (basis step): 0+0=0+0

1. 0+0=0+0  (properties of equality)

We will relax our formality in certain respects as we go on.
One feature is that we avoid explicit reference to the equality
rules where possible.

Goal (induction step): (Az.0+z=z+0 -> 0+z'=z'+0)

We open a box for univ. intro.

| 2.  a=a                  arbitrary object intro
| Goal: 0+a=a+0 -> 0+a'=a'+0

We open a box for imp. intro.

| | 3. 0+a=a+0             subpremise
| | Goal: 0+a' = a'+0
| | 4. 0+a' = (0+a)'       axiom 4, univ. elim.
| | 5. 0+a = (a+0)'        line 3, prop =
| | 6. 0+a = a'            axiom 3, univ. elim., line 5, prop =

The justification here allows us to eliminate the ``obvious'' line a+0
= a (an instance of axiom 3) and an application of equality
elimination using the omitted line and line 5.

| | 7. 0+a = a'+0          axiom 3, univ. elim., line 6, prop =

Similar to the previous line.  We are now done.

| 8. 0+a=a+0 -> 0+a'=a'+0  imp. elim. lines 3-7
9. (Az.0+z=z+0 -> 0+z'=z'+0)  univ. intro. lines 2-8
10. (Ay.0+y=y+0)           math. induction (property form) lines 1,9

Here we have not used the form of the math induction rule with a box
described above.  We demonstrate how the proof can be abbreviated:

Goal: (Ay.0+y=y+0)

We prove this goal by induction as well!

Goal (basis step): 0+0=0+0

1. 0+0=0+0  (properties of equality)

We open a box for the induction step (a casualty of abbreviation 
is that this proof has no line 2).

| 3. 0+a=a+0             inductive hypothesis
| Goal: 0+a' = a'+0
| 4. 0+a' = (0+a)'       axiom 4, univ. elim.
| 5. 0+a = (a+0)'        line 3, prop =
| 6. 0+a = a'            axiom 3, univ. elim., line 5, prop =
| 7. 0+a = a'+0          axiom 3, univ. elim., line 6, prop =

which is our goal.

10. (Ay.0+y=y+0)           math. induction lines 1,3-7.

This is clearly more economical, and we should be able to see from
the more verbose proof above why this form of proof is valid.



Randall Holmes
2000-05-05