Online Otter-λ

Examples

Proof that a ≤ s(0) implies a = 0 | a = s(0) in PA, using the definition of ≤ in terms of existence.

One should read the commentaries on le.in and le2.in before reading this one.

This is another illustration of the use of "exists" in lambda logic. It is similar to le2.in but more difficult, and the Otter-lambda proof is hard to understand. An informal proof might proceed as follows: since a ≤ s(0) we have a + u = s(0) for some u. Prove by induction on u that a + u ≠ s(0) unless a = 0 or a = s(0). The basis case u =0 demodulates to a ≠ s(0), which we are given. The induction step is a + s(u) ≠ s(0). Using the definition of addition this becomes s(a+u) ≠ s(0). Since successor is one-to-one, that becomes a+u ≠ 0. That can be proved as in le2.in, since we are also given a ≠ 0.

The Otter-lambda proof given below closely follows the beginning of this outline. At line [18] it begins the inductive proof; for readability the Skolem term g(lambda(x,a+x=s(0))) and its alphabetic variants have been replaced by a constant c for readability, but the occurence of this term indicates that the induction hypothesis is as sketched above. At line [32] then, Otter-lambda has arrived at a+c = 0, which corresponds to a+u = 0 in the above proof. Note that the definition of addition [13] was used already to derive [19]. So at line [32], it only remains to derive a contradiction from a+c = 0 and a ≠ 0. But now, unlike in le2.in, c is a Skolem term for induction, and not a Hilbert epsilon-symbol term. So it is NOT the first choice of a masking term when Otter-lambda attempts to unify [32] with the third literal in [7]. This file was created an run before the option existed to allow multiple unifiers; since the input file doesn't contain assign(max_unifiers,2), the default is 1 and no other masking term is tried. Hence the proof does NOT complete as in le2.in, the way the proof sketch above suggests it might. Instead it has a lot of strange steps, which I have verified step by step, but of which I have no intuitive understanding. Finally at the last step, it does complete as in le2.in, with an application of one but not both of the induction axioms and a use of the definition of addition.

I did run this file again with assign(max_unifiers,2) and again with assign(max_unifiers,8), but it finds this same proof. Without the line in the input file commented about nested g-terms, it does produce a similar proof, but involving nested Skolem terms and paramodulation into those terms, which is even uglier than this proof.

1 [] a!=0.
2 [] a!=s(0).
3 [] x=x.
4 [] s(x)!=0.
5 [] s(x)!=s(y)|x=y.
6 [] ap(y,0)| -ap(y,g(y))| -ap(y,z).
7 [] ap(y,0)|ap(y,s(g(y)))| -ap(y,z).
8 [] x+0=x.
9 [] -ap(Z,w)|exists(lambda(x,ap(Z,x))).
10 [] -exists(lambda(x,ap(Z,x)))|ap(Z,e(Z)).
12 [] x+0=x.
13 [] x+s(y)=s(x+y).
14 [] (u<=v)=exists(lambda(x,u+x=v)).
15 [] a<=s(0).
18 [binary,15.1,7.3,demod,14,beta,14,14,beta,factor_simp] exists(lambda(x,a+x=s(0))).
19 [binary,18.1,10.1,demod,beta] a+e(lambda(x,a+x=s(0)))=s(0).
21 [binary,19.1,7.3,demod,beta,12,beta,13,unit_del,2] s(a+g(lambda(x,a+x=s(0))))=s(0).
22 [binary,19.1,6.3,demod,beta,12,beta,unit_del,2] a+g(lambda(x,a+x=s(0)))!=s(0).
32 [binary,21.1,5.1] a+g(lambda(x,a+x=s(0)))=0.
34 [para_from,21.1.1,5.1.2] s(x)!=s(0)|x=a+g(lambda(y,a+y=s(0))).
44 [binary,32.1,9.1,demod,beta] exists(lambda(x,a+g(lambda(y,a+y=s(0)))=0)).
45 [para_from,32.1.1,22.1.1] 0!=s(0).
46 [para_from,32.1.2,8.1.1.2] x+a+g(lambda(y,a+y=s(0)))=x.
49 [para_from,32.1.2,1.1.2] a!=a+g(lambda(x,a+x=s(0))).
90 [para_into,44.1.1.2.1,32.1.1] exists(lambda(x,0=0)).
92 [para_into,90.1.1.2.2,32.1.2] exists(lambda(x,0=a+g(lambda(y,a+y=s(0))))).
130 [binary,92.1,10.1,demod,beta] 0=a+g(lambda(x,a+x=s(0))).
176 [para_from,34.2.2,130.1.2] 0=x|s(x)!=s(0).
182 [para_from,34.2.2,49.1.2] a!=x|s(x)!=s(0).
195 [binary,176.2,7.2,demod,beta,beta,unit_del,45] 0=g(lambda(x,x=s(0)))|y!=s(0).
248 [binary,195.2,46.1] 0=g(lambda(x,x=s(0))).
252 [para_into,248.1.1,130.1.1] a+g(lambda(x,a+x=s(0)))=g(lambda(y,y=s(0))).
267 [para_from,248.1.1,4.1.2] s(x)!=g(lambda(y,y=s(0))).
358 [binary,182.1,7.1,demod,beta,beta,unit_del,3] a=s(g(lambda(x,a=x)))|a!=y.
370 [binary,358.2,3.1] a=s(g(lambda(x,a=x))).
375 [para_from,370.1.1,252.1.1.1] s(g(lambda(x,a=x)))+g(lambda(y,a+y=s(0)))=g(lambda(z,z=s(0))).
441 [binary,375.1,7.3,demod,beta,12,beta,13,unit_del,267,267] $F.