[FOM] 699::Refuting the Continuum Hypothesis?/9

[Harvey Friedman]

We now want to use the Consistent Truth Program to prove? |R| >
omega_omgea. Of course, it suffices to prove? that c is greater than
each omega_n.

Recall that we started with

$. For all f:R into R, there exist two (distinct) reals, neither being
the value of f at an integral shift of the other.

Recall the failed attempt

$[k]. For all f:R into R, there exist k distinct reals, none being the
value of f at an integral shift of the sum of the others.

where we show that for each k >= 2, $[k] is equivalent to |R| >=
omega_2. This is done in
http://www.cs.nyu.edu/pipermail/fom/2016-July/019952.html

We instead use

#[k]. For all f:R into R, there exist k (distinct) reals, none being
the value of f at an integral shift of the sum of the values of f at
the others.

Of course, #[k] lends itself well to some new simple languages for
Consistent Truth that are like the ones we have been using but
somewhat more expressive.

THEOREM 1. ZC proves #[k] iff |R| >= omega_k. (forall k)(#(k)) is
equivalent to |R| > omega_omega.

We will prove Theorem 1 by linking it up with a version of the
Kuratowski Free Set Theorem. This is in fixed finite dimensions.
.
FREE SET THEOREM

We give a self contained account of a theorem closely related to the
Kuratowski Free Set
Theorem. [A]^k is the set of all k element subsets of A.

THEOREM A. Let A be any set and k >= 1. The following
are equivalent.
i. For all f_1,f_2,... with domain [A]^k-1, there exist k distinct
elements of A, none being any f_i at the set of the others.
ii. |A| >= omega_k.

LEMMA A1. Let |A| = omega_1. For all f_1,f_2,... with domain [A]^0,
there exist an element of A which is not any f_i at the empty set.

LEMMA A2. Suppose k >= 1, and for every |A| = omega_k and f_1,f_2,...
with domain [A]^k-1, there exist k distinct elements of A, none being
any f_i at the set of the others.
Then for every |A| = omega_k+1 and f_1,f_2,... with domain [A]^k,
there exist k+1 distinct elements of A, none being any f_i at the set
of the others.

Proof: Let |A| = omega_k+1 and f_1,f_2,... have domain [A]^k. Let B
containedin A, |B| = omega_k, f[[B]^k] intersect A containedin B. Let
x in A\B. Let g_i:[B]^k-1 be given by g_i(y) = f_i(y U {x}). Let
y_1,...,y_k be distinct, none being any g_i at the set of the others.
Then y_1,...,y_k,x is as required. QED

LEMMA A3. Let |A| = omega. there exist f_1,f_2,... with domain [A]^0,
where for all x in A, x is some f_i at the empty set.

LEMMA A4. Suppose k >= 1, and for all |A| = omega_k-1, there exist
f_1,f_2,... with domain [A]^k-1, where for all distinct x_1,...,x_k in
A, each is some f_i at the set of the others. Then for all |A| =
omega_k, there exists f_1,f_2,... with domain [A]^k, where for all
distinct x_1,...,x_k+1 in A, each is some f_i at the set of the
others.

Proof: Let |A| = omega_k. We define f_1,f_2,... on [A]^k by
transfinite induction using an enumeration x_alpha, alpha < omega_k,
of A without repetition. Suppose the f_i have been defined on
[x_<alpha]^k, where for distinct y_1,...,y_k+1 in x_<alpha, each is
some f_i at the set of the others. It remains to define the f_i at the
y U {x_alpha}, y in [x_<alpha]^k-1. Let g_1,g_2,... have domain
[x_<alpha]^k-1, where for distinct y_1,...,y_k in x_<alpha, each is
some g_i at the set of the others. Define f_i(y U {x_alpha}) = g_i(y).
Thus each f_i has now been defined on [x_<=alpha]^k and has the
required property. QED

Proof of Theorem A: From Lemmas A1,A2, we see that by induction, ii
implies i in Theorem A, with >= replaced by = in ii. It is immediate
that we can use >= in ii.

>From Lemmas A3,A4, we obtain the following by induction. For all k >= 1,
and |A| = omega_k-1, there exist f_1,f_2,... with domain [A]^k, where
for all k+1 distinct elements of A, none are any f_i at the set of the
others. This establishes not ii implies not i in Theorem A, except
that we are using |A| = omega_k-1 instead of |A| < omega_k. It is
immediate that we can instead use |A| < omega_k. QED

FREE SET THEOREM WITH TUPLES

