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))).
(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(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).
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.