911: Ultra Convergence/3

[Harvey Friedman]

First we correct
https://cs.nyu.edu/pipermail/fom/2021-October/022900.html  #900  I
wrote

THEOREM 1. For every bounded infinite sequence of reals, x[1],x[2],..,
there are primes p1 < ... < pk+1 such that |x[p2p3...pk] -
x[p3p4...pk+1]| < 2^-p1.

THEOREM 2. In Theorem 1, the p's can be chosen below a fixed integer
depending only on the sup of the x's and k.

THEOREM 3. For a sequence x[1],...,x[n] of reals, n sufficiently large
relative to its diameter and k, there are primes p1 < ... < pk+1 such
that |x[p2p3...pk] - x[p3p4...pk+1]| < 2^-p1.

This should be (somewhat simplified)

THEOREM 1a. For every x[1],x[2],.. in [0,1],
there are primes p1 < ... < pk+2 such that
|x[p2p3...pk] - x[p3p4...pk+1]| < 2^-p1 and
|x[p3p4...pk+1] - x[p4p5...pk+2]| < 2^-p2.

THEOREM 1b. In Theorem 1, the p's can be chosen below a fixed integer
depending only on k.

THEOREM 1c. For every x[1],...,x[n] in [0,1], n sufficiently large
relative to k, there are primes p1 < ... < pk+2 such that
|x[p2p3...pk] - x[p3p4...pk+1]| < 2^-p1 and
|x[p3p4...pk+1] - x[p4p5...pk+2]| < 2^-p2.

with the same metamathematical PA properties.

Note the three equivalent forms in each case. From now on we will only
give the first form.

All this is related to

[1] Harvey Friedman and Florian Pelupessy
Proc. Amer. Math. Soc. 144 (2016), 853-860
https://www.ams.org/journals/proc/2016-144-02/S0002-9939-2015-12759-1/home.html

Here is a form inspired by #900 and [1]:

THEOREM 2. For every infinite sequence of positive integers with each x[i] <= i,
there are primes p1 < ... < pk+2 such that
x[p1p2...pk] <= x[p2p3...pk+1| <= x[p3p4...pk+2]|.

with the same metamathematical PA properties.

We now give general templates for such statements.

TEMPLATE A. For every x[1],x[2],... in [0,1],
there are elements  p1 < ... < pk+2 in E such that
|x[f(p1,...,pk)] - x[f(p2,...,pk+1)]| < g(p1) and
|x[f(p2,...,pk+1)] - x[f(p3,...,pk+2)] < g(p2).

TEMPLATE B. For every infinite sequence of positive integers with each
x[i] <= F(i),
there are elements  p1 < ... < pk+2 in E such that
x[G(p1,...,pk)] <= x[G(p2,...,pk+1)] <= x[G(p2,...,pk+1)].

In the above, E is an infinite set of positive integers, f maps Z+k
into R, g maps Z+ into R+, F maps Z+ into Z+, G maps Z+k into Z+. Here
k,E,f,g,F,G are fixed in advance.

STRONGER TEMPLATES. The infinite sequence is given, and then we
quantify over all k,E,f,g,F,G. Independently of this, we can length
the Template A conclusion from two inequalities to r inequalities, and
we can lengthen the Template B conclusion from the length 3 inequality
to length r.

THEOREM 3. For each fixed k, ACA0 proves Templates A,B for all such
E,f,g,F,G. For the stronger Templates, ACA' suffices (for all k,x, the
k-th Turing jump of x exists). This holds even for the Stronger
Templates.

PROJECT. Get information about the logical strengths and provable
equivalences as the parameters k,E,f,g,F,G,r vary.

Very special cases and classes of cases seem very interesting. For
example, look at

PROPOSITION 4. For every ix[1],x[2],.. in [0,1], there are p1 < ... <
pk+2 such that there are p1 < ... < pk+2 where
|x[p2p3...pk] - x[p3p4...pk+1]| < 2^-p1 and
|x[p3p4...pk+1] - x[p4p5...pk+2]| < 2^-p2.

PROPOSITION 5. For every x[1],x[2],.. in [0,1], there are p1 < ... <
pk+2 such that there are p1 < ... < pk+2 where
|x[p2+p3+...+pk] - x[p3+p4+...+pk+1]| < 2^-p1 and
|x[p3+p4+...+pk+1] - x[p4+p5...+pk+2]| < 2^-p2.

PROPOSITION 6. For every infinite sequence of positive integers with
each x[i] <= i, there are positive integers p1 < ... < pk+2 such that
x[p1...pk)] <= x[p2...pk+1] <= x[p3...pk+2].

PROPOSITION 7. For every infinite sequence of positive integers with
each x[i] <= i, there are positive integers p1 < ... < pk+2 such that
x[p1+...+pk)] <= x[p2+...+pk+1] <= x[p3+...+pk+2].

Also maybe use p1^2 + ... + p1^2 or even p1^1 + p2^2 + ... + pk^k or
even (p1^1)( p2^2)( pk^k). p1! + ... + pk! easy to deal with because
of univalence.

Opportunities for metamathematical phase transitions in the style of
Weiermann are fantastic.

The case k = 1 corresponds to Ultra Convergence/1 #898
https://cs.nyu.edu/pipermail/fom/2021-October/022897.html which goes
through the Ackermann hierarchy.

SEQUENCES OF PAIRS

THEOREM 2. For every infinite sequence of positive integers with each x[i] <= i,
there are primes p1 < ... < pk+2 such that
x[p1p2...pk] <= x[p2p3...pk+1| <= x[p3p4...pk+2]|.

THEOREM 8. For every infinite sequence from Z+^2 with each max(x[i])
<= i, there are primes p1 < ... < pk+1 such that
x[p2p3...pk+1| - x[p1p2...pk] lies in [0,infinity)2.

Theorem 8 also has the same PA metamathematical phenomena.

##########################################

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 911th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1
908: Base Theory Proposals for Third Order RM/2
909: Base Theory Proposals for Third Order RM/3
910: Base Theory Proposals for Third Order RM/4  10/15/21  3:15PM

Harvey Friedman