FOM: Induction illogical?

[Michael R. Fara]

On Thu, 25 Feb 1999, Harvey Friedman wrote:


>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?

Boolos has a discussion of something similar in his "A Curious Inference",
JPL 16 (1987), reprinted in his posthumous *Logic, Logic and Logic*, HUP 1998.