[FOM] 688:Large Cardinals and Continuations/8

[Harvey Friedman]

THIS POSTING IS ENTIRELY SELF CONTAINED

We continue to fine tune the headline statement. This now looks rather
optimal (I have said this before), and I will give complete
definitions.

1. The symmetry that we want to use is what I call regional
translation symmetry - of subsets S of Q^k. We identify two regions
A,B in Q^k, and assert that there is a translation from A onto B which
also maps the part of S lying in A onto the part of S lying in B.
2. The most convenient regions for this purpose are special kinds of
finite unions of rectangles - actually a product of rational intervals
and finite sets of rationals.
3. It is also possible to use rectangles, as we indicate.

SYMMETRIC MAXIMAL CONTINUATIONS
by
Harvey M. Friedman
June 9, 2016

1. Maximal Continuation.
2. Symmetric Maximal Continuation.
3. Finite Symmetric Rich Continuation.
4. Smoothly Maximal Continuation.
5. Rectangles.
6. Templates.
7. Subsets of N
8. Formal Systems Used.

We will present each statement first with only the numerical parameter
k. This is somewhat artificial, but it makes the presentation more
readily digestible. We will later present the obvious variant with the
maximum number of relevant numerical parameters. It is easy to see
that both formulations are equivalent. using dummy variables. The
versions with many numerical parameters are of course important for
further detailed studies.

1. MAXIMAL CONTINUATION

DEFINITION 1.1. Q,Z+,N is the set of all rationals, positive integers,
nonnegative integers, respectively. We use p,q for rationals and
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). Let S containedin Q^k. S|<p, S|<=p, S|>p,
S|>=p is the set of all elements of S all of whose coordinate are <p,
<=p, >p, >=p, respectively.

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 a k-continuation of A within C if and only if
A containedin B containedin C containedin Q^k, and every <=k element
subset of B is isomorphic to some subset of A. B is a maximal
k-continuation of A within C if and only if B is a k-continuation of A
within C, and no B U. {x} is an t-continuation of A within C.

We think of A containedin Q^k|<0 as a seed. We let the seed "grow"
within Q^k|<=k. We think of the continuations of A within Q^k|<=k as
plants. Maximal continuations of A within Q^k|<=k are thought of as
plants growing from A as much as possible, within the space constraint
Q^k|<=k.

THEOREM 1.1. Every A containedin Q^k|<0 has a maximal continuation
within Q^k|<k. Furthermore, there is an effective process that starts
with finite A and k, and produces a (normally infinite) maximal
continuation of A within Q^k|<=k.

The obvious constructions for Theorem 1.1 generally do not result in
maximal continuations with any 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. SYMMETRIC MAXIMAL CONTINUATION

We now introduce a vivid kind of symmetry in subsets S of Q^k via
translation between regions A and B. We call this "regional
translational symmetry".

DEFINITION 2.1. Let S,A,B containedin Q^k. S translates from A onto B
if and only if there exists p in Q^k such that
i. A+p = B.
ii. (A intersect S) + p = (B intersect S).

In section 4 we use partial translational symmetry, defined as follows.

DEFINITION 2.2. Let S,A,B containedin Q^k. S translates from A into B
if and only if there exists p in Q^k such that
i. A+p = B.
ii. (A intersect S) + p containedin (B intersect S).

Generally speaking, we use rather nice sets A,B. However, A intersect
S and B intersect S will generally be rather complicated.

SYMMETRIC MAXIMAL CONTINUATION. SMC. For all finite subsets of
Q^2k|<0, some maximal k-continuation within Q^2k|<=k translates from
Q^k|<0 x N^k|<k onto Q^k|<0 x Z+^k|<=k.

THEOREM 2.1. SMC is implicitly Pi01 via the Goedel Completeness
Theorem. In fact, SMC is implicitly Pi01 over WKL_0.

Proof: First observe that there is a unique translation from Q^k|<0 x
N^k|<k onto Q^k|<0 x Z+^k|<=k, and the use of addition here is
severely limited. Is then easy to see the SMC asserts that each of an
effectively given list of sentences in first order predicate calculus
with equality have a countable model. Now apply Goedel's completeness
Theorem. QED

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

It is doubtful if there exists a fixed k for which SMC corresponds
exactly to ZFC in this sense: SMC for k is provably equivalent to
Con(ZFC) over WKL_0. This has a better chance with the introduction of
the full panoply of parameters, although even this probably is not the
case. We probably need to adjust more parameters as well as the two
regions.

