FOM: Induction illogical?

[Harvey Friedman]

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

THEOREM. T_k logically implies that there exists x_1,...,x_k, 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 proof 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?