Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >

Examplessmall logo

Examples -> ExternalSimplification -> sumofnsquared.html

Sum of the squares of the first n integers

This is another classical exercise in mathematical induction, similar in logical structure to the sum of the first n integers, but a bit more demanding in the algebra required in the induction step. You should read the commentary on first.

Here is the proof that Otter-lambda finds, with the Skolem term g(lambda(y,6*sum(z,z^2,0,y)=y* (y+1)* (2*y+1))) (and terms that differ only by renaming the bound variable) replaced by a constant c for readability:

6 [] sum(u,v,x,y+1)=sum(u,v,x,y)+Ap(lambda(u,v),1+y).
7 [] sum(u,v,x,x)=Ap(lambda(u,v),x).
10 [] x+1!=y+1|x=y.
11 [] -Ap(y,0)|Ap(y,g(y))|Ap(y,z).
12 [] -Ap(y,0)| -Ap(y,g(y)+1)|Ap(y,z).
14 [] 6*sum(x,x^2,0,n)!=n* (n+1)* (2*n+1).
15 [binary,14,12,demod,beta,7,beta,beta,6,beta,simplify] 6* (1+2* c+ c^2+sum(x,x^2,0, c))!= (1+ c)* (2+ c)* (3+2* c).
16 [binary,14,11,demod,beta,7,beta,beta,simplify] 6*sum(x,x^2,0, c)= (1+2* c)* (1+ c)* c.
26 [binary,15,10,simplify] 6* c^2+12* c+6*sum(z,z^2,0, c)!=2* c^3+9* c^2+13* c.
32 [para_into,26,16,simplify] $F.

The proof follows the same structure as the proof of It begins at steps 15, where in one step, lambda unification has identified the induction step to be proved, expanded "sum" using its definition in terms of lambda, and broken up the sum to n+1 into the sum to n and the last term. Note that, since this is a resolution proof, the equality to be proved occurs negated, so that the final result should be a contradiction. Similarly, in line 16 the induction hypothesis is identified. In step 26, simplification is used, a bit more powerfully than in Then we are in a position to use the induction hypothesis (by paramodulation from 16 into 26), and then simplification easily verifies the desired equality. Since that desired equality was negated, the penultimate form of the inequality is of the form x != x for some term x, which resolves with the equality axiom x=x to yield a contradiction.