For which k is SMC for k independent of ZFC? SMC for k = 1 doesn't
pack any punch since 1-continuations are so trivial.

THEOREM 2.3. SMC for k = 1 is provable in RCA_0.

But our proof of SMC for k = 2 uses far more than ZFC. We have not
formed an opinion as to whether this is independent of ZFC, but it
takes the following nice form:

SYMMETRIC MAXIMAL CONTINUATION (tiny). SMC (tiny). For all finite
subsets of Q^4|<0, some maximal 2-continuation within Q^4|<=2
translates from Q^2|<0 x {0,1}^2 onto Q^2|<0 x {1,2}^2.

Because we are thinking of "seeds continuing (growing) to plants", it
would be particularly interesting to use 3 dimensions here. Here is
the full panoply of parameters:

SYMMETRIC MAXIMAL CONTINUATION (parametric). SMCp. For all finite
subsets of Q^n+m|<0, some maximal s-continuation within Q^n+m|<=r
translates from Q^n|<0 x N^m|<r onto Q^n|<0 x Z+^m|<=r.

The tiniest version that is not readily provable in ZFC is as follows.

SYMMETRIC MAXIMAL CONTINUATION (tiniest). SMC (tiniest). For all
finite subsets of Q^3|<0, some maximal 2-continuation within Q^3|<=2
translates from Q^|<0 x {0,1}^2 onto Q|<0 x {1,2}^2.

3. FINITE SYMMETRIC RICH CONTINUATION

Note that even though SMC is implicitly Pi01, it is 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, so that
finite rich continuations can always be found.

DEFINITION 3.1. The height of a rational, rational vector, or finite
set of rational vectors, 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 3.2.  B is a rich k-continuation of A within C if and only
if B is a k-continuation of A within C, and no B U. {x}, hgt(x) <=
hgt(A), is an k-continuation of A within C.

THEOREM 3.1. For all  finite subsets of Q^2k|<0, some finite rich
k-continuation within Q^2k|<=k translates from Q^k|<0 x N^k|<k onto
Q^k|<0 x Z+^k|<=k.

FINITE SYMMETRIC RICH CONTINUATION. FSRC. For all  finite subsets of
Q^2k|<0, some two successive finite rich k-continuations within
Q^2k|<=k translate from Q^k|<0 x N^k|<k onto Q^k|<0 x Z+^k|<=k.

FINITE SYMMETRIC RICH CONTINUATION (parametric). FSRCp. For all finite
subsets of Q^n+m|<0, some t successive finite rich s-continuations
within Q^n+m|<=r translate from Q^n|<0 x N^m|<r onto Q^n|<0 x
Z+^n|<=r.

FSRC, FSRCp 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 3.2. FSRC, FSRCp are provably equivalent to Con(SRP) over EFA.
For each fixed k, FSRC is provable in EFA.

4. SMOOTHLY MAXIMAL CONTINUATIONS

Here instead of continuing subsets of Q^k by subsets of Q^k, we
continue Q,k systems by Q,k systems.

DEFINITION 4.1. A Q,k system is a pair (A,R), where A containedin Q
and R containedin A^k. (A,R) is finite if and only if A is finite.
(A,R) is negative if and only if A containedin Q|<0.

DEFINITION 4.2. Let (A,R) be a Q,k system. (B,S) is a k-continuation
of (A,R) if and only if
i. (B,S) is a Q,k system.
ii. A U {0,1} containedin B.
iii. Every subset of S with <=k elements is isomorphic to some subset of R.

DEFINITION 4.3. Let (A,R) be a Q,k system. (B,S) is a smoothly maximal
k-continuation of (A,R) if and only if (B,S) is a k-continuation of
(A,R), and no (B|<=max(x),S U. {x}), min(x) < 0 < max(x), is a
k-continuation of (A,R).

DEFINITION 4.4. Let (A,R) be a Q,k system, B,C containedin Q^k. (A,R)
translates from B onto (into) C if and only if R translates from from
B onto (into) C.

SMOOTHLY MAXIMAL CONTINUATION. SMC. For all finite negative Q,2k
systems, some smoothly maximal k-continuation translates from Q^k|<1 x
Q^k|>=1 into Q^k|<1 x Q^k|>=2.

