Online Otter-λ

Examples

Definition of < and ≤ in PA in terms of exist and proofs of their transitivity

In lambda logic, one has the existential quantifier of first-order logic, but one also can introduce a constant "exists" that defines the existential quantifier as a function taking a propositional function as an argument and returning a proposition. This can be done in an otter-lambda input file using the following two axioms, called the "first law of existence" and the "second law of existence":

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

In these axioms, the constant e plays the role of Hilbert's epsilon operator.

Hilbert's notation: εx.Zx

Our notation: e(lambda(x,Ap(Z,x)))

or just e(Z).

This represents "some x such that Ap(Z,x) if there is one". What it denotes (or whether it is even defined, in partial lambda logic) when there doesn't exist an x such that Ap(Z,x), is not relevant.

In the above formulation, we made e a function symbol. We could have made it a constant and used Ap(e,Z) instead of e(Z).

Since resolution theorem provers do not work directly with quantifiers, it is customary to first "Skolemize" first order formulas (after negating the theorem to be proved). But with the aid of lambda unification, we can use a first-order prover to work directly with quantifiers, represented in this way as constants. That is the point of this example.

We define u <= v to mean that for some x, u+x = v. (That is correct in the context of Peano Arithmetic, where variables are supposed to range over natural numbers 0,1,2,...) Then to prove the transitivity of <=, suppose a < b and b < c. Then b = a + u for some u and c = b + v for some v, so c = (a + u) + v and, using associativity, c = a + (u+v), so a <= c. The point of the example is both "laws of existence" are correctly used to carry out this proof.

Here is the proof that Otter-lambda finds.

5 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).
6 [] -exists(lambda(x,Ap(Z,x)))|Ap(Z,e(Z)).
7 [] (x+y)+z=x+y+z.
8 [] (u<=v)=exists(lambda(x,u+x=v)).
9 [] a<=b.
10 [] b<=c.
11 [] -(a<=c).
13 [9,demod,8] exists(lambda(x,a+x=b)).
15 [10,demod,8] exists(lambda(x,b+x=c)).
17 [11,demod,8] -exists(lambda(x,a+x=c)).
18 [binary,13.1,6.1,demod,beta] a+e(lambda(x,a+x=b))=b.
19 [binary,15.1,6.1,demod,beta] b+e(lambda(x,b+x=c))=c.
20 [binary,17.1,5.2,demod,beta] a+x!=c.
38 [para_into,19.1.1.1,18.1.2,demod,7] a+e(lambda(x,a+x=b))+e(lambda(y,b+y=c))=c.
39 [binary,38.1,20.1] $F.

Line [18] corresponds to "b = a + u for some u"; the u in question is e(lambda(x,a+x=b)). Similarly, line [19] corresponds to "c = b + v" for some v. Since resolution provers work by contradiction, the negated goal becomes a + x != c, by the first law of existence, and then associativity is used to find a contradiction, taking x to be u + v. The proof follows the sketch above, except for the adjustment required to make it a proof by contradiction.

Induction was not used in this example, but we include it in the Peano Arithmetic example set anyway, since arguments like this are essential in the development of formal number theory. The normal way of treating this example in a resolution theorem prover would require introducing a Skolem function f with the axiom x <= y if and only if x + f(x,y) = y. One could also first define cutoff subtraction and use that in place of f.