[FOM] 692:Large Cardinals and Continuations/11

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

Here we have further fine tuning, and we focus on standard symmetry -
congruence on two line segments.

LARGE CARDINALS AND CONTINUATIONS
subsets of Q^k, finite subsets of N
by
Harvey M. Friedman
June 15, 2016

1. Maximal Continuation.
2. Congruence.
3. Congruent Maximal Continuation.
4. Congruent Rich Continuation.
5. Smoothly Maximal Continuation.
6. Templates.
7. Formal Systems Used.
9. The Future.

1. MAXIMAL CONTINUATION

This section is slightly modified from
http://www.cs.nyu.edu/pipermail/fom/2016-June/019903.html The main
change is that I now prefer to use Q[-n,m] rather than Q|<=k and
Q[-n,0) rather than Q|<0.

DEFINITION 1.1. Q,Z+,N is the set of all rationals, positive integers,
nonnegative integers, respectively. We use p,q for rationals and
i,j,k,n,m,r,s,t for positive integers, with and without subscripts, unless
otherwise indicated. A U. B is A U B if A,B are disjoint; undefined
otherwise (disjoint union). Q[p,q], Q[p,q) is Q intersect [p,q], Q
intersect [p,q), respectively. For S containedin Q^k, S|<p = S
intersect (-infinity,p)^k.

DEFINITION 1.2. Let A containedin Q^k. h is an isomorphism from A onto
B if and only if B containedin Q^k, and h:Q into Q is an (everywhere
defined) order preserving bijection sending A onto B by the coordinate
action. (There are some variants of this, but not for finite A, the
only case we use). B is an r-continuation of A within C if and only if
A containedin B containedin C containedin Q^k, and every <=r element
subset of B is isomorphic to some subset of A. B is a maximal
r-continuation of A within C if and only if B is an r-continuation of A
within C, and no B U. {x} is an r-continuation of A within C.

We think of A containedin Q[-n,0)^k as a seed. We let the seed "grow"
within Q[-n,m]^k. We think of the r-continuations of A within Q[-n,m]^k as
plants. Maximal continuations of A within Q[-n,m]^k are thought of as
plants growing from A as much as possible, under the space constraint
Q[-n,m]^k.

THEOREM 1.1. Every A containedin Q[-n,0)^k has a maximal r-continuation
within Q[-n,m]^k. Furthermore, there is an effective process that starts
with finite A and k,n,m and produces a (normally infinite) maximal
r-continuation of A within Q[-n,m]^k.

The obvious constructions for Theorem 1.1 generally do not result in
maximal continuations with any significant kind of symmetry.

DEFINITION 1.3. A sentence J is implicitly Pi01 if and only if for
some algorithm alpha processing finite strings, ZFC proves "J holds if
and only if alpha runs forever with the empty string input". J is
implicitly Pi01 over a formal system T if and only if t proves "J
holds if and only if alpha runs forever with the empty string input".

2. CONGRUENCE

DEFINITION 2.1. Let S,A,B contained Q^k. An isometry from A onto B is
a bijection f:A onto B which is Euclidean distance preserving. S is
congruent from A onto B if and only if there is an isometry from S
intersect A onto S intersect B.

We will be focusing on open line segments A,B.

DEFINITION 2.2. For x,y in Q^k, x||y is the open line segment in Q^k
from x to y. Here x||x is emptyset.

THEOREM 2.1. (background) In Q^k, x||y and z|w are congruent if and
only if d(x,y) = d()z,w).

3. CONGRUENT MAXIMAL CONTINUATION

CONGRUENT MAXIMAL CONTINUATION (specific). CMCs. For finite subsets of
Q[-k,0)^k, some maximal 2-continuation within Q[-k,k]^k is congruent
from (0,1,...,k-1)||(1,1,...,k-1) onto open (0,2,...,k)||(1,2,...,k).

CONGRUENT MAXIMAL CONTINUATION (parametric). CMCp. For finite subsets
of Q[-n,0)^k, some maximal r-continuation within Q[-n,m]^k is
congruent from any (i+1,...,i+k)||(i+2,i+2,...,i+k) onto any
(j+1,...,j+k)||(j+2,j+2,...,j+k), -1 <= i,j <= m-k.

THEOREM 3.1. CMCs, CMCp are implicitly Pi01 via the Goedel Completeness
Theorem. In fact, SMCs, SMCp are implicitly Pi01 over WKL_0.

