18a Presentation

Mouctar Diallo

Prove by induction that +:N×N→N is commutative (∀m,n,m+n=n+m) and satisfies cancellation (∀m,n,p,m+p=n+p if and only if m=n).

rules we can use

(#1) n+0=n
(#2) n+succ(m)=succ(n+m)

Proof by induction

induct on n
WTS| m+0=0+m
induct on m
WTS| 0+0=0+0
anything is equal to itself —> statement is true, reflexive property of equality, equal introduction
IH|m+0=0+m
IS| WTS| succ(m)+0=0+succ(m)
0+succ(m)
=succ(0+m)(#2)
=succ(m+0)(IH)
=succ(m)(#1)
=succ(m)+0(#1)
we proved right side is equal to the left side
IH|m+n=n+m
IS| WTS| m+succ(n)=succ(n)+m
induct on m
IH| m+succ(n)=succ(n)+m
IS| WTS| succ(m)+succ(n) = succ(n)+succ(m)
succ(n)+succ(m)
=succ(succ(n)+m)(#2)
=succ(m+succ(n))(IH)
=succ(succ(m+n))(#2)
=succ(succ(n+m))(IH)
=succ(n+succ(m))(#2)
=succ(succ(m)+n)(IH)
=succ(m)+succ(n)

by showing this we prove that
m+n=n+m

m+p=n+p iff m=n

proof by induction on p

base case m+0=n+0 iff m=n
m=n
IH| m+p=n+p iff m=n
IS| m+succ(p)=n+succ(p)
succ(m+p)=succ(n+p) (#2)
m+p=n+p RULE —> successor function is injective
m=n(IH)

page revision: 0, last edited: 18 Apr 2018 01:47