Since I'll be out of town next Monday, our Honors Seminar won't meet next week. But to avoid losing too much time, I'd like to offer the following exercise. Recall the system of Peano Arithmetic I defined in class this Monday: it has one constant symbol ("0"), one unary function symbol ("s(...)"), all the usual axioms for equality, axioms for all instances of tautologies (i.e. for any valid formula of PROPOSITIONAL logic with k propositional variables, and any sequence of predicate-logic formulae A_1, A_2,...,A_k, the formula produced by replacing all instances of p with A_1, all instances of q with A_2, etc.), and an extra axiom scheme for induction: for any formula A with free variable x, (A(0) ^ (forall y)(A(y) -> A(s(y)))) -> (forall y)A(y) where "A(0)", "A(y)", and "A(s(y))" mean the formula A with all free occurrences of "x" replaced by "0", "y", or "s(y)" respectively. Now let's add another, binary, function symbol "f(...,...)" and the axioms (forall x)(f(x,0) = x) and (forall x)(forall y)(f(x,s(y))=s(f(x,y))) (This function symbol is supposed to represent addition, but you don't know that yet. :-) Exercise: prove that addition is commutative, i.e. (forall x)(forall y)(f(x,y) = f(y,x)) Hint: I did this by induction on x, and I don't see any other way to do it. To do the induction on x, we need to first prove (forall y)(f(0,y) = f(y,0)) which itself seems to require an induction on y. We also need to prove (forall y)((f(x,y)=f(y,x)) -> (f(s(x),y)=f(y,s(x)))) which I did by forall-introduction from (f(x,y)=f(y,x)) -> (f(s(x),y)=f(y,s(x))) which I got by assuming f(x,y)=f(y,x), proving f(s(x),y)=f(y,s(x)), and discharging the assumption. Even with the assumption f(x,y)=f(y,x), I was unable to get f(s(x),y)=f(y,s(x)) without using yet another induction to prove (forall y)(f(x,y)=f(y,x) -> f(s(x),y)=f(x,s(y))) All of this adds up to a long, complicated proof, especially if you do it as formally as I did in class on Monday. If you finish the whole thing, great! but I'll only ASK you to do one induction, rather than three: either a) prove (forall y)(f(0,y)=f(y,0)) or b) prove (forall y)(f(x,y)=f(y,x) -> f(s(x),y)=f(x,s(y))) (which, since you proved it without assuming anything special about x, immediately gives (forall x)(forall y)(f(x,y)=f(y,x) -> f(s(x),y)=f(x,s(y))) by the forall-introduction rule) or c) given both of the above, prove (forall x)(forall y)(f(x,y)=f(y,x)) If you're REALLY a glutton for punishment, you might (after completing this proof) go on to prove that every number is either even or odd, i.e. (forall x)(exists y)(x=f(y,y) v x=s(f(y,y)))