THEOREM 3.2. SMCp is provable in SRP+. If SRP is consistent, SMC is not
provable in SRP. For each fixed k, SMCp is provable in SRP. There is no
finite fragment of SRP which, for each fixed k, proves SMCs (assuming
SRP is consistent).  Assuming ZFC is consistent, there is a fixed k
for which SMCs is not provable in ZFC. SMCs, SMCp, and also SMCs, SMCp for
some fixed k are independent of ZFC (assuming SRP is consistent). SMCs,
SMCp are provably equivalent to Con(SRP) over WKL_0.

4. CONGRUENT RICH CONTINUATION

Note that even though SMC, SMCp are implicitly Pi01, they are not explicitly
Pi01, because in general, maximal continuations are infinite.

We now give an explicitly Pi01 form of SMC by weakening the maximality
to "rich", using the notion of height from number theory.

DEFINITION 4.1. The height of a rational, rational tuple, or finite
set of rational tuples, is the least integer i such that every
rational number involved is the ratio of two integers of magnitude at
most i. The height of an infinite set of rational vectors is infinity.
We use hgt for height.

DEFINITION 4.2.  B is a rich r-continuation of A within C if and only
if B is a FINITE r-continuation of A within C, and no B U. {x}, hgt(x) <=
hgt(A), is an r-continuation of A within C.

THEOREM 4.1. For finite subsets of Q[-n,0]^k, there is a rich
r-continuation within Q[-n,m]^k. In fact, there are infinitely many
successive rich r-continuations within Q[-n,m]^k.

We can obtain our congruence with just one continuation.

THEOREM 4.2. For finite sets of Q[-k,0]^k, some rich r-continuation
within Q[-k,k]^k is congruent from (0,1,...,k-1)||(1,1,...,k-1) onto
(0,2,...,k)||(1,2,...,k).

CONGRUENT RICH CONTINUATION (specific). CRC. For finite subsets of Q[-k,0]^k,
some 2 successive rich k-continuations within Q[-k,k]^k are
congruent from (0,1,...,k-1)||(1,1,...,k-1) onto (0,2,...,k)||(1,2,...,k).

CONGRUENT RICH CONTINUATION (parametric). CRCp. For finite subsets of
Q[-n,0]^k, some t successive rich r-continuations within Q[-n,m]^k are
congruent from
any (i+1,...,i+k)||(i+2,i+2,...,i+k) onto any
(j+1,...,j+k)||(j+2,j+2,...,j+k), -1 <= i,j <= m-k.

FRC, FRCp are explicitly Pi02. There is an obvious a priori
exponential upper bound on the height of the successive finite rich
continuations. This results in explicitly Pi01 statements.

THEOREM 4.3. SRC, SRCp are provably equivalent to Con(SRP) over EFA.

5. SMOOTHLY MAXIMAL CONTINUATIONS

Note that so far we have used two notions of maximal r-continuation.
The first is indeed called maximal r-continuation within C. The second
is rich r-continuation within C. The maximality condition, in both
cases, takes the form that there is no r-continuation S U. {x}, where
x is subject to a condition. In the case of maximal r-continuation,
the condition is just that x lies in C. In the case of rich
r-continuaion, the condition is that x lies in C and the height of x
is at most the height of what is being r-continued.

We now consider another kind of maximal r-continuation which we call
smoothly maximal r-continuation. Just as for maximal r-continuations,
this notion does not involve heights. We also have the analogous
smoothly rich r-continuation, which brings in heights in the same way
that rich r-continuations brings them in.

DEFINITIOIN 5.1. For S containedin Q^k, S# is the least set (E U
{0,1})^k  that contains S.

DEFINITION 5.2. Let A containedin Q^k. B is a smoothly maximal
r-continuation of A within C if and only if B is an r-continuation of
A within C, and no B|<max(x) U. {x}, x in B#, min(x) < 0 < max(x), is
an r-continuation of A within C.

CONGRUENT SMOOTHLY MAXIMAL CONTINUATION. CSMC. For finite subsets of
Q[-k,0)^k, some smoothly maximal k-continuation is congruent from
Q[-k,0) x Q[0,k-1]^k-1 into Q[-k,0) x Q[1,k]^k-1.

