We will give two proofs of the theorem that the sum of the even numbers from 0 to 2×n is given by the formula (n+1)×n (for example, when n=3, we find 0+2+4+6=12=(3+1)×3). First will be a semi-formal proof in a mixture of words and symbols, which is essentially the proof that would be found in a math text. The other proof will be a completely formal, symbolic proof in Peano Arithmetic; you should compare the structure of the two proofs to see how the formal system relates to more common practice. We will use the notation S(i=0,n) a{i} for the iterated sum a{0}+a{1}+...+a{n}; the necessary axioms for this operation are
We will also freely use the numerals 0, 1, 2, ..., instead of the terms 0, 0', 0'', ..., to improve readability.
\begin{thm} The sum of the even numbers from 0 to 2×n, which may be expressed as S(i=0,n) 2×i, is equal to (n+1)×n. \end{thm} \begin{pf} We proceed by induction on n. For the base case, we need to show that S(i=0,0) 2×i=(0+1)×0. By the definition of iterated sum, the left side is just 2×0, which equals 0; the right side is also 0, so the base case is established. For the inductive case, we assume that S(i=0,n) 2×i=(n+1)×n holds for some number n, and we need to show that also S(i=0,n') 2×i=(n'+1)×n'. This is established by the following chain of equalities: \[ \begin{array}{rcll} S(i=0,n') 2×i & = & (S(i=0,n) 2×i)+2×n' & \textrm{(def. of S)} & = & (n+1)×n+2×n' & \textrm{(induction hypothesis)} & = & (n+1)×n+(n+1)×2 & \textrm{(commutativity, def. of +)} & = & (n+1)×(n+2) & \textrm{(distributivity)} & = & (n'+1)×n' & \textrm{(commutativity, def. of +)} \end{array} \] \end{pf} \begin{derivation}{\seq{}{S(i=0,n) 2×i=(n+1)×n}} & (1) & S(i=0,0) 2×i=(0+1)×0 & \TI{1, below} & (2) & (S(i=0,n) 2×i=(n+1)×n)\impl (S(i=0,n') 2×i=(n'+1)×n') & \TI{2, below} & (3) & S(i=0,n) 2×i=(n+1)×n & 1,2\IND \end{derivation} \begin{enumerate} \item Base case: \begin{derivation}{\seq{}{S(i=0,0) 2×i=(0+1)×0}} & (1) & S(i=0,0) 2×i=2×0 & \textrm{SUM0} & (2) & 2×0=0 & \MULT0 & (3) & (0+1)×0=0 & \MULT0 & (4) & 0=(0+1)×0 & 3\SYMM & (5) & 2×0=(0+1)×0 & 4,2\SUBST & (6) & S(i=0,0) 2×i=(0+1)×0 & 5,1\SUBST \end{derivation} \item Inductive case: \begin{derivation}{\seq{}{(S(i=0,n) 2×i=(n+1)×n)\impl (S(i=0,n') 2×i=(n'+1)×n')}} 1 & (1) & S(i=0,n) 2×i=(n+1)×n & \A & (2) & S(i=0,n') 2×i=(S(i=0,n) 2×i)+2×n' & \textrm{SUM1} 1 & (3) & S(i=0,n') 2×i=(n+1)×n+2×n' & 1,2\SUBST & (4) & 2×n'=n'×2 & \TIS{\seq{}{a×b=b×a}} & (5) & n+1=(n+0)' & \PLUS1 & (6) & n+0=n & \PLUS0 & (7) & n+1=n' & 6,5\SUBST & (8) & n'=n+1 & 7\SYMM & (9) & 2×n'=(n+1)×2 & 8,4\SUBST 1 & (10) & S(i=0,n') 2×i=(n+1)×n+(n+1)×2 & 9,3\SUBST & (11) & (n+1)×(n+2)=(n+1)×n+(n+1)×2 & \TIS{problem 3} & (12) & (n+1)×n+(n+1)×2=(n+1)×(n+2) & 11\SYMM 1 & (13) & S(i=0,n') 2×i=(n+1)×(n+2) & 12,10\SUBST & (14) & (n+1)×(n+2)=(n+2)×(n+1) & \TIS{\seq{}{a×b=b×a}} & (15) & n+2=(n+1)' & \PLUS1 & (16) & n+2=n'' & 7,15\SUBST & (17) & n'+1=(n'+0)' & \PLUS1 & (18) & n'+0=n' & \PLUS0 & (19) & n'+1=n'' & 18,17\SUBST & (20) & n''=n'+1 & 19\SYMM & (21) & n+2=n'+1 & 20,16\SUBST & (22) & (n+1)×(n+2)=(n'+1)×(n+1) & 21,14\SUBST & (23) & (n+1)×(n+2)=(n'+1)×n' & 7,22\SUBST 1 & (24) & S(i=0,n') 2×i=(n'+1)×n' & 23,13\SUBST & (25) & (S(i=0,n) 2×i=(n+1)×n)\impl (S(i=0,n') 2×i=(n'+1)×n') & 1,24\CP