Phase transitions for the miniaturized monotone Bolzano Weierstrass theorem (ref 898 Ultra convergence 1)

[Andreas Weiermann]

Dear colleagues,


in FOM 898 Ultra convergence Harvey Friedman discussed his findings on 
the miniaturization of the Bolzano Weierstrass theorem.


In my opinion these are really interesting results relating the 
Ackermann function

to a theorem from mathematical practice.

Here I would like to share some findings on the phase transition for the 
monotone version.


For a number-theoretic function f non decreasing unbounded let

MBW_f be the assertion


For all positive integers K>=3 there exists a positive integer M

so big that for all monotone sequences of real numbers

x_1,...,x_M in the unit interval

there exist k_1<...<k_K such that for all l <= K-2 we have

that the distance between

x_{k_{l+2}} and x_{k_{l+1}} is smaller than 1/f(k_l).

Harvey showed that for usual functions f the dependence of M (when 
chosen to be minimal) on K

is bounded by an Ackermannian function.


Let log_d be the d-th iterate of the log function and log* be the 
functional inverse

of the tower function. So log*(e_n)=n where e_1=e and e_{n+1}=e^{e_n}.


Let f*(a):=a log_1(a) log_2(a) ... log_{log^*(a)}(a).

Then ISigma_1 proves MBW_f*.

The proof is elementary and uses the divergence of the sum of the 1/f*(a).

(I presented this result in the Helsinki seminar in November 2021.)


Let epsilon>0.

Now fix a positive integer d.

Let f_d(a):=a log_1(a) log_2(a) ... log_{d}^{1+epsilon}(a).

Then, as long as I did not make a mistake in my proof, ISigma_1 does not 
proves MBW_f*.

Some stronger results will hold when d or epsilon may depend on a

but this leads to a more messy formulation.


These results hold for the monotone version where the sequence

x_1,...,x_M is assumed to be monotone. For the non monotone version BW_f

where the monotonicity assumption is simply dropped the situation

for a good threshold seems to be more difficult.


Harvey Friedman has shown that the corresponing principle BW_f is 
provable in EFA

for f(a)=a/log(a). Bounds for ISigma_1 unprovability of BW_f follow from 
the thresholds

for MBW_f above but there is still some room for improvement.


All the best,

Andreas