next up previous
Next: Tuesday, March 21, 2000 Up: Lecture Notes Previous: Official List of Rules

Friday, March 17, 2000, completed Monday, March 20, 2000

Please note that there is a ``typo'' (an instance of mathematical
dyslexia) in problem 5 on the take-home exam.  The correct form of the
statement to be proved is

(Ex.Px->S) <-> ((Ax.Px)->S)  -- I transposed the first implication,
and implication, as we all know, is not commutative.

In the following proof I have used capital letters like Q, R, K, L to
suggest the use of ``lucky charms'' in the underlying formal argument.
The maneuver of assigning values to q and r in the existential
statements (Eqr.qx+r = 0 & (x=0 | r<x)) and (Eqr.qx+r = a' & (x=0 |
r<x)) in this proof is a mode of expressing an argument by existential

Division Theorem

We set out to prove the following theorem by induction:

(Axy.(Eqr.qx+r = y & (x=0 | r<x)))

We prove this by induction on y; I'm afraid I pulled this decision like
a rabbit out of a hat...

Basis step:  (Ax.(Eqr.qx+r = 0 & (x=0 | r<x)))

Let x be arbitrary.  Our aim is now to prove (Eqr.qx+r = 0 & (x=0 |
r<x)).  If we let q=0 and r=0, we have qx+r = 0x+0 = 0 (by axioms 3,5,
comm *) and (x = 0 | r < x) <-> (x=0 | 0<x) (by choice of r) which is
true by the trichotomy property of order: (x<0 | x=0 | 0<x) is an
instance of trichotomy, which simplifies to (x=0 | 0<x) because the
case x<0 is impossible (this last statement was proved in class -- I
will give the proof below).  We have proved the existential statement
by exhibiting values of the variables q and r which make it true, and
we have proved the universal statement because x was taken to be
arbitrary.  The proof of the basis step is complete.

Before commencing the induction step, we include the proof of
(Ax. ~x<0).  Let x be arbitrary.  Suppose for the sake of a
contradiction that x<0.  This means that we can choose K such that x +
K = 0, and moreover, it means that x =/= 0.  If we had K = 0, we would
have 0 = x + K = x + 0 = x, which is impossible, so we must have K =/=
0.  Since K is nonzero, it has a predecessor: we can choose L such
that L' = K.  Now 0 = x+K = x+L' = (x+L)' is impossible, because 0 cannot
equal any successor by axiom 1.  So the original assumption that x<0
cannot have been true, and since x is completely arbitrary we have proved
(Ax. ~x<0).

We resume the proof of the main theorem.

Induction step: We assume (Ax.(Eqr.qx+r = a & (x=0 | r<x))) (inductive
hypothesis); our goal is to prove (Ax.(Eqr.qx+r = a' & (x=0 | r<x))).

Let x be arbitrary.

By inductive hypothesis, we can introduce Q and R such that Qx+R = a
and x=0 | R<x. [in a formal proof, we would be introducing lucky
charms here]. The disjunctive premise x=0 | R<x suggests an argument by

Case 1: Suppose x = 0.  Then let q be anything you like and let r =
a'.  We have qx+r = q0 + a' = a' by axs. 3,5 and comm +.  Obviously we
have (x=0 | r<x).  So we have established the goal (Eqr.qx+r = a' &
(x=0 | r<x)) in case x=0.

A possibly confusing feature of our reasoning in case 1 is that we
never used the witnesses Q and R introduced above.  It does not seem
possible to avoid this in a simple way.

Case 2: Suppose R<x.  It has been observed in class that of course Qx
+ R' = a', meeting part of our goal, but the weakness of the choice q
= Q, r = R' is that we also need to establish (x = 0 | R' < x), and R'
< x might not be true!

We introduce a subsidiary argument by cases, using trichotomy.  By
trichotomy, either R' < x, R' = x, or x < R'.

subcase 1: Assume R' < x.  In this case we are done, following the
suggestion given above: set q = Q, r = R', and we have qx + r = (by
choice of q and r) Qx + R' = (by ax. 4) (Qx+R)' = (by choice of Q and
R) a', so we have qx + r = a', and we have x=0 | r<x, equivalent to
x=0 | R'<x, by hypothesis of subcase 1.  This establishes our goal qx
+ r = a' & (x=0|r<x).

subcase 2: Assume R' = x.  In this case we set q = Q' and r = 0.  qx+r
= (by choice of q and r) Q'x + 0 = (by ax. 3) Q'x = (by ax. 6) Qx + x
= (by hyp. of subcase 2) Qx + R' = (by ax. 4) (Qx + R)' = (by choice
of Q and R) a'.  We have x = 0 | r < x, equivalently x = 0 | 0 < x, by
choice of r, and we already saw how to prove this in the basis step.
This establishes our goal qx + r = a' & (x=0|r<x).  

subcase 3: Assume x < R'.  Our aim is to show that this case actually
does not occur.  Since x < R', there is K such that x + K = R', and
moreover x =/= R'.  If K = 0, we would have x = R', so K =/= 0.  Since
K=/= 0, there is L such that L' = K (K has a predecessor since it is
nonzero).  We then have x + L' = R', from which we have (x+L)' = R' by
ax. 4 and x+L = R by ax. 2.  From this it follows that x <= R.  From
x<=R and R<=x (a consequence of R<x, the hypothesis of the top level
case 2) we deduce x=R; but this contradicts the assumption R<x, so
this case in fact does not occur.

We have proved the goal qx + r = a' & (x=0|r<x) for suitable choices
of q and r in each possible subcase of case 2 (in fact, we could prove
it in the impossible subcase 3 as well, because anything follows from
a contradiction).  Thus, we have proved (Eqr.qx + r = a' & (x=0|r<x))
in case 2 (when R<x).

Since we have proved (Eqr.qx + r = a' & (x=0|r<x)) in both case 1 and
case 2, we have proved (Eqr.qx + r = a' & (x=0|r<x)) for any value of
x (since x was chosen arbitrarily) and so we have completed the proof
of (Ax.(Eqr.qx + r = a' & (x=0|r<x))), the goal of the induction step.

Randall Holmes