STRONG CONGRUENT SMOOTHLY MAXIMAL CONTINUATION. SCSMC. For finite
subsets of Q[-k,0)^k, some smoothly maximal k-continuation is
congruent from Q[-k,0) x Q[0,k-1]^k-1 into Q[-k,0) x Q[1,k]^k-1 and
congruent from Q[0,k/2] x {4k/3}^k-1 onto Q[1,3k/2] x {4k/3}^k-1.

DEFINITION 5.3. Let A containedin Q^k. B is a smoothly rich
r-continuation of A within C if and only if B is a FINITE
r-continuation of A within C, and no B|<max(x) U. {x}, x in B#, min(x)
< 0 < max(x), hgt(x) <= hgt(A), is an
r-continuation of A within C.

CONGRUENT SMOOTHLY RICH CONTINUATION. CSRC. For finite subsets of
Q[-k,0)^k, some k successive smoothly rich k-continuations are congruent
from Q[-k,0) x Q[0,k-1]^k-1 into Q[-k,0) x Q[1,k]^k-1.

STRONG CONGRUENT SMOOTHLY RICH CONTINUATION. SCSRC.  For finite
subsets of Q[-k,0)^k, some k successive smoothly rich k-continuations
are congruent from Q[-k,0) x Q[0,k-1]^k-1 into Q[-k,0) x
Q[1,k]^k-1 and congruent from Q[0,k/2] x {4k/3}^k-1 onto Q[1,3k/2]
x {4k/3}^k-1.

SSRC and SSSRC are explicitly Pi02. A priori upper bounds can be given
on the heights of the rich k-continuations, resulting in explicitly
Pi01 forms.

THEOREM 5.1. CSMC is provably equivalent to Con(SRP) over WKL_0. CSRC
is provably equivalent to Con(SRP) over WKL_0. The former holds even for a
fixed k.

THEOREM 5.2. SCSMC is provably equivalent to Con(HUGE) over WKL_0.
SCSRC is provably equivalent to Con(HUGE) over EFA.

6. TEMPLATES

MAXIMAL CONTINUATION TEMPLATE. MCT. Let A,B,C_1,...,C_i,D_1,...,D_i be
finite unions of rational rectangles in a common dimension, For
finite subsets of A and r >= 1, some maximal r-continuation within B
is congruent from C_1,...,C_i onto D_1,...,D_i, respectively.

CONJECTURE. Every instance of MCT is refutable from RCA_0 or provable in SRP.

This Conjecture looks quite accessible if all of the sides of the
rectangles involved are either singletons or have a common endpoint
with B.

SMOOTHLY MAXIMAL CONTINUATION TEMPLATE (onto). SMCTo. Same as MCT but with
maximal replaced by smoothly maximal.

SMOOTHLY MAXIMAL CONTINUATION TEMPLATE (into). SMCTi. Same as MCT but with
maximal replaced by smoothly maximal, and using "into".

CONJECTURE. Every instance of SMCTo and SMCTi is refutable from RCA_0
or provable in SRP.

This Conjecture looks quite accessible without restricting the
rational rectangles involved.

STRONG SMOOTHLY MAXIMAL CONTINUATION TEMPLATE. SSMCT. Same as MCT but
with maximal replaced by smoothly maximal, and using both "onto" and
"into".

Obviously instances of SMC, SMCp are instances of MCT. Each
instance of SSMC is an instance of SMCTi. Each instance of SSSMC is an
instance of SSMCT.

7. SUBSETS OF N

We can go down to finite subsets of N if we involve addition, and ask
for at least two successive continuations. . In fact, we
can work within N. Instead of imposing symmetry/congruence conditions,
we require
that geometric progressions appear in the continuations.
See http://www.cs.nyu.edu/pipermail/fom/2016-June/019892.html.

8. FORMAL SYSTEMS USED

