[FOM] 793: Emulation Theory/Inductive Equations/3
Harvey Friedman
hmflogic at gmail.com
Tue Feb 27 00:11:46 EST 2018
There has been a likely-true important improvement for the infinite
statement equivalent to Con(HUGE).
We have been using the well founded relation on x,y in Q^k,
max(x) < max(y)
which we now write as
x <m y
When we go up to HUGE, there are some huge (pun) advantages in using
the well founded relation on x,y in Q^k,
x <c y if and only if for all 1 <= i <= k, x_i < y_i.
Right now, I am in the middle of writing down the details of the reversal of
INDUCTIVE UPPER SHIFT/m. IUS/m. Every order invariant R containedin Q^2k
has some S = S#\R<m[S] containing ush(S).
from
[1] Concrete Mathematical Incompleteness Status 2/8/18
http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#98
Here R<m[S] = {y: there exists x in S with x <m y and x R y}.
We expect to obtain the same equivalence with Con(SRP) over WKL_0 for
INDUCTIVE UPPER SHIFT/c. IUS/c. Every order invariant R containedin Q^2k
has some S = S#\R<c[S] containing ush(S).
So far, nothing new. BUT we have the INTERNAL INDUCTIVE UPPER SHIFT/m
in [1] that uses =_<= instead of =.
But we can keep = and avoid this =_<= if we move to
INTERNAL INDUCTIVE UPPER SHIFT/c. IIUS/c. Every order invariant R
containedin Q^2k has some S = S#\R<c[S] strongly containing ush(S).
To support this, we do have to modify the notion of "strongly containing".
DEFINITION. Let A,B containedin Q^k. A strongly contains B if and only
if A contains B, and every upper bounded section of B obtained by
fixing at least two arguments is an upper bounded section of A
obtained by fixing at least two arguments.
CAUTION. I claim that IIUS/c is provable in WKL_0 + Con(HUGE) and is
provable equivalent to a Pi01 sentence over WKL_0. I am not ready at
this time to claim the reversal, but this looks very promising.
Note that in the Definition above, the arguments may not be in the
same positions. A stronger variant is to require that they be in the
same positions. This is still provable in WKL_0 + Con(HUGE). Also,
IIUS/c is refutable if in the Definition, we replace "two" throughout
by "one".
BACK TO BACK COMPARISON
To reinforce my main point, look at these, back to back:
INDUCTIVE UPPER SHIFT/c. IUS/c. Every order invariant R containedin
Q^2k has some S = S#\R<c[S] containing ush(S).
INTERNAL INDUCTIVE UPPER SHIFT/c. IIUS/c. Every order invariant R
containedin Q^2k has some S = S#\R<c[S] strongly containing ush(S).
We jump from SRP to HUGE! (see Caution above).
SIMPLIIFED TEMPLATES
TEMPLATE A. Let alpha_1,...,alpha_n,beta_1,...,beta_n be formal
Boolean combinations of S,S#,R<c[S],ush(S). For all order invariant R
containedin Q^2k there exists S containedin Q^k such that each alpha_i
strongly contains beta_i.
More ambitious is
TEMPLATE B. Let alpha,beta,gamma_1,...,gamma_n,delta_1,...,delta_n be
formal Boolean combinations of S,S#,R<m[S],R<c[S],R[S],ush(S). For all
order invariant R containedin Q^2k there exists S containedin Q^k such
that alpha = beta, and each gamma_i strongly contains delta_i.
Note that there are only finitely many statements involved here for
fixed n, when we quantify over k.
CONJECTURE. Every instance of Template B is provable in WKL_0 +
Con(HUGE) or refutable in RCA_0.
A relevant question is: how big does n need to be in Template A in
order to get SRP, or get HUGE? n = 1 is enuf for SRP and n = 3 is enuf
for HUGE, although n = 2 is plausible for HUGE.
Partial results can be expected along the way that limit the
complexity of the finitely many formal Boolean combinations covered -
in various ways.
DARE to expand such Templates to allow for multiple R's. And then more
complex constructs than these upper images - maybe Boolean
combinations and iterates of such. We still can be dealing with
finitely many statements.
************************************************************************
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 793rd 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-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
711: Large Cardinals and Continuations/21 9/18/16 10:42AM
712: PA Incompleteness/1 9/23/16 1:20AM
713: Foundations of Geometry/1 9/24/16 2:09PM
714: Foundations of Geometry/2 9/25/16 10:26PM
715: Foundations of Geometry/3 9/27/16 1:08AM
716: Foundations of Geometry/4 9/27/16 10:25PM
717: Foundations of Geometry/5 9/30/16 12:16AM
718: Foundations of Geometry/6 101/16 12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7 10/2/16 1:59PM
721: Large Cardinals and Emulations//23 10/4/16 2:35AM
722: Large Cardinals and Emulations/24 10/616 1:59AM
723: Philosophical Geometry/8 10/816 1:47AM
724: Philosophical Geometry/9 10/10/16 9:36AM
725: Philosophical Geometry/10 10/14/16 10:16PM
726: Philosophical Geometry/11 Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25 10/20/16 1:37PM
728: Philosophical Geometry/12 10/24/16 3:35PM
729: Consistency of Mathematics/1 10/25/16 1:25PM
730: Consistency of Mathematics/2 11/17/16 9:50PM
731: Large Cardinals and Emulations/26 11/21/16 5:40PM
732: Large Cardinals and Emulations/27 11/28/16 1:31AM
733: Large Cardinals and Emulations/28 12/6/16 1AM
734: Large Cardinals and Emulations/29 12/8/16 2:53PM
735: Philosophical Geometry/13 12/19/16 4:24PM
736: Philosophical Geometry/14 12/20/16 12:43PM
737: Philosophical Geometry/15 12/22/16 3:24PM
738: Philosophical Geometry/16 12/27/16 6:54PM
739: Philosophical Geometry/17 1/2/17 11:50PM
740: Philosophy of Incompleteness/2 1/7/16 8:33AM
741: Philosophy of Incompleteness/3 1/7/16 1:18PM
742: Philosophy of Incompleteness/4 1/8/16 3:45AM
743: Philosophy of Incompleteness/5 1/9/16 2:32PM
744: Philosophy of Incompleteness/6 1/10/16 1/10/16 12:15AM
745: Philosophy of Incompleteness/7 1/11/16 12:40AM
746: Philosophy of Incompleteness/8 1/12/17 3:54PM
747: PA Incompleteness/2 2/3/17 12:07PM
748: Large Cardinals and Emulations/30 2/15/17 2:19AM
749: Large Cardinals and Emulations/31 2/15/17 2:19AM
750: Large Cardinals and Emulations/32 2/15/17 2:20AM
751: Large Cardinals and Emulations/33 2/17/17 12:52AM
752: Emulation Theory for Pure Math/1 3/14/17 12:57AM
753: Emulation Theory for Math Logic 3/10/17 2:17AM
754: Large Cardinals and Emulations/34 3/12/17 12:34AM
755: Large Cardinals and Emulations/35 3/12/17 12:33AM
756: Large Cardinals and Emulations/36 3/24/17 8:03AM
757: Large Cardinals and Emulations/37 3/27/17 2:39AM
758: Large Cardinals and Emulations/38 4/10/17 1:11AM
759: Large Cardinals and Emulations/39 4/10/17 1:11AM
760: Large Cardinals and Emulations/40 4/13/17 11:53PM
761: Large Cardinals and Emulations/41 4/15/17 4:54PM
762: Baby Emulation Theory/Expositional 4/17/17 1:23AM
763: Large Cardinals and Emulations/42 5/817 2:18AM
764: Large Cardinals and Emulations/43 5/11/17 12:26AM
765: Large Cardinals and Emulations/44 5/14/17 6:03PM
766: Large Cardinals and Emulations/45 7/2/17 1:22PM
767: Impossible Counting 1 9/2/17 8:28AM
768: Theory Completions 9/4/17 9:13PM
769: Complexity of Integers 1 9/7/17 12:30AM
770: Algorithmic Unsolvability 1 10/13/17 1:55PM
771: Algorithmic Unsolvability 2 10/18/17 10/15/17 10:14PM
772: Algorithmic Unsolvability 3 Oct 19 02:41:32 EDT 2017
773: Goedel's Second: Proofs/1 Dec 18 20:31:25 EST 2017
774: Goedel's Second: Proofs/2 Dec 18 20:36:04 EST 2017
775: Goedel's Second: Proofs/3 Dec 19 00:48:45 EST 2017
776: Logically Natural Examples 1 12/21 01:00:40 EST 2017
777: Goedel's Second: Proofs/4 12/28/17 8:02PM
778: Goedel's Second: Proofs/5 12/30/17 2:40AM
779: End of Year Claims 12/31/17 8:03PM
780: One Dimensional Incompleteness/1 1/4/18 1:14AM
781: One Dimensional Incompleteness/2 1/6/18 11:25PM
782: Revolutionary Possibilities/1 1/12/18 11:26AM
783: Revolutionary Possibilities/2 1/20/18 9:43PM
784: Revolutionary Possibilities/3 1/21/18 2:59PM
785: Revolutionary Possibilities/4 1/22/18 12:38AM
786: Revolutionary Possibilities/5 1/24/18 12:15AM
787: Revolutionary Possibilities/6 1/25/18 4:09AM
788: Revolutionary Possibilities/7 2/1/18 2:18AM
789: Revolutionary Possibilities/8 2/1/18 9:02AM
790: Revolutionary Possibilities/9 2/2/18 3:07AM
791: Emulation Theory/Inductive Equations/1 2/8/18 11:52PM
792: Emulation Theory/Inductive Equations/2 Feb 25 12:58:25 EST 2018
Harvey Friedman
More information about the FOM
mailing list