[FOM] 674: Refuting the Continuum Hypothesis?/2
Harvey Friedman
hmflogic at gmail.com
Wed May 4 02:36:03 EDT 2016
OPENING STATEMENT: I do not know if CH is matter of fact. I am not
sure what 'matter of fact" means. I am an opportunistic foundational
and philosophical whore. That why I use $. END OF OPENING STATEMENT.
Continuing from
http://www.cs.nyu.edu/pipermail/fom/2016-May/019791.htmlhttp://www.cs.nyu.edu/pipermail/fom/2016-May/019791.html
There we started off with
THEOREM 1. For all Borel f:R into R there exists x,y in R such that x
is not f at any integer shift of x and y is not f at any integer shift
of x.
THEOREM 2. For all Borel f:R into R there exists x,y in R such that x
(y) is not f at any integer shift of y (x).
An alternative is
THEOREM 3. For all Borel f:R into R there exists x,y in R such that x
is not f at any multiple of x and y is not f at any multiple of x.
THEOREM 4. For all Borel f:R into R there exists x,y in R such that x
(y) is not f at any multiple of y (x).
I am using the definition of multiple as given in
https://en.wikipedia.org/wiki/Multiple_(mathematics)
And obviously there are far more general statements of this kind, also
proved by the same measure or category theoretic argument. They take
the form that for all Borel f:R into R there exists x,y in R such that
x is not generated from y and y is not generated from x. But this is
tangential to the issues at hand.
For the sake of definiteness we will stick with the integer shift
formulation, and do not foresee it making any significant difference
which of various myriad formulations we choose.
We then consider the lifting
$. For all f:R into R there exists x,y in R such that x (y) is not f
at any integer shift of y (x)
THEOREM 5. ZC proves that $ is equivalent to the negation of the
continuum hypothesis.
$ takes the form
*) For all f:R into R there exists x,y in R
Before digging into our COHErENCE PROGRAM for *), we want to consider
$(kappa). For all f:R into R there exists a set of reals of
cardinality kappa such that no element is the value of f at any
integer shift of any other element.
So $ = $(2), and $(1) is vacuously true.
THEOREM 6. (ATR_0) $(c) is true for Borel f:R into R. The set of
cardinality c can be taken to be a perfect set of real numbers.
THEOREM 6. ZC proves the following. Assume not CH.
i. If kappa <= c is regular then $(kappa).
ii. If kappa < c then $(kappa).
THEOREM 7. ZC proves that the following are equivalent.
i. $(2).
ii. For all kappa < c, $(kappa).
iii. not CH.
We now come to our main topic. Let's look carefully at these two:
$. For all f:R into R there exists x,y in R such that x (y) is not f
at any integer shift of y (x)
*) For all f:R into R there exists x,y in R such that for all n in Z, phi.
The program consists of
i. Fixing a language for the phi', far more than expressive enuf to
cover $ by admitting phi = "x not= f(y+n) and y not= f(x+n)".
ii. Determining when *) is true for all Borel f:R into R, for phi
chosen from that language.
iii. Determining the set theoretic status of *), for phi chosen from
that language.
iv. Looking to see whether you get any *) that are consistent with ZFC
and imply CH. Hopefully not.
This is already far too much for me to swallow whole yet - not enuf
experience. Here is what I expect. Playing around with this will allow
me to get some reasonably clean theorems that i-iv hold for some
reasonably interesting moderately expressive languages. So in
retrospect, we don't have to look so hard at actual formulas. After
that, we look really hard at actual formulas, and then get more
reasonably clean theorems that i-iv hold for yet more expressive
languages.
FROM THE OTHER SIDE - GETTING CH
refined normal form theory
Also, from the other side, see how restrictive we can make the
language so that we can get CH, probably at first at least, through
getting "all reals are constructible". Recall from
http://www.cs.nyu.edu/pipermail/fom/2016-May/019791.htmlhttp://www.cs.nyu.edu/pipermail/fom/2016-May/019791.html
this normal form, where T is the usual Baire space N^N:
#) (for all f:T into T)(there exists x in T)(for all n in
N)(S(n,x|<=n,f(x)|<=n)),
where S is a ternary recursive predicate of
nonnegative integers, finite sequence numbers, and finite sequence
numbers. In fact, this hold of third order sentences over countable
domains where all third order quantifiers are in front and are
universal.
I'm going to end this posting with an exploration of what kind of phi
we can use in *) in order to get everything in the universal #).
*) For all f:R into R, there exists x,y in R, such that for all n in Z, phi.
I think the first good step is to restate #) in order to remain
universal but get rid of the finite sequence numbers. Put # in the
following equivalent form.
#1) for all f:T into T, there exists x,y,z,w in T, where
i. for all n in N, S(n,y(n),z(n)).
ii. for all n in N, y(0) = x(0), y(n+1) = P(y(n),x(n+1)).
iii. f(x) = z.
iv. for all n in N, w(0) = z(0), w(n+1) = P(w(n),z(n+1)).
v. S(n,y(n),w(n)).
Here P(i,j) = (i+j)^2 + i. And of course addition and multiplication
can be absorbed I think through allowing more f:T into T. Furthermore,
the low level computational S can also be absorbed with more f:T into
T. So I am thinking that we have the following important universal
form:
##) for all f_1,...,f_k:T into T, there exists x_1,...,x_r in T, for
all n_1,...,n_t in N, phi
where phi is a propositional combination of equations in the obvious
compound terms using +1 on the n's. The compounding here is rather
controlled since all of the operations involved are unary. Of course,
we can certainly cut down the terms here considerably at the cost of
increasing the numbers of variables. Also probably we can cut the
number of variables down considerably by using the power of Baire
space and f's. So we are immersed ourselves in what I called in the
previous posting, REFINED NORMAL FORM THEORY.
Next, we want to move from Baire space T = N^N to Cantor space K =
2^N. The idea is to simulate elements of T by elements of K. However,
now it seems like we are going to be drenched in order on the natural
numbers, addition, and perhaps finite sequence coding. We are going to
wind up with a mess of bounded quantifiers at least, and this would be
using the power of the f:K into K. The technical issue is: can the
power of the f:K into K be used cleverly to get rid of a lot of ugly
stuff in the propositional part?
See, normally in recursion theory, we take bounded quantifiers, even a
bunch of alternating ones, for granted as nothing. The main places
where you don't do this is in finite sequence trees like in #), and in
Hilbert's Tenth Problem. In the former case, you also take for granted
primitive recursive predicates (like the S in #). In the latter case,
you have addition and multiplication on integers. So this stuff here
is kind of moving in a different than normal direction.
Now after the move from T to K, we have to move from K to R = reals.
Now that, superficially, with binary expansions, is going to involve
base 2 exponentiation, as in 2^-n. But again, I don't know how
powerfully you can use the f:R into R.
If this comes out well, we would presumably still have a lot of f's
and/or a lot of x's and/or a lot of n's, and it would seem that we
would also be using at least general binary addition. Note that in our
$, we have so much less.
So my general feeling is that universal forms, which take care of all
projective statements, applied to the continuum hypothesis, is
probably going to need something like
*an airplane compared to an inclined plane*
which is such a difference in amount that it can construed as a
difference in kind.
In the next posting, we really do take aim at differences in kind. We
start looking at baby languages for the phi in *), and see what
happens.
***********************************************
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 674th 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?/1 5/1/16 9:38PM
673: Pi01 Incompleteness/SRP,HUGE/16 5/1/16 11:27PM
Harvey Friedman
More information about the FOM
mailing list