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

Wednesday, March 9, 2000

Hints for Homework 8:

Don't use multiplication; put everything into terms of addition and
successor.

Introducing New Predicates by Definition:

I give permission to define predicates.  If P is any formula in which
only x occurs free, we can introduce a new predicate symbol New_Predicate
with the defining axiom:

(Ax.New_Predicate(x) <-> P)

Notice that New_Predicate is a predicate symbol standing for the set
{x | P} already introduced:  New_Predicate(a) is equivalent to
a E {x|P}, because either is equivalent to P[a/x].

For example, we could define a predicate of ``being zero'' as follows:

Definition:

Is_Null(x) <-> x = 0

The same principles apply to defining multi-place predicates:

Definition of Order:

x <= y <-> (Ez.x+z=y)

This definition of the symbol <= is valid because the only free
variables in the formula (Ez.x+z=y) are x and y and <= is a new symbol
(in the Watson environment I have to use =< for this relation because
<= is reserved for reverse theorem application :-( )

Similar rules apply to introducing new constants and function symbols
by definition.  Mr. Guha asked about recursive definitions; we will
see later that we can justify recursive definitions, but they take a
little extra work.

Proofs in Class

The rest of our time on Wednesday was spent doing proofs on the board.
I wrote up the following facts that we know:

Axioms:

1. (Ax. x' =/= 0)
2. (Axy. x'=y' -> x=y)
3. (Ax. x+0=x)
4. (Axy. x+y' = (x+y)')
5. (Ax. x*0 = 0)
6. (Axy. x*y' = x*y + x)

Definitions:

1. 0'=1 (and so forth)
2. x=/=y is defined as ~(x=y) (notice that this is allowed by our rules
                              of definition above)

Theorems:

1. (Ax.x' = x+1)  (On the basis of this theorem, I allow you to use
             the notations x' and x+1 interchangeably without comment)
2. (Ax.x+y=y+x)   

I exhibit the proofs given in class.  These give examples of the kinds
of abbreviated justifications (and reductions of numbers of lines) that
are being allowed.

Theorem 3:  (Ax.x' =/= x)

Prove this by induction on x.

Goal (basis step): 0' =/= 0

1.  0' =/= 0        axiom 1, univ elim

| 2.  a' =/= a      ind hyp
| Goal:  a'' =/= a'
| | 3.  a'' = a'    subpremise for neg intro
| | 4.  a' = a      axiom 2, univ elim twice, m.p.
| | 5.  a'=a & a'=/=a c.i. lines 2,4
| 6. a'' =/= a'     neg intro lines 3-5

7. (Ax.x' =/= x)    math induction, 1, 2-6

This is the first proof where we have brought Theorem 2 into play.
Notice that we treat x=/=y logically exactly as if it were ~(x=y);
we omit formal appeals to the definition of =/=.

Theorem 4:  (Axyz.x+z=y+z -> x=y)

Notice that the converse implication is true by properties of equality,
so we could prove the biconditional instead with very little more work.

We prove this by induction on z.

| 1.  a=a, b=b  arbitrary object intro
| Goal: (Az.a+z=b+z->a=b)

Prove this by induction on z.  Notice that we do the induction proof
inside the outermost box (a univ intro box); there was some confusion
about this in class.

| Goal (basis): a+0=b+0 -> a=b
| 2. a+0=b+0 -> a=b     axiom 3 with univ elim, twice; prop =; 
|                        obvious propositional tautology
| | 3. a+c=b+c -> a=b   ind hyp
| | Goal:  a+c'=b+c' -> a=b  
| | | 4.  a+c'=b+c'      subpremise for imp. intro.
| | | 5.  (a+c)' = (b+c)' axiom 4, univ. elim., prop. =
| | | 6.  a+c=b+c        axiom 2, univ. elim.
| | | 7.  a=b            ind. hyp (line 3), line 6, m.p.
| | 8. a+c'=b+c' -> a=b  imp. intro. lines 4-7
| 9. (Az.a+z=b+z->a=b)   math. induction lines 2,3-8
10. (Axyz.x+z=y+z -> x=y)  multiple univ. intro., lines 1-9

Comments:  in line 2, we allow a line to be justified by the fact that
it is an obvious propositional tautology; this is an allowed move henceforth.

The proof by ``multiple univ. intro'' can easily be unpacked into two
proofs by univ intro -- we need to open two nested boxes with separate
arbitrary object intro lines, then put the quantifiers back on one at
a time.

| a=a, b=b          arbitrary object intro
| .
| .
| .
| Pab               who knows how?
(Axy.Pxy)           multiple univ. intro.

is an abbreviation for

| a=a               a.o.i.
| | b = b           a.o.i.
| | .
| | .
| | .
| | Pab             who knows how?
| (Ay.Pab)          univ. intro.
(Ax.(Ay.Pxy)) (equivalently, (Axy.Pab)) univ. intro.

We allow ourselves henceforth to introduce many arbitrary objects in a
single box for a proof of a statement with many leading universal
quantifiers.

A comment on the box in the math induction derived rule:

We know if we look at how the rule was derived that the box

| Pa
|.
|.
|.
| Pa'

in a math induction proof comes from the proof of the
sentence (Ax.Px->Px') which our abbreviated format allows 
us to avoid writing down.

In fact, this is a valid derived rule we might want to
use on other occasions:

| Pa
| .
| .
| .
| Qa
(Ax.Px->Qx)

where a occurs only in the box, is valid reasoning, as we see
if we pretty up the packaging a bit:

Goal:(Ax.Px->Qx)
| a=a     arbitrary object intro
| Goal: Pa -> Qa
| | Pa
| | .
| | .
| | .
| | Qa
| Pa -> Qa    imp. intro. previous box
(Ax.Px->Qx) previous box

On this basis, we allow reasoning like this:

| Pa
| .
| .
| .
| Qa
(Ax.Px->Qx)   universal implication introduction (uii) prev. box.

where a is a new variable (it does not occur outside the box).  Just
as in the math induction rule, we will use Greek letters for the new
object, because it was an arbitrary object in the original reasoning.



Randall Holmes
2000-05-05