Online Otter-λ

Examples

Proof that x ≤ 0 implies x = 0 in PA, using the definition of ≤ in terms of existence.

One should read the commentary on le.in before reading this one.

This is another illustration of the use of "exists" in lambda logic. Proceeding by contradiction as resolution provers do, we assume a ≤ 0 but a ≠ 0. Then by the definition of ≤, there is some u such that a + u = 0. That u is e(lambda(x,a+x = 0)), and this point is reached in line [17] of the Otter-lambda proof below. Now in Peano Arithmetic, of course, variables range over natural numbers, so a + u = 0 is only possible if a and u are both 0. That fact, however, is not directly given in the axioms. The last step in the Otter-lambda proof below is a bit complicated. It uses one of the two induction axioms, but not both! Writing line [17] as a + c = 0 for a moment, using a constant c for the term e(lambda(x,a+x=0)) for readability, lambda unification is used to unify a + c = 0 with ap(y,z) from the third literal of line [6]. The masking term will be c, and y will get the value lambda(z,a + z = 0). The result of the resolution inference comes from the first two literals of [6], namely ap(y,0) | ap(y,s(g(y))); with y having the stated value, a beta-reduction is possible, and the result of the resolution inference will be a+0 = 0 | a + s(g(y)) = 0. The literal a+0 demodulates to a = 0, which contradicts [1] and is removed by unit deletion. That leaves a + s(g(y)) = 0, which demodulates to s(a + g(y)) = 0, and then contradicts [3]. Hence it too is removed by unit deletion, completing the proof without ever needing the induction hypothesis!

1 [] a!=0.
3 [] s(x)!=0.
6 [] ap(y,0)|ap(y,s(g(y)))| -ap(y,z).
9 [] -exists(lambda(x,ap(Z,x)))|ap(Z,e(Z)).
11 [] x+0=x.
12 [] x+s(y)=s(x+y).
13 [] (u<=v)=exists(lambda(x,u+x=v)).
14 [] a<=0.
16 [14,demod,13] exists(lambda(x,a+x=0)).
17 [binary,16.1,9.1,demod,beta] a+e(lambda(x,a+x=0))=0.
18 [binary,17.1,6.3,demod,beta,11,beta,12,unit_del,1,3] $F.