Online Otter-λ

-->

Examples

Examples -> PeanoArithmetic -> le2.html

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

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.