EFA  Exponential Function Arithmetic.
RCA_0  Our base theory for Reverse Mathematics. Recursive
Comprehension Axiom Scheme naught.
WKL_0  Our second main theory for RM. Weak Konig's Lemma naught.
ACA  Arithmetic Comprehension Axiom Scheme. Somewhat stronger than our
main third theory for RM.
ZFC  Zermelo Frankel Set Theory with the Axiom of Choice.
SRP  Stationary Ramsey Property. ZFC + {there exists lambda with the k-SRP}_k
SRP+  ZFC + "for all k, there exists lambda with the k-SRP".
SMAH  Strongly Mahlo. ZFC + {there exists a strongly k-Mahlo cardinal"_k.
SMAH+  ZFC + "for all k there exists a strongly k-Mahlo cardinal".
HUGE  ZFC + {there exists an k-huge cardinal}_k.
HUGE+  ZFC + "for all k, there exists a k-huge cardinal".

9. THE FUTURE

A major issue is whether this independence arises already in dimension
k = 3, at least for ZFC. We believe that it does, probably, for SMCp.
SMC for k = 3. More dubious would be k = 3 for SMC.

Also we believe that SSMC and SSSMC for k = 3 are very strong provided
that we use parametric forms.

Progress on dimension reduction will have to wait until the more
urgent matter is addressed, that of producing a verifiable manuscript
with proofs of the claims make here. Proofs of SMC and SMCp in SRP+
are already presented in
http://www.cs.nyu.edu/pipermail/fom/2016-June/019905.html

***********************************************
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 692nd 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM
650: Necessary Irrelevance 3  12/24/15  2:42AM
651: Pi01 Incompleteness Update  2/2/16  7:58AM
652: Pi01 Incompleteness Update/2  2/7/16  10:06PM
653: Pi01 Incompleteness/SRP,HUGE  2/8/16  3:20PM
654: Theory Inspired by Automated Proving 1  2/11/16  2:55AM
655: Pi01 Incompleteness/SRP,HUGE/2  2/12/16  11:40PM
656: Pi01 Incompleteness/SRP,HUGE/3  2/13/16  1:21PM
657: Definitional Complexity Theory 1  2/15/16  12:39AM
658: Definitional Complexity Theory 2  2/15/16  5:28AM
659: Pi01 Incompleteness/SRP,HUGE/4  2/22/16  4:26PM
660: Pi01 Incompleteness/SRP,HUGE/5  2/22/16  11:57PM
661: Pi01 Incompleteness/SRP,HUGE/6  2/24/16  1:12PM
662: Pi01 Incompleteness/SRP,HUGE/7  2/25/16  1:04AM
663: Pi01 Incompleteness/SRP,HUGE/8  2/25/16  3:59PM
664: Unsolvability in Number Theory  3/1/16  8:04AM
665: Pi01 Incompleteness/SRP,HUGE/9  3/1/16  9:07PM
666: Pi01 Incompleteness/SRP,HUGE/10  13/18/16  10:43AM
667: Pi01 Incompleteness/SRP,HUGE/11  3/24/16  9:56PM
668: Pi01 Incompleteness/SRP,HUGE/12  4/7/16  6:33PM
669: Pi01 Incompleteness/SRP,HUGE/13  4/17/16  2:51PM
670: Pi01 Incompleteness/SRP,HUGE/14  4/28/16  1:40AM
671: Pi01 Incompleteness/SRP,HUGE/15  4/30/16  12:03AM
672: Refuting the Continuum Hypothesis?  5/1/16  1:11AM
673: Pi01 Incompleteness/SRP,HUGE/16  5/1/16  11:27PM
674: Refuting the Continuum Hypothesis?/2  5/4/16  2:36AM
675: Embedded Maximality and Pi01 Incompleteness/1  5/7/16  12:45AM
676: Refuting the Continuum Hypothesis?/3  5/10/16  3:30AM
677: Embedded Maximality and Pi01 Incompleteness/2  5/17/16  7:50PM
678: Symmetric Optimality and Pi01 Incompleteness/1  5/19/16  1:22AM
679: Symmetric Maximality and Pi01 Incompleteness/1  5/23/16  9:21PM
680: Large Cardinals and Continuations/1  5/29/16 10:58PM
681: Large Cardinals and Continuations/2  6/1/16  4:01AM
682: Large Cardinals and Continuations/3  6/2/16  8:05AM
683: Large Cardinals and Continuations/4  6/2/16  11:21PM
684: Large Cardinals and Continuations/5  6/3/16  3:56AM
685: Large Cardinals and Continuations/6  6/4/16  8:39PM
686: Refuting the Continuum Hypothesis?/4  6/616  9:29PM
687: Large Cardinals and Continuations/7  6/7/16  10:28PM
688: Large Cardinals and Continuations/8  6/9/16  11::41PM
689: Large Cardinals and Continuations/9  6/11/16  2:51PM
690: Two Brief Sketches  6/13/16  1:18AM
691: Large cardinals and Continuations/10  6/13/16  9:09PM

Harvey Friedman