Online Otter-λ

Examples

Theorem. There are no nilpotents in an integral domain.

An integral domain is a ring with no zero divisors. A nilpotent element is a non-zero element b of the ring such that the n-th power of b, here written pow(n,b), is zero. Proving this is an elementary exercise in mathematical induction; it does occurs as an exercise in Jacobson's textbook on algebra. It is an interesting example because it mixes abstract algebra and induction. Even to formulate it, we need variables for ring elements and variables for natural numbers.

You might think that we should use unary predicates N(x) and R(x) for the natural numbers and the ring. That is not necessary, because of a technique called "implicit typing", explained in detail elsewhere on this website and in Beeson's papers. Roughly speaking, as applied here, it means that
+ and * are operations on the ring, i.e. type(R,+(R,R)) and type(R, *(R,R)), and pow is an operation that takes a number and a ring element
and produces a ring element: type(R, pow(N,R)). These are "implicit" typings because these type expressions are not part of Otter-lambda's input.
The typing of ap is type(Boolean, ap(Pred,N)), where Pred is the type of predicates on natural numbers, i.e. Boolean-valued functions on N.
The typing of the Skolem function g is type(N,g(N,Pred)). The constant 0 is used for the zero element of the ring, and a different symbol o
is used for the natural number o. You will see that the axioms in the input file are correctly typed, i.e. all the axioms use the symbols in accordance with these typings. In fact the proof is also correctly typed, and hence it could be converted to a proof in which unary predicates N(x) and R(x) were used. However, it is much easier to find the proof without the predicates N(x) and R(x); you will note that the input file specifies hyperresolution as a rule of inference, and with unary predicates that will no longer be applicable.

Otter can find this proof if you specifically tell it the instance of induction to use (see nilpotent3) ; but in this example, Otter-lambda is given only the completely general formulation of the induction axiom, and finds the correct instance of induction by lambda-unification.

The integral domain axioms that are used in the proof are the first two lines:

27 [] 1!=0.
28 [] x*y!=0|x=0|y=0.

The axioms use s(x) for the successor of x, and
the n-th power of x, pow(n,x), is recursively
defined:

30,29 [] pow(s(x),y)=y*pow(x,y).
32,31 [] pow(o,x)=1.

Note that the zero element of the ring is written 0, while the natural number zero is written o. That is done to ensure that the axioms are "implicitly typed". When Otter-lambda (or Otter itself) puts two equation numbers on a line, it's because it has added a copy of the equation as a new demodulator, which will be used to rewrite future conclusions before saving them.

The next two axioms are the clausal form of mathematical induction, in the appropriate for proving a negated proposition by induction. Here the propositional function x represents the negation of the proposition to be proved by induction. This way the negated goal, which will not be a negation, can be resolved with the third literal -ap(x,y).

35 [] ap(x,o)| -ap(x,g(y,x))| -ap(x,y).
36 [] ap(x,o)|ap(x,s(g(y,x)))| -ap(x,y).

Finally we have the negation of the goal:
37 [] b!=0.
39 [] pow(n,b)=0.

Otter-lambda polishes this proof off in two steps, which we will explain below:

41 [binary,39.1,36.3,demod,beta,32,beta,30,unit_del,27] b*pow(g(n,lambda(x,pow(x,b)=0)),b)=0.
43 [binary,39.1,35.3,demod,beta,32,beta,unit_del,27] pow(g(n,lambda(x,pow(x,b)=0)),b)!=0.
136 [binary,41.1,28.1,unit_del,37,43] $F.

Let's see how this works. To get 41, Otter-lambda resolves 39, which is pow(n,b) = 0, with the last literal in 36, namely -ap(x,y). That means that it will try to unify pow(n,b) = 0 with ap(x,y). Lambda unification has to pick either n or b to replace by a new lambda variable z. Since the input file contains the command set(induction), it prefers the integer variable n. Here it knows that n is an integer variable because it begins with "n"; but we could also have used the command list(types) to specify the type of pow. Lambda unification then succeeds, finding

x := lambda(z,pow(z,b)=0), y := n.

This is a correct result in the sense that the lambda term for x is the propositional function whose value is the negation of what we are trying to prove by induction, namely that pow(z,b) is not zero for all integers z.

The result of the resolution step should then be the clause formed of the first two literals of 35 under this substitution. The first literal is

ap(lambda(z,pow(z,b)=0),o)

which beta reduces to pow(o,b) = 0. But the demodulator 31 now applies, and pow(o,b) reduces to 0, so the literal reduces to 0=0. Unit deletion then discards this literal. You can see in the justification of step 41 that unit_del is mentioned.

The second literal is ap(x,s(g(y,x))). The Skolem term g(y,x) becomes g(n,lambda(z,pow(z,b)=0). It helps to think of this, and write it, as a constant c. The second literal is then ap(lambda( z,pow(z,b)=0),s(c)), which beta reduces to pow(s(c),b) = 0. That demodulates using 30 to b*pow(c,b) = 0, which is what you see listed as clause 41. This is intuitively the negated goal of the "induction step" to be proved.

The "induction hypothesis" arises similary when 39 is resolved with 35 instead of 36. Again the first literal simplifies and is deleted, and the second literal now becomes -ap(lambda(z,pow(z,b)=0),c), which beta reduces to pow(c,b) != 0.

To finish the proof we have to get a contradiction from pow(c,b) !=0 (the induction hypothesis) and b*pow(c,b) = 0 (the negated conclusion of the induction step). But by the integral domain axiom 28, these two imply b = 0, while 37 tells us b != 0. That completes the proof.