FOM: feasibility

[Harvey Friedman]

I have no quarrel with Sazonov that investigating the notion or notions of
feasibility sounds interesting and promising. The only issue might be: what
kind of results would make this into a serious ongoing subject, with deep
and surprising results? I'm not sure we are there yet.

I would like to come back to the kind of thing you said Parikh did. Let
PA(F) be Peano arithemtic formulated without the unary predicate F for
feasible, together with the single axioms:

F(0).
(forall x)(F(x) implies F(x+1)).

We also allow abbreviations; i.e., we can introduce new predicates by
explicit definition. This shortens formulas, and hence proofs.

Let 2^[n] be an exponential stack of n 2's. Obviously, we can prove in
PA(F) that F(2^[n]). A question is: how many symbols in such a proof? The
answer is: linear in n with a small constant. Also, it appears that you
need only a tiny fragment of PA for this. Just standard quantifier free
information about 0,S,+,x,exp. Conversely, how many symbols are required
for such a proof? Again, the answer seems to be: linear in n with a small
constant.

How explicit are the known estimates?