[FOM] 682:Large Cardinals and Continuations/3

Harvey Friedman hmflogic at gmail.com
Thu Jun 2 08:05:27 EDT 2016


TECHNICAL PART OF THIS POSTING IS LARGELY SELF CONTAINED
see 681:Large Cardinals and Continuations/2. for informal discussion

The main point of this posting is to get to HUGE.

We begin with a review of the notions that we are using, starting from
the beginning.

So far, all of the objects are subsets of the Q^k. We use only one
notion of continuation:

DEFINITION 1. S is an r-continuation of A containedin Q^k if and only
if A containedin S containedin Q^k, and every subset of S of
cardinality r is isomorphic to a subset of A. For the important case
of  r = 2, we omit r.

Here isomorphisms respect <.

We then use various notions of maximality.

DEFINITION 2. S is a maximal r-continuation of A containedin Q^k
within B if and only if S containedin B is an r-continuation of A,
where no S U. {x}, x in B, is an r-continuation of A. In case r = 2,
we omit r.

EMBEDDED MAXIMAL CONTINUATIONS. EMC. For finite subsets of Q^k|<0,
some maximal continuation within Q^k|<=n is partially self embedded by
the function p if p < 0; p+1 if p = 0,...,n-1.

DEFINITION 3. S is a rich r-continuation of A containedin Q^k within B
if and only if S containedin B is an r-continuation of A, where no S
U. {x}, x in B of height at most that of A, is an r-continuation of A.

This is the number theorist's height, and is the least integer such
that all of the rationals involved can be written as a ratio of two
integers of magnitude at most that integer.

FINITE EMBEDDED MAXIMAL CONTINUATIONS. FEMC. For finite subsets of
Q^k|<0, some two successive finite rich 3-continuations within Q^k|<=n
are partially self embedded by the function p if p < 0; p+1 if p =
0,...,n-1.

The above is explicitly Pi02, and with a priori bounds, can be put in
explicitly Pi01 form.

So far, we have used two notions of maximal r-continuations. We now use a third.

DEFINITION 4. S is a step maximal r-continuation of A containedin Q^k
if and only if each S|<=n is a maximal r-continuation of A within
Q^k|<=n.

EMBEDDED STEP MAXIMAL CONTINUATIONS (partial). ESMCp. For finite
subsets of Q^k|<0, some step maximal continuation is partially self
embedded by the function p if p < 0; p+1 if p in N.

EMBEDDED STEP MAXIMAL CONTINUATIONS (total). ESMCt. For finite subsets
of Q^k|<0, some step maximal continuation is self embedded by a
function which is p if p < 0; p+1 if p in N.

****************************

The above statements are equivalent to Con(SRP).  We now use some
additional notions of maximality in order to get to HUGE.

We make a useful change of perspective. Instead of continuing subsets
of Q^k, we continue pairs (A,R), where A containedin Q and R
containedin A^k.

First we get to just Con(SRP) again, with this change of perspective.

DEFINITION 5. A Q-system is a pair (A,R), where A containedin Q and R
containedin Q^k. (A,R) is a Q-system on (its domain) A. 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-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.

DEFINITION 6. (B,S) is an r-continuation of the Q-system (A,R) if and
only if (A,R) is a part of the Q-system (B,S), 0 in B, and every part
of (B,S) of cardinality r is isomorphic to some part of (A,R). If r =
2 then we omit r.

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

DEFINITION 8. Let (A,R) be a Q system. A self embedding h of (A,R) is
a one-one h:Q into Q 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)). Here R containedin
Q^k.

SMOOTHLY EMBEDDED MAXIMAL CONTINUATIONS. SEMC. For Q-systems on finite
subsets of Q^k|<0, some smoothly maximal continuation is self embedded
by the function p if p < 0; p+1 otherwise.

We now present a weakened form of smoothly maximal r-continuations.

DEFINITION 8. (B,S) is a smoothly/<= maximal r-continuation of (A,R)
if and only if (B,S) is an r-continuation of (A,R), where no
(B|<=max(x),S|<max(x) U. {x}) x increasing, is an r-continuation of
(A,R).

DEFINITION 9. Let x in Q^k. x is positive if and only if min(x) > 0. x
is increasing if and only if x_1 <= ... <= x_k. E containedin Q^k is
positive if and only if all elements of E are positive. The sections
of Q-systems (A,R) are the sets of one lower dimension obtained from R
by fixing one or more arguments in any positions.

SMOOTHLY/<= EMBEDDED MAXIMAL CONTINUATIONS (<=). SEMC(<=). For
Q-systems on finite subsets of Q^k|<0, the positive elements and
positive upper bounded sections of some smoothly/<= maximal
continuation are closed under +1.

Positive means all rationals involved are > 0. 1-sections are the
result of fixing the first argument.

SEMC is equivalent to Con(SRP) over WKL_0. SEMC(<=) is equivalent to
Con(HUGE) over WKL_0.

***********************************************
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 682nd 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

Harvey Friedman


More information about the FOM mailing list