THEOREM B. Let A be any set and k >= 1. The following
are equivalent.
i. For all f_1,f_2,... with domain A^k-1, there exist k elements of
A, none being any f_i at any tuple drawn from the others.
ii. For all f_1,f_2,... with domain A^k-1, there exist k distinct elements of
A, none being any f_i at any tuple drawn from the others.
iii. |A| >= omega_k.

Proof: First of all, i,ii are equivalent because we can always include
among the f's, any function which sends x,...,x to x.

Assume |A| >= omega_k and f_1,f_2,... have domain A^k-1. Let <
be any linear ordering on A. Now each f_i gives rise to (k-1)^(k-1)
corresponding g:[A]^k-1, where g(x) =
f(x_alpha(1),x_alpha(2),...,x_alpha(k-1)), alpha a function from
{1,...,k-1} into {1,...,k-1}, and where x = {x_1 < ... < x_k-1}. Let
g_1,g_2,... contain all the functions that the f's give rise to in
this manner. By Theorem A, let x_1 < ... < x_k in A, none being any
g_i at the set of the others. Then none are any f_i at any of the
others. Thus we have derived ii and hence ii.

Assume ii. Let f_1,f_2,... have domain [A]^k-1. Let g_1,g_2,... have
domain A^k-1, where g_i(x) = f_i(rng(x)) if |rng(x)| = k-1; g_i(x) a
default value outside all ranges of the f's otherwise.Then we obtain i
in Theorem A. QED

:PROOF OF THEOREM 1

LEMMA. Let k >= 2 and f:_1,f_2,... from [0,1)^k-1 into [0,1). There
exists g:R into R such that the following holds. For all
x_1,...,x_k-1, the g(g(x_1) + ... + g(x_k-1) + m), m >=1, include all
f_n(y), where y is in {x_1,...,x_k-1}^k-1.

Proof: Let k and the f's be as given. Let B containedin [1,1+1/2k] be
a basis for the vector space of R over Q, containing 1. First define g
on [0,1) in any way so that it is one-one and into B\{1}. The sums
g(x_1) + ... + g(x_k-1), x_1,...,x_k-1 lie in [k-1,k), and if two of
these sums, S, are equal then they must come from equal multisets (not
necessarily tuples or sets of terms). Also, any two of these sums, S,
differ by an irrational. These gives us a lot of freedom in extending
g to the sums S+m, m >= 1. Now let such S+m be given. Then it must lie
in [k-1+m,k+m), and so we can decompose S+m into S and m, and we can
then read off the multiset {x_1,...,x_k-1}. We cannot read off the
actual k-1 tuple x_1,...,x_k-1. However, we can use m to code any
given n and order type of a k-1 tuple. This identifies a particular
x_1,...,x_k-1, depending on m but not on S. Then we assign the value
of g(S+m) tp be f_n)(x_1,...,x_k-1) with this particular
x_1,...,x_k-1. QED

LEMMA. (ZC) If k >= 1, |R| >= omega_k, then #[k].

Proof: Using Theorem B, iii implies ii. Use the functions
f_n(x_1,...,x_k-1) = g(g(x_1) + ... + g(x_k-1) + n). QED

LEMMA. (ZC) If k >= 2 and #[k], then |R| >= omega_k.

Proof: Using Theorem B, i implies iii. Assume #[k]. Let f_1,f_2,...
have domain R^k-1. For the purposes of deriving Bi, we assume that the
f's map [0,1)^k-1 into [0,1). Let g be as given by the first Lemma.
Now apply #[k]. then Bi  follows QED

THEOREM 1. ZC proves #[k] iff |R| >= omega_k.

Proof: By the last two Lemmas. 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 699th 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  6/9/16  11::41PM
689: Large Cardinals and Continuations/9  6/11/16  2:51PM
690: Two Brief Sketches  6/13/16  1:18AM
691: Large Cardinals and Continuations/10  6/13/16  9:09PM
692: Large Cardinals and Continuations/11  6/15/16  10:22PM
693: Refuting the Continuum Hypothesis?/5  6/21/16  10:44AM
694: Large Cardinals and Continuations/12  6/29/16  11:46PM
695: Refuting the Continuum Hypothesis?/6  7/16  2:28AM
696: Refuting the Continuum Hypothesis?/7  7/ 5/16  7:41PM
697: Refuting the Continuum Hypothesis?/8  7/6/16  6:40PM
698: Large Cardinals and Continuations/13  7/20/16  1:28AM