898: Ultra Convergence/1

[Harvey Friedman]

Ultra Convergence pertains to convergence in what we call subsequences.

DEFINITION 1. A subsequence is a finite or infinite sequence indexed
by strictly increasing positive integers.

E.g., (x_5, x_14, x_24, x_67) is a subsequence of length four.

We focus on the simplest kind of "convergence" or "Cauchy" property of
subsequences.

DEFINITION 2. A subsequence in a metric space is ultra convergent if
and only if each d(x_i+1,x_i+2)  <= 2^-i.

THEOREM 1. Every infinite sequence from [0,1] has an ultra convergent
infinite subsequence. This is provably equivalent to ACA0 over RCA0.

THEOREM 2. Every infinite sequence from [0,1] has ultra convergent
finite subsequences of every finite length. For all k there exists n
such that every infinite sequence from [0,1] has a length k ultra
convergent subsequence from the first n terms.

THEOREM 3. Let n >> k. Every sequence from [0,1] of length n has an
ultra convergent subsequence of length k.

THEOREM 4. Theorems 1-3 are provably equivalent to "Ackermann function
is total" over RCA0. Theorem 3 is provably equivalent to "Ackermann
function is total" over EFA. The >> in Theorem 3 eventually dominates
all primitive recursive functions.

In fact there is a universal constant c such that the n >> k+c
strictly dominates the k-th function in the standard Ackermann
hierarchy from k onwards.

I'm convinced that even the following holds, but it does need some
careful computations I don't have the time for at the moment: For k >=
3, n >> k strictly dominates the k-th function. And also I haven't had
the time to do careful upper bounds, but n >> k is strictly dominated
by the (k+c)-th function starting at k, k >= 3, or something roughly
like that.

It would seem that for k = 8 (or so), the n >> k is a COMPLETELY
RIDICULOUS integer. Maybe 8 can be lowered considerably.

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

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 898th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM
820: Sugared ZFC Formalization/2  6/14/18  6:45PM
821: Beyond Perfectly Natural/18  6/17/18  1:11AM
822: Tangible Incompleteness/1  7/14/18  10:56PM
823: Tangible Incompleteness/2  7/17/18  10:54PM
824: Tangible Incompleteness/3  7/18/18  11:13PM
825: Tangible Incompleteness/4  7/20/18  12:37AM
826: Tangible Incompleteness/5  7/26/18  11:37PM
827: Tangible Incompleteness Restarted/1  9/23/19  11:19PM
828: Tangible Incompleteness Restarted/2  9/23/19  11:19PM
829: Tangible Incompleteness Restarted/3  9/23/19  11:20PM
830: Tangible Incompleteness Restarted/4  9/26/19  1:17 PM
831: Tangible Incompleteness Restarted/5  9/29/19  2:54AM
832: Tangible Incompleteness Restarted/6  10/2/19  1:15PM
833: Tangible Incompleteness Restarted/7  10/5/19  2:34PM
834: Tangible Incompleteness Restarted/8  10/10/19  5:02PM
835: Tangible Incompleteness Restarted/9  10/13/19  4:50AM
836: Tangible Incompleteness Restarted/10  10/14/19  12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20  02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory  2/8/20  2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20  12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1:  5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1  5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1  6/19/20 1132PM :
860: Unary Regressive Growth/1  8/120  9:50PM
861: Simplified Axioms for Class Theory  9/16/20  9:17PM
862: Symmetric Semigroups  2/2/21  9:11 PM
863: Structural Mapping Theory/1  2/4/21  11:36PM
864: Structural Mapping Theory/2  2/7/21  1:07AM
865: Structural Mapping Theory/3  2/10/21  11:57PM
866: Structural Mapping Theory/4  2/13/21  12:47AM
867: Structural Mapping Theory/5  2/14/21  11:27PM
868: Structural Mapping Theory/6  2/15/21  9:45PM
869: Structural Proof Theory/1  2/24/21  12:10AM
870: Structural Proof Theory/2  2/28/21  1:18AM
871: Structural Proof Theory/3  2/28/21  9:27PM
872: Structural Proof Theory/4  2/28/21  10:38PM
873: Structural Proof Theory/5  3/1/21  12:58PM
874: Structural Proof Theory/6  3/1/21  6:52PM
875: Structural Proof Theory/7  3/2/21  4:07AM
876: Structural Proof Theory/8  3/2/21  7:27AM
877: Structural Proof Theory/9  3/3/21  7:46PM
878: Structural Proof Theory/10  3/3/21  8:53PM
879: Structural Proof Theory/11  3/4/21  4:22AM
880: Tangible Updates/1  4/15/21 1:46AM
881: Some Logical Thresholds  4/29/21  11:49PM
882: Logical Strength Comparability  5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans  5/16/21 1:29:44
884: Low Strength Zoo/1  5/16/21 1:34:
885: Effective Forms  5/16/21 1:47AM
886: Concerning Natural/1   5/16/21  2:00AM
887: Updated Adventures  9/9/21 9:47AM  2021
888: New(?) kinds of questions  9/9/21 12:32PM
889: Generating r.e. sets  9/12/21  3:38PM
890: Update on Tangible Incompleteness  9/18/21  9:50AM :
891: Remarks on Reverse Mathematics/1  9/21/21  12:50AM   :
892: Remarks on Reverse Mathematics/2  9/21/21  8:37AM :
893: Remarks on Reverse Mathematics/3  9/23/21  10:04PM
894: Update on Tangible Incompleteness/2 9/25/21 2:51AM
895: Provably Recursive Functions and Sigma02  9/27/21  1:21 AM
896: (R,<,0,1,+,-,x,Z)  9/27/21  4:52AM
897: Remarks on Reverse Mathematics/4  10/1/21  1:13AM

Harvey Friedman