Online Otter-λ

The clausal form of mathematical induction in first-order logic

We will find the clausal form of mathematical induction. Induction is stated using the successor function s(x) = x+1. But in the Peano axioms for the integers, s(x) is considered fundamental, and addition is defined in terms of successor rather than successor in terms of addition. The following is the usual form of mathematical induction.

P(0) and forall(x, P(x) implies P(s(x))) implies forall(z,P(z))

Here P is any predicate; for the purpose of bringing induction to clausal form, we assume that P is atomic, but it may have other variables that are not shown. To bring this to clausal form, we first bring the two quantifiers to the front. The order in which those quantifiers come to the front is a matter of choice. We could obtain either of the two following forms:

exists(x,forall(z, (P(0) and P(x) implies P(s(x))) implies P(z))).
forall(z,exists(x, (P(0) and P(x) implies P(s(x))) implies P(z))).

We choose the first form, and replace x by a Skolem term. If P has no variables except x, that term can just be a constant g. If P contains additional variables y, then x should be replaced by g(y). We will just write g for this term. The result is

(P(0) and (P(g) implies P(s(g)))) implies P(z).

Replacing "A implies B" by -A | B (which is clause-language notation for "not A or B"), we get

-P(0) | (P(g) and -P(s(g))) | P(z).

To bring this to clausal form, we distribute the "and", producing two clauses:

-P(0) | P(g) | P(z).
-P(0) | -P(s(g)) | P(z).

This is the clausal form of induction. Let's see if we can recognize it. Suppose we want to prove for all(z,P(z)). Then, in a clausal theorem prover like Otter or Otter-λ, we start with the negated goal -P(b), where b is a constant. Then we resolve this with the last literal in each of the two induction clauses. The result is

-P(0) | P(g).
-P(0) | -P(s(g)).

If we can prove the basis case P(0), then the first literals will resolve away, leaving

P(g).
-P(s(g)).

We recognize this as the familiar "induction step": We assume P(g) holds and try to prove P(s(g)) holds, by starting with P(g) and -P(s(g)) and trying to derive a contradiction.

If we take the other clausal form of induction, it comes out just the same, except that we have g(z) instead of just g, or g(z,y) instead of g(y), if P has additional variables y. Some of the example files have this additional variable in the Skolem term.

The clausal form of mathematical induction in lambda logic

Lambda logic is first-order logic augmented by Ap and lambda. It is the natural logic in which Otter-λ finds proofs. In lambda logic, we can use a variable to stand for a predicate of the natural numbers. In the induction axiom, we can then replace P(x) by Ap(y,x), which means "predicate y holds at argument x". We switch from letter P to y, since y is now considered a variable in the induction axiom. In the first-order formulation, induction was an axiom schema, meaning that a different axiom is needed for each particular P. In lambda logic, as in higher-order typed logics, we can formulate the induction schema with a single axiom, using a variable for the predicate. When we bring it to clausal form, the result is the same as above, except that the "constant" g now is a Skolem term g(y):

-Ap(z,0) | Ap(y,g(y))) | Ap(y,z).
-Ap(z,0) | -Ap(y,s(g(y))) | Ap(y,z).

This is the clausal formulation of induction in lambda logic. Again, it can also be formulated with g(y,z) instead of g(y), which is what we would obtain bringing the quantifiers out in the other order, but it is simpler this way.