STRONG SMOOTHLY MAXIMAL CONTINUATION. SSMC. For all finite negative
Q,2k systems, some smoothly maximal k-continuation translates from
Q^k|<1 x Q^k|>=1 into Q^k|<1 x Q^k|>=2 and from Q[1,k]^k x {k+(3/2)}^k
onto Q[2,k+1]^k  x {k+(3/2)}^k.

DEFINITION 4.5. Let (A,R) be a Q,k system. (B,S) is a smoothly rich
k-continuation of (A,R) if and only if (B,S) is a k-continuation of
(A,R), and no (B|<=max(x),S U. {x}), min(x) < 0 < max(x), hgt(x) <=
hgt(A), is a k-continuation of (A,R).

THEOREM 4.1. SMC is provably equivalent to Con(SRP) over WKL_0. SSMC
is provably equivalent to Con(HUGE) over WKL_0. This holds even for a
fixed k.

FINITE SMOOTHLY MAXIMAL CONTINUATION. FSMC. For all finite negative
Q,2k systems, some two successive finite smoothly rich k-continuations
translate from Q^k|<1 x Q^k|>=1 into Q^k|<1 x Q^k|>=2.

STRONG FINITE SMOOTHLY MAXIMAL CONTINUATION. SFSMC. For all finite
negative Q,2k systems, some two successive finite smoothly rich
k-continuations translates from Q^k|<1 x Q^k|>=1 into Q^k|<1 x Q^k|>=2
and from Q[1,k]^k x {k+(3/2)}^k onto Q[2,k+1]^k  x {k+(3/2)}^k.

The above two statements are explicitly Pi02. A priori upper bounds
can be given on the heights of the rich k-continuations, resulting in
explicitly Pi01 forms.

THEOREM 4.2. FSMC is provably equivalent to Con(SRP) over EFA. SFSMC
is provably equivalent to Con(HUGE) over WKL_0.

The same results apply to obvious parametric forms of SMC, SSMC, FSMC,
SFSMC. (Among the parameters to be introduced is the number t of
successive continuations, rather than just t = 2).

5. RECTANGLES

For all of our statements, we have been using finite unions of
rectangles. It is possible to use rectangles instead.

DEIFNITION 5.1. A rational interval is an interval in Q whose
endpoints are from Q U {-infinity,infinity}. A rational rectangle is a
product of finitely many rational intervals.

In sections 2-4 we have used

Q^k|<0 x N^k|<k
Q^k|<0 x Z+^k|<=k.
Q^k|<1 x Q^k|>=1
Q^k|<1 x Q^k|>=2
Q[1,k]^k x {k+(3/2)}^k
Q[2,k+1]^k  x {k+(3/2)}^k

Note that the last four are rational rectangles. The first two can be
viewed either as finite union of rational rectangles, or a product of
rational intervals and finite sets of rationals. Obviously the later
is a special kind of finite union of rational rectangles.

An alternative to using the first two is to use

Q^k|<0 x {(0,...,k-1)}.
Q^k|<0 x {(1,...,k)}.

The same results hold.

6. TEMPLATES

We use three categories of subsets of Q^k. Rectangles - X1, X2, X3.

X1. Rectangles.
X2. Products of finite sets and rationals.
X3. Finite unions of Rectangles.

MAXIMAL CONTINUATION TEMPLATE. Let A,B,C,D be in Xi,  in a common
dimension. For all finite subsets of A, some maximal t-continuation
within B translates from C onto D.

SMOOTHLY MAXIMAL CONTINUATION TEMPLATES. Let A,B,C,D be in Xi. For all
finite negative Q,k systems, some smoothly maximal t-continuation
translates from A (onto, into) B, and C (onto, into) D.

The statements in sections 2,3 fall under the Maximal Continuation
Template with either X2 or X3. We can instead use only X1.

The statements in section 4 fall under the Smoothly Maximal
Continuation Terminal, with X1,X2,X3. We can clearly get away with
only X1.

Obviously SMC is a special case of HCT, and is equivalent to Con(SRP)
over WKL_0.

CONJECTURE. Every instance of the Maximal Continuation Template is
refutable in RCA_0 or provable iin SRP.

7. SUBSETS OF N

see next posting

8. FORMAL SYSTEMS USED

see next posting

***********************************************
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 688th 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

Harvey Friedman