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)))