Bernoulli's Inequality
This is the inequality
1 + na ≤ (1+a)n if -1 < a.
Otter-lambda successfully proves this by induction on n. This example is of particular interest for several reasons:
(i) It involves two types: reals and natural numbers. In order to formulate this theorem in such a way that the axioms can be correctly typed, so that the soundness theorems about implicit typing will apply, we must use a function symbol i for an injection i: N-> R. We use o for the zero in N and 0 = i(o) for the zero in R.
Technically, if we want the soundness theorem to apply a priori to any proof that Otter-$\lambda$ might find, we should not use 0 at all, but only i(o); and indeed if we make that replacement, the proof will still be found; but we can also simply observe that if we do use 0, the proof that is found is in fact correctly typed.
(ii) It offers an interesting interplay between algebra performed by MathXpert (external simplification) and algebra performed in the clausal search system, since at some point a law of exponents has to be used in the opposite direction from which simplification uses it. This is performed by demodulation.
(iii) Simplification is performed not only on terms of type N or R, but also on terms of type ``proposition'', specifically inequalities.
Here is the proof, with the Skolem term g(lambda(x,a*i(x)+1<= (a+1)^{}x)) replaced by a constant c for readability.
2 [] x<=x.
3 [] x+1!=0.
7 [] -ap(y,o)|ap(y,g(y))|ap(y,z).
8 [] -ap(y,o)| -ap(y,s(g(y)))|ap(y,z).
10 [] -(x<y)| -(z<=x)|z<y.
12 [] -(x<=y)| -(y<x).
13 [] 0<a+1.
17 [] -(x<=y)| -(0<z)|z*x<=y*z.
19 [] -(x<y)|x+ -y<0.
22 [] x^o=1|x=0.
23 [] 0<=i(x).
25 [] i(o)=0.
26 [] i(s(x))=i(x)+1.
27 [] x^s(y)=x*x^y.
28 [] x*0=0.
30 [] 0+x=x.
33 [] x^ (y+z)=x^y*x^z.
34 [] x^1=x.
35 [] -(1+i(n)*a<= (1+a)^n).
36 [simplify,35] (a+1)^n<a*i(n)+1.
41 [binary,36,12] -(a*i(n)+1<= (a+1)^n).
43 [binary,41,8,demod,beta,25,28,30,beta,26,27]
-(1<= (a+1)^o)| -(a* (i(c)+1)+1<= (a+1)* (a+1)^c).
44 [binary,41,7,demod,beta,25,28,30,beta]
-(1<= (a+1)^o)|a*i(c)+1<= (a+1)^c.
85 [para_into,43,22,unit_del,2,3]
-(a* (i(c)+1)+1<= (a+1)* (a+1)^c).
117 [para_into,44,22,unit_del,2,3]
a*i(c)+1<= (a+1)^c.
119 [hyper,117,17,13]
(a+1)* (a*i(c)+1)<= (a+1)^c* (a+1).
160 [para_into,43,22,unit_del,2,3,simplify,85,demod,33,34]
(a+1)^c* (a+1)<a*i(c)+a+1.
298 [hyper,119,10,160]
(a+1)* (a*i(c)+1)<a*i(c)+a+1.
299 [binary,298,19]
(a+1)* (a*i(c)+1)+ -(a*i(c)+a+1)<0.
398 [binary,298,19,simplify,299]
and(a!=0,i(c)<0).
404 [split and,398]
i(c)<0.
412 [binary,404,12]
-(0<=i(c)).
413 [binary,412,23] $F.
Let us go over this proof. First (at 36), the negated goal is simplified to an inequality. The next two steps, 43 and 44, represent the "decision" to attempt to prove this inequality by induction. The next two steps take care of the base case, so that 85 and 117 are recognizable as the induction step and the induction hypothesis, respectively. Hypothesis 17 says that we can multiply both sides of an inequality by the same positive quantity; line 119 is deduced by applying that, using the positive quantity a+1. Line 160 is deduced from line 43 much as 117 was, but going further: the law 33, that is, x^{y+z} = x^y * x^z, is applied. Simplification uses this law in the right-to-left direction, so 160 would never be deduced by simplification alone; here it is deduced by using 33 as a demodulator. This is an important interplay between simplification (which has a tendency to be unidirectional, like demodulation) and the clausal-search mechanism, which can accumulate various equivalent forms of an expression. Once 160 is derived, trichotomy (10) and 119 give us 298, and subtracting the same term from both sides we get 299, which is
(a+1)* (a*{i(c)} + 1) - (a*i(c) + a + 1) < 0.
This simplifies to a conjunction: a ≠0 and i(c) < 0. Incidentally, I think one might wait a long time for this conclusion to come out without external simplification, using only paramodulation and demodulation! This conjunction is at first represented at the object level in Otter-lambda as a term with functor and (line 398). But Otter-lambda has an inference rule called {\tt split and}, which converts a clauseand(P,Q) | R
to two clauses P | R and Q | R. This rule
gives special meaning to the functor and. It is necessary because the mechanism for calling external simplification returns a single clause, not several clauses. After the use of "split and", the proof completes immediately, since the hypothesis that i maps integers to nonnegative reals has been contradicted.