Online Otter-λ

Examples

This example demonstrates the "second law of existence". If you haven't already done so, you should first study the commentary on the first law of existence in divides.html, as that commentary explains the use of lambda logic to express quantification.

The "second law of existence" is the law that says, if we have proved "there exists an x such that Z[x]", then

-exists(lambda(x,Ap(Z,x))) | Ap(Z, e(Z)). % e is Hilbert's epsilon ex.Zx = e(lambda(x,Ap(Z,x))) = e(Z).

The example uses this law to prove the transitivity of the divisibility relation divides(n,m) on the natural numbers. This relation is defined by

divides(u,v) = exists(lambda(x,u*x = v)).

which is used as a demodulator. To prove the transitivity of divides, we assume

divides(a,b).
divides(b,c).
-divides(a,c).

and try to deduce a contradiction. The definition of divides applies to yield

exists(lambda(x,a*x=b)).
exists(lambda(x,b*x=c)).
-exists(lambda(x,a*x=c)).

What we would informally say is "fix some u such that a*u = b, fix some v such that b*v = c, and take x to be u*v; then a*x = c, contradiction". Of course the file provides as an axiom the associativity of multiplication so we can compute c = b*v = (a*u)*v = a*(u*v) = a*x.

Our point in this commentary is to show how the second law of existence is used to provide the formal counterpart to this informal argument. Namely, resolving the second law of existence with exists(lambda(x,a*x = b)) we call lambda unification to unify Ap(Z,x) with a*x = b. That produces Z:=lambda(x,a*x = b). Then e(Z) = e(lambda(x,a*x = b)) plays the role of u, i.e. it is "some x such that a*x =b". The result of the resolution is Ap(Z,e(Z)), which with the given value of Z reduces to a*e(Z) = b, or to be completely explicit,

a*e(lambda(x,a*x=b))=b

Informally, a times "some x such that a*x = b" is equal to b. Similarly, we have

b*e(lambda(x,b*x=c) = c,

and Otter-λ easily finishes the first-order part of the proof.