FOM: Induction illogical?(corrected version)

[Harvey Friedman]

There were some careless errors in the first version. This should be better.

Simpson 5:01PM 2/25/99, ends with:

>What does this do to the Poincare-Detlefsen claim [which I reject]
>that mathematical induction gives insight that is inaccessible to
>logic?

I haven't followed this particular thread too carefully, but this does
suggest an important line of research.

First of all, it is obvious that mathematical induction is "illogical" in
some very restricted sense of the word:

1. Induction cannot be derived in (first order) predicate calculus (with
equality). This is clear, since it cannot even be stated in predicate
calculus.

2. Induction cannot be derived in predicate calculus even if we have a
predicate symbol for being a natural number, and the usual quantifier free
axioms for 0,+,x. I.e., there are formulas for which induction cannot be
derived.

But now I want to ask this:

3. Is there a sentence of predicate calculus that can be proved to be valid
with the help of mathematical induction, but which cannot be proved in
predicate calculus?

4. The answer is obviously no, since such a sentence would in fact be
valid, and hence by the completeness theorem, provable in predicate
calculus.

Now we ask:

5. Is there a sentence of predicate calculus that can be proved to be valid
**via a short proof** with the help of mathematical induction, but which
cannot be proved in predicate calculus **via a short proof**?

The answer to this is well known, and the answer is yes. But now we ask:

6. Is there a simple, natural example of 5?

*****

Let T_0 consist of the following axioms:

a) < is a linear ordering;
b) 0 is the least element;
c) S(x) is the immediate successor of x.

Now for each k >= 1, we let T_k consist of T_0 together with the following
axioms using a k-ary predicate symbol P:

d) P(S(0),...,S(0));
e) if P(x_1,...,x_k) then there exists y_1,...,y_k such that P(y_1,...,y_k)
and for all 1 <= i <= k, x_i = y_i or S(x_i) = y_i or x_i = S(y_i), and
max(x_1,...,x_k) < max(y_1,...,y_k).

THEOREM. T_k logically implies that there exists distinct k-tuples
x_1,...,x_k, and y_1,...,y_k, such that P(x_1,...,x_k), P(y_1,...,y_k), and
each x_i <= y_i. This is proved by induction. The proofs of these
infinitely many logical implications using induction is linear in k, with
very small constant (low overhead). However, the least length of a proof in
predicate calculus, as a function of k, grows like Ackerman's function. In
fact, already for k = 4, this is considerably more than, say, a stack of
1000 2's.

NOTE: We are talking about lengths of proofs with cuts allowed. I recall
that Boolos had some interesting lower bounds, but maybe only for cut free
proofs?? Does anybody recall where Boolos' stuff appeared?