[FOM] sharply bounded versions of FFF

[Andreas Weiermann]

Dear FOM'ers,

some time ago there was a discussion on FOM concerning
the naturality of Friedman's independence results.

In favour of naturality might be (as I believe)
the following observations.
We consider sharply bounded versions of FFF
Thus instead of requiring in a Friedman
style growth rate condition that the i-th element
(from a given species) is bounded by K+i 
where K is an input parameter we consider
the condition that the i-th element
(from a given species) is bounded by log_2(K)+\log_2(i).
This leads to some independence results for weak fragments
of arithmetic.
Let SWP(Nat,r) be the statement that for
every K there exists M so large that for every
finite sequence \sigma_0,\ldots,\sigma_M of finite
sequences of natural numbers with 
N(\sigma_i)\leq \log_2(K)+r\cdot \log_2(i)
for i=0,\ldots, M
there exists indices i<j\leq M such that
\sigma_i is a subsequence of \sigma_j.
(This is a sharply bounded variant of Higman's Lemma.)
Here for \sigma=<s_1,\ldots,s_n> we define
N\sigma=1+s_1+\ldots+1+s_n.

Then for all small \epsilon>0
1. I\Delta_0 "proves" SWP(Nat,1-\epsilon).
To be precise I only checked that the length of bad sequences
is polynomially bounded.
2. I\Delta_0 does not prove SWP(Nat,1)
3. I\Delta_0+exp proves SWP(Nat,1)
4. I\Delta_0+exp does not prove SWP(Nat,1+\epsilon)
In fact I\Sigma_2 does not prove SWP(Nat,1+\epsilon)
but of course I\Sigma_3 does prove SWP(Nat,1+\epsilon)

Let SWP(k,r) be the corresponding statement 
for sequences of k-bounded sequences (i.e. all
entries are below k). Then
1. For every k I\Delta_0 "proves" SWP(k,1)
To be precise I only checked that the length of bad sequences
is polynomially bounded.
2. I\Delta_0 does not prove \forall k SWP(k,1)

So 1 appears to be as a very interesting phase transition
threshold where one jumps from I\Delta_0 to 
I\Delta_0+exp and then to I\Sigma_3

Similar phase transition
results will presumably be true for finite
sequences of finite trees. (This is part of a joint
research project with L. Gordeev.)
Sharply bounded versions can
also be formulated for Ramsey's theorem and the
Paris Harrington theorem but it is not yet clear
whether this leads to something of interest.

Best regards,
Andreas Weiermann