Online Otter-λ

Examples

Theorem: The identity function exists; that is, for some f, f(x) =x for all x.

This example mainly is just a test that lambda unification is working correctly. We put in X(a) != a, and the logical axiom x=x, and when these two clauses are resolved, lambda unification is called to unify X(a) and a. It is supposed to find X = lambda(x,x), and it does.

It's worth remarking that the use of x=x indicates that we are using "total" lambda calculus, in which Ap(f,x) is always defined, rather than "partial" lambda calculus, in which Ap(f,x) need not always be defined. To make this proof work with partial lambda logic, we would replace x = x with

-E(x) | x =x.

We would then have to explicitly add E(a) as an axiom.