[FOM] 690:Two Brief Sketches
Harvey Friedman
hmflogic at gmail.com
Mon Jun 13 01:18:34 EDT 2016
Now is a good time to present two brief proof sketches. EXERCISE: Find
at least some small bugs below.
First that the basic statement $ is provably equivalent to not CH.
This is something that is very close to things well known to set
theorists that set theorists certainly do not need to see this proof.
Other people may want to see this.
Second is the proof from large cardinals of my latest headline
statement that is implicitly Pi01.
Both proof sketches are reasonably short so that they make a
reasonable length FOM posting.
$. For all f:R into R there exists x,y in R such that x is not f at an
integral shift of y, and y is not f at an integral shift of x.
We first prove $ from not CH. Let f:R into R. Let A be any set of
reals of cardinality omega_1. Let x be a real that is not the value of
f at any integral shift of any element of A. Choose y in A which is
not the value of f at any integral shift of x. So x,y are as required.
QED
Now assume CH. We find a counterexample f:R into R to $. We use the
equivalence relation: x,y are equivalent iff x-y is an integer. We
begin by defining f(x+2n) for 0 <= x < 1. Set f(x+2n) = x+n. Note that
we already have this: If x,y are equivalent then x is the value of f
at an integral shift of y. Now enumerate the equivalence class without
repetition of length omega_1. We have not yet defined f on infinitely
many elements of each equivalence class. So we are free to define f on
these remaining elements so that f maps each equivalence class onto at
least the union of all of the previous equivalence classes. Now let
x,y in R. If x,y are equivalent then x,y is as required. Otherwise, x
appears earlier or later than y in the transfinite enumeration. If x
appears earlier, then x is the value of f at some integral shift of y.
If x appears later, then y is the value of f at some integral shift of
x. QED
We now sketch a proof from large cardinals of the current headline statement:
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
{(0,...,k-1)} onto Q^k|<0 x {(1,...,k)}.
We use the following linear ordering. Let kappa be a suitable large
cardinal. The points are pairs (alpha,p), alpha < kappa, where p is in
Q[0,1). These pairs are ordered lexicographically, using the standard
ordering on Q[0,1), forming (D,<lex). Let D' be D without (0,0).
We will actually be using (D',<lex) and (D',<*).
We now start with the given finite subset A of Q^2k|<0. We use an
isomorphic copy of A, which is a finite subset A' of {(0,p): 0 < p <
1}^2k, where A via < is isomorphic to A' via <lex .
The notion of k-continuations of 2k-dimensional sets make perfectly
good sense in the context of any linear ordering, and we use it for
(D',<lex).
We build a maximal k-continuation of A' within (D',<lex)^2k, constructed
along kappa as follows. For every alpha, let S[alpha] = {(beta,p):
beta < alpha}, T[alpha] = S[alpha] U {(alpha,0)}.
Note that the S[alpha] and T[alpha] are initial segments under <lex.
We start with a maximal k-continuation of A' within T[1]^2k. Suppose we
have built a maximal k-continuation of A' within T[alpha]^2k. We extend
it to a maximal k-continuation of A' within T[alpha + 1]^2k.
Suppose we have built a tower of k-continuations of A' within each
T[alpha]^2k, alpha < lambda, lambda a limit. We take the union, which
is a k-continuation of A' within S[lambda]^2k, and then extend it to a
k-continuation of A' within T[lambda]^2k.
Thus we obtain a maximal k-continuation C[alpha] of A' within
T[alpha]^2k, for each alpha < kappa. Note that for alpha < beta,
C[alpha] = C[beta] intersect T[alpha]^2k.
We now apply the large cardinal property of kappa to obtain
uncountable cardinals
lambda_0 < lambda_1 < ... < lambda_k < kappa such that the
following holds. For all x in S[lambda_0]^k, we have
(x,(lambda_0,0),(lambda_1,0),...,(lambda_k-1,0)) lies in C if and
only if (x,(lambda_1,0),(lambda_2,0),...,(lambda_k,0)) lies in C.
The above makes use of an easy to construct well ordering of D' where
each S[alpha] comes entirely before T[alpha]\S[alpha) which comes
entirely before S[alpha+1]\T[alpha]. Then S[lambda_0] consists of the
points in this well ordering whose position is < lambda_0, and each
(lambda_i,0) has position lambda_i. NOTE: Of course, (D',<lex) is not
well ordered.
This verifies SMC except that we have the structure
(T(lambda_k),A',<lex,(lambda_0,0),...,(lambda_k,0),C[lambda_k]) living
in (D',<lex) instead of some structure (Q|<=k,A,<|<=k,0,...,k,C#),
living in (Q,<Q). However, we can make a standard countable
substructure argument to push our gigantic structure down to an
appropriate countable substructure, and then isomorphically to
(Q|<=k,A,<,0,...,k,C#), with C# as required. QED
***********************************************
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 690th 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 Jun 9 23:41:05 EDT 2016
689: Large Cardinals and Continuations/9 Jun 11 14:51:56 EDT 2016
Harvey Friedman
More information about the FOM
mailing list