[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