I have a homework assignment that has made my head hurt for the past several days. I found no explanation on the materials provided by the Professor on this matter. I'm given:
$$
sum: \mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}\\
\begin{align}
s1&:sum(0, y)=y\\
s2&:sum(x+1, y)=sum(x,y)+1
\end{align}
$$
And the Prof. wants me to prove that $\forall x,y\in\mathbb{N}:sum(x,y)=sum(y,x)$.
My induction basis is $P(0)=sum(0, y)=sum(y,0)$, which, by commutativity, is valid.
My induction hypothesis: $HI:sum(x,y)=sum(y,x)$.
I really am stuck. Any and all help is greatly appreciated! Not even the Isabelle proofer could help me figure this out…
Best Answer
You can do induction within induction.
What I mean is, since the claim to be proved is $\forall x \ \forall y \ sum(x,y) = sum(y,x)$, you can set up the 'outer' inductive proof on variable $x$ as:
Base: Show that $\forall y \ sum(0,y) = sum(y,0)$
Step: Let $n$ be some arbitrary number, and show that if $\forall y \ sum(n,y) = sum(y,n)$, then $\forall y \ sum(n+1,y) = sum(y,n+1)$
Now, to show the Base $\forall y \ sum(0,y) = sum(y,0)$ of this outer induction, you can;t just say, as you do, 'by commutativity'. In fact, some sort of commutativity is the very thing we are proving over and over here. Anyway, to prove this, we can do induction on the variable $y$:
'Base's Base': Show that $sum(0,0)=sum(0,0)$
'Base's Step': Let $m$ be some arbitrary number, and show that if $sum(0,m) = sum(m,0)$, then $sum(0,m+1) = sum(m+1,0)$
Likewise, to prove the 'outside' Step (if $\forall y \ sum(n,y) = sum(y,n)$, then $\forall y \ sum(n+1,y) = sum(y,n+1)$) we can use induction. To be specific, once we have assumed that $\forall y \ sum(n,y) = sum(y,n)$, we can show that $\forall y \ sum(n+1,y) = sum(y,n+1)$ by induction on the $y$:
'Step's Base': Show that $sum(n+1,0) = sum(0,n+1)$
'Step's Step': Let $m$ be some arbitrary number, and show that if $sum(n+1,m) = sum(m,n+1)$, then $sum(n+1,m+1) = sum(m+1,n+1)$