Online Otter-λ

Examples

Examples -> LambdaLogic -> divides.html

Although it is normal in resolution-based theorem provers to remove quantifiers by Skolemization before submitting a problem to the prover, this makes it difficult to deal with definitions that involve quantifiers, such as continuity of a function, or the divides relation on integers. In this example, we show how this problem can be solved in Otter-$\lambda$. We show how to treat quantification at the clause level, based on the machinery of $\lambda$-calculus and lambda unification. One can regard "there exists" as a boolean-valued functional, whose arguments are boolean functions (defined, for simplicity, on the integers, let's say). Then "there exists n such that P[n]$ is an abbreviation for the result of applying the functional "exists" to the propositional function lambda(n,P[n]). Introducing a constant symbol exists this takes the explicit form

Ap(\exists, lambda(n,Ap(P,n))).

This definition of quantification allows one to work with quantified statements directly in Otter-λ. One of the rules for exists can be expressed in an Otter-λ file (it is not hard-coded):

-Ap(Z,w) | exists(lambda(x, Ap(Z,x))

This works in Otter-λ as follows: if Z(t) can be proved for any term t, then the literal -Ap(Z,w) will be resolved away, using the substitution w:= t. Then exists(lambda(x,Ap(Z,x))) is deduced, which is the formal expression of "there exists an x such that Z(x)". No machinery is added to Otter-λ to accomplish this, other than what was already added for λ-calculus. This permits the use of definitions that explicitly involve a quantified formula in the definition. That is the point illustrated in this example. We define

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

Now, given the clause 2 * 3 = 6, Otter-λ can deduce divides(2,6) as follows: First, the negated goal -divides(2,6) will rewrite to

-exists(lambda(x,2*x = 6))

This will unify with exists(lambda(x,Ap(Z,x)) if 2*x=6 will unify with Ap(Z,x). lambda unification will be called with x forbidden to Z, since the unification happens within the scope of the bound variable x. We get

Z := lambda(w,2*w = 6).

Resolution of the two clauses containing exists will then generate a new clause containing the single literal $-Ap(Z,w)$ with this value of $Z$. Specifically,

-Ap(lambda(w,2*w = 6),w).

That will be beta-reduced to 2*w != 6$ so the clause finally generated will be 2*w != 6. That resolves with 2*3 = 6, producing a contradiction that completes the proof. We emphasize that this example is not meant to demonstrate prowess in number theory; we told the program that 2*3=6 and concluded that 2 divides 6, which is trivial as number theory. Our point is rather to demonstrate how the program expanded a definition that involved a quantifier, and then used the second-order definition of quantifiers and lambda unification to automatically complete the proof. On the other hand, even though unmodified Otter incorporates a utility for Skolemizing first-order formulas, so that in some sense one can input quantifiers, it cannot do what is demonstrated here: use quantified formulas within the clause language while a resolution proof is being constructed.

This example demonstrates the "first law of existence";. For a demonstration of the "second law of existence", see the file divides2.html.