[FOM] 685:Large Cardinals and Continuations/6

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

We have found some major simplifications in the implicitly Pi01 and
explicitly Pi01 statements equivalent to Con(HUGE), and to the
statements in the positive integers equivalent to Con(MAH).

***IMPLICITLY Pi01 FOR HUGE***

DEFINITION 1. A Q,k system is a pair (A,R), where A containedin Q, and
R containedin A^k. A negative Q,k system is a Q,k system with its
domain A containedin Q|<0. We say that (A,R) is a part of (B,S) if and
only if A containedin B and R containedin S. The cardinality of a Q,k
system is the cardinality of its domain. Isomorphisms from (A,R) onto
(B,S)  are order preserving bijections h:A into B that send R onto S.
p > A containedin Q^k if and only if for all y in A, p > max(y). x in
Q^k is increasing if and only if x+1 <= ... <= x_k.

DEFINITION 2. (B,S) is an r-continuation of the Q,k system (A,R) above
C containedin Q if and only if
i. (A,R) is a part of the Q,k system (B,S),.
ii. Every element of B]A is greater than every element of C.
iii. Every part of (B,S) of cardinality <=r is isomorphic to some part of (A,R).
If r = 2 then we omit r.

NOTE: Bringing in C in this way has not been important for our first,
and most basic continuation theory, for "plants into seeds". There we
brought in C for "continuations within C". So before, we are
interested in growth within C, and here we are interested in growth
above C.

DEFINITION 3. (B,S) is a smoothly maximal r-continuation of the Q,k
system (A,R) above C containecin Q if and only if (B,S) is an
r-continuation of (A,R) above C, where no (B|<=max(x),S|<max(x) U.
{x})  is an r-continuation of (A,R) above C.

DEFINITION 4. Let (A,R) be a Q,k system. A self embedding h of (A,R)
is a one-one h:A into A such that for all p_1,...,p_k in A,
R(p_1,...,p_k) if and only if R(h(p_1),...,h(p_k)).

SMOOTHLY EMBEDDED MAXIMAL CONTINUATIONS. SEMC. For finite negative Q,k
systems, some smoothly maximal continuation above its domain has a
self embedding with a least point moved.

We now weaken smooth/<= maximality.

DEFINITION 5. (B,S) is a smoothly/<= r-continuation of the Q,k system
(A,R) above C containedin Q if and only if (B,S) is an r-continuation
of (A,R) above C, where no (B|<=max(x),S|<max(x) U. {x}) , x
increasing, is an r-continuation of (A,R) above C.

DEFINITION 6. We say that B is atomic in the Q,k system (A,R) if and
only if B = {x: (A,R) |= phi(x)}, where phi is atomic, with parameters
allowed from A. B is locally atomic in (A,R) if and only if each B|<=n
is atomic in (A,R).

SMOOTHLY/<= EMBEDDED MAXIMAL CONTINUATIONS. SEMC(<=). For finite
negative Q,k systems, k >= 3, some smoothly/<= maximal continuation
above its domain has a nontrivial locally atomic self embedding.

THEOREM 1. SEMC is provably equivalent to Con(SRP) over WKL_0.
SEMC(<=) are provably equivalent to Con(HUGE) over WKL_0.

***EXPLICITLY Pi01 FOR HUGE***

DEFINITION 7. The height of x in Q^k or E containedin Q^k is the least
n such that all of the rationals that appear are the ratio of two
integers of magnitude at most n. We write hgt(x), hgt(A).

DEFINITION 8. (B,S) is a smoothly/<= r-continuation of the Q,k system
(A,R) above C containedin Q if and only if (B,S) is an r-continuation
of (A,R) above C, where no (B|<=max(x),S|<max(x) U. {x}) , x
increasing, hgt(x) <= hgt(A), is an r-continuation of (A,R) above C.

DEFINITION 9. Let (A,R) be a Q,k system and B containedin Q^k. We say
that B is very locally atomic if and only if each B|<=n is atomic with
parameters of height <= 8n.

FINITE SMOOTHLY/<= RICH CONTINUATIONS. FSRC(<=). Each finite negative
Q,k system (A,R) starts k successive finite smoothly/<= rich
continuations above A, where each |<=k has a very locally atomic self
embedding moving 0.

FSMSC(<=) is explicitly Pi02. An obvious bound can used to convert it
to explicitly Pi01.

THEOREM 2. FSRC(<=) is provably equivalent to Con(HUGE) over EFA.

***Pi01 FOR THE MAHLO HIERARCHY***
In the nonnegative integers

DEFINITION 8. Let A,B containedin N. We say that A,B are k-isomorphic
if and only if A,B are of the same (possibly infinite) cardinality,
and for any signed sum of at most k elements of A, the corresponding
signed sum from elements of B (under the unique order preserving
bijection from A onto B) has the same sign - positive, negative, or 0.

DEFINITION 9. Let X containedin N. A proper k sum from X is an
unsigned sum of k elements of X greater than all of its summands. The
powers of r are the r^i, i >= 0.

DEFINITION 10. Let A containedin N. B is a k,+ continuation of A above
C containedin N if and only if
i. A containedin B containedin N.
ii. Every element of B\A is greater than every element of C.
iii. A,B have the same proper k sums up to isomorphism.

THEOREM 3. Every subset of N has a maximal k,+ continuation.

DEFINITION 11. B is an optimal k,+ continuation of A above C if and
only if B is a k,+ continuation of A above C, where no B U. {n}  is a
k,+ continuation of A above C, with n a proper k sum from A.

PROPOSITION 1. Let A containedin N be finite. For all k, A has k
successive optimal k,+ continuations above A, each containing an
infinite geometric progression.

THEOREM 4. Proposition 1 is provably equivalent to Con(MAH) over ACA.
In fact, there is a fixed finite A such that Proposition 1 for A is
provably equivalent to Con(MAH) over ACA.

We now focus on some more explicit forms.

PROPOSITION 2. Every A containedin [k] has two successive optimal k,+
continuations containing the powers of (8k)!,

FINITE BINARY OPTIMALITY IN N . FBON. Every A containedin [k] has r
successive optimal 2,+ continuations above A containing the first n
powers of (8kr)!, and lying below the next.

FINITE MULTIPLE OPTIMALITY IN N. FMON. Every A containedin [k] has two
successive optimal r,+ continuations above A containing the first n
powers of (8kr)!, and lying below the next.

FBON and FMON are obviously explicitly Pi01 without modification.

THEOREM  5. FBON, FMON are provably equivalent to Con(MAH) over ACA.

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

Harvey Friedman