# [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
#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
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

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
```