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.