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 introduction. 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 cases. 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.