[FOM] 676: Refuting the Continuum Hypothesis?/3

Tue May 10 03:30:04 EDT 2016

Continuation from http://www.cs.nyu.edu/pipermail/fom/2016-May/019800.html

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.

EXISTENTIAL TRUTH. ET. If it is consistent with ZC that a given simple
existential property holds of all f:R into R, then the given simple
existential property holds of all f:R into R.

EXISTENTIAL TRUTH PROGRAM. Show that ET is consistent with ZFC when
stated for existential properties in more and more expressive
languages.

ET quickly leads to a "refutation" of the continuum hypothesis.

DIGRESION. There is another principle that we have been investigating.
See http://www.cs.nyu.edu/pipermail/fom/2016-April/019775.html

BOREL TRANSFER. BT. If a given simple existential property holds of
all Borel f:R into R, then it holds of all projective f:R into R.

BOREL TRANSFER PROGRAM. Show that BT is provable from large cardinals,
when stated for existential properties in more and more expressive
languages.

BT quickly leads to a "proof" of PD.
http://www.cs.nyu.edu/pipermail/fom/2016-April/019775.html

END OF DIGRESSION.

We already know that for extremely simple languages, ET already
refutes the continuum hypothesis.

Specifically, look at this:

$. 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)

We work with $, but there is a notable variant that uses less
characters, and with the same status:

$'. For all f:R into R there exists x,y in R such that x (y) is not f
at any multiple of y (x).

THEOREM. $,$' are provably equivalent to not CH over ZC.

We now focus on the following logical form, which obviously covers $:

*) For all f:R into R there exists x,y in R such that for all n in Z, phi.

We start the ET program with *) using phi from a small language L1.

TERM LIST 1

Let x,y be real variables and n be an integer variable. The following
are terms, for any particular integers a,b,c in Z.

ax+bn+c
ay+bn+c
f(ax+bn+c)
f(ay+bn+c)

LANGUAGE L1

The nonempty finite conjunctions of inequations between terms in Term List 1.

We carry out the ET program for *) with L1.

case 1. ax+bn+c not= a'x+b'n+c', a not= a'. Provable in ZC.

Proof: Choose x to be irrational. QED

case 2. ax+bn+c not= a'x+b'n+c', a = a', c'-c is a multiple of b-b'.
Refutable in ZC.

case 3. ax+bn+c not= a'x+b'n+c', a = a', c'-c is not a multiple of
b-b'. Provable in ZC.

case 4. ax+bn+c not= a'y+b'n+c', not(a = a'  = 0). Provable in ZC.

Proof: By symmetry, assume a not= 0. Set y = 0 and x irrational. QED

case 5. ax+bn+c not= a'y+b'n+c', a = a' = 0, c'-c is a multiple of
b-b'. Refutable in ZC.

case 6. ax+bn+c not= a'y+b'n+c', a = a' = 0, c'-c is not a multiple of
b-b'. Provable in ZC.

case 7. ax+bn+c not= f(a'x+b'n+c'), a',b' not= 0. Refutable in ZC.

LEMMA 1. Let a',b',c' be integers, a',b' nonzero. There exists g:R
into R such that the following holds. For all x in R, there exists n
in Z, such that g(a'x+b'n+c') = x.

Proof: Compute g(x) as follows. Set h(x) to be the n >= 1 for which
b'(2^n)+c' is nearest to x, where we tie break with smaller of the
two. Return (x-(b'(2^h(x))+c'))/a'. Now let x in R. Choose n so large
that h(a'x+b'(2^n)+c') = n. Then g(a'x+b'(2^n)+c') =
(a'x+b'(2^n)+c'-(b'(2^n)+c'))/a' = a'x/a' = x. QED

Proof of case 7: Define f(x) = ag(x)+bn+c, where g is given by Lemma
5. Let x in R, and choose n such that g(a'x+b'n+c') = x. Then
f(a'x+b'n+c') = ax+bn+c. QED

case 8. ax+bn+c not= f(a'x+b'n+c'), a' = 0, a not= 0. Provable in ZC.

case 9.  ax+bn+c not= f(a'x+b'n+c'), a' = 0, a = 0. Refutable in ZC.

case 10. ax+bn+c not= f(a'x+b'n+c'), a' not= 0, b' = 0. Refutable in ZC.

case 11. f(s) not= f(t). Refutable in ZC.

Proof: Set f to be identically 0. QED

case 12. ax+bn+c not= f(a'y+b'n+c'), a not= 0. Provable in ZC.

Proof: Let y = 0. Choose x to not be an integral shift of f at any integer. QED

case 13. ax+bn+c not= f(a'y+b'n+c'), a = 0. Refutable in ZC.

Proof: If a',b' not= 0, see case 7. If a' = 0, see case 9. If a' not=
0, b' = 0, see case 10. QED

THEOREM 2. Every phi with one conjunct is provable or refutable in ZC.

For multiple phi, we need only look at the provable in ZC single phi's
determined above. We organize these as follows.

case 1. ax+bn+c not= a'x+b'n+c', a not= a'. Provable in ZC.

case 3. ax+bn+c not= a'x+b'n+c', a = a', c'-c is not a multiple of
b-b'. Provable in ZC.

case 4. ax+bn+c not= a'y+b'n+c', not(a = a'  = 0). Provable in ZC.

case 6. ax+bn+c not= a'y+b'n+c', a = a' = 0, c'-c is not a multiple of
b-b'. Provable in ZC.

case 8. ax+bn+c not= f(a'x+b'n+c'), a' = 0, a not= 0. Provable in ZC.

case 12. ax+bn+c not= f(a'y+b'n+c'), a not= 0. Provable in ZC.

case 1'. Replace x by y.

case 3'. Replace x by y.

case 8'. Replace x by y.

case 12'. Switch x and y.

THEOREM 3. The statement " * holds for all phi's not refutable in ZC"
is equivalent to not CH over ZFC.

We have actually established more information, not needed for our
statement of the ET program.

WEAK NORMALITY. Let phi be a formula in any reasonable language whose
free variables are among f,x,y,n. We say that phi is normal if and
only if *) with phi is
1. Refutable in Z and refutable in ATR_0 when restricted to Borel f:R into R; or
2. Provable in Z and provable in ATR_0 when restricted to Borel f:R into R; or
3. Provable in ZC + not CH and provable in ATR_0 when restricted to
Borel f:R into R. And does not imply CH over ZFC.

The ideas here should be pushed through to establish

NORMALITY. Let phi be a formula in any reasonable language whose free
variables are among f,x,y,n. We say that phi is normal if and only if
*) with phi is
1. Refutable in Z and refutable in ATR_0 when restricted to Borel f:R into R; or
2. Provable in Z and provable in ATR_0 when restricted to Borel f:R into R; or
3. Provably equivalent to not CH over ZC and provable in ATR_0 when
restricted to Borel f:R into R.

***********************************************
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 676th 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
674: Refuting the Continuum Hypothesis?/2  May 4 02:36:03 EDT 2016
675: Embedded Maximality and Pi01 Incompleteness/1  5/7/16  12:45AM

Harvey Friedman