FOM: inductive proofs of validity

[Harvey Friedman]

I whipped off two postings that are really on this topic: 6:02PM 2/25/99
"Induction illogical?", and  8:37PM 2/25/99 "Induction illogical?(corrected
version).

Robert Black has kindly responded to my inquiry about the work of Boolos in
this vein.

I will get a chance to look at Boolos in a few days, and I thank Black for
the references.

In the meantime, I realized that my examples were overly complicated and
also unnecessarily delicate. There are much better ways to do this. Here is
one.

The problem is to give simple examples of predicate calculus validities, or
logical implications, that can be (humanly) seen to be validities, or
logical implications, using "extralogical" principles; but where all purely
logical proofs (i.e., in predicate calculus) are absurdly large.

We also take some care to make the examples purely existential; i.e., we
are looking at purely existential validities (function symbols allowed).

We define the theory T_k, which uses <=,=,0, and the unary function symbols
S,F_1,...,F_k. The axioms are as follows (in free variable form):

i) S(0) notequal 0;
ii) x <= 0 if and only if x = 0;
iii) x <= S(y) if and only if x <= y or x = S(y);
iv) For each 1 <= i <= k, F_i(x) <= S(x).

Let *(k) be

(therexists distinct x,y)(x <= y & F_1(x) <= F_1(y) & ... & F_k(x) <= F_k(y)).

THEOREM 1. For each k >= 1, T_k logically implies *(k). Any proof in
predicate calculus of the validity

T_5 arrows *(5)

must use more than an exponential stack of 2's of height 1000 number of
symbols (cuts allowed). The growth rate of the number of symbols needed to
prove

T_k arrows *(k)

in predicate calculus grows as the Ackerman function in k.

This perhaps can be done with k = 4.

I now believe that my new "perfect" tree statement - see by FOM posting
2:46AM 2/5/99, "Perfect" statements - can be used to good effect in this
context to provide simple predicate calculus validities that can only be
proved to be validities using impredicative methods. The size of the
predicate calculus proof is bounded below by what I call an "uncountable"
integer.

Now I have to go look at what Boolos did.