[FOM] 818: Beyond Perfectly Natural/17

Wed Jun 13 16:16:20 EDT 2018

Here we present the Finite Solitaire Games associated with Inductive
Equation Theory, including Finite Solitaire Games associated with
HUGE.

At present, our best explicitly finite statements equivalent to
Con(HUGE) are these Games in section 2 below.

1. Finite Games Associated with SRP.
2. Finite Games Associated with HUGE.

1. FINITE GAMES ASSOCIATED WITH SRP

We have already seen the Finite Solitaire Games associated with
Emulation Theory, which correspond to SRP:

[1] https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
  #106

First let's review the lead statement in Inductive Equation Theory from

[2] https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
   #105 First Link (main link)

INDUCTIVE UPPER SHIFT. IUS. For all order invariant R containedin Q^k
x Q^k there exists S = S#\R<[S] containing ush(S).

We now present the Finite Solitaire Game UIG(k,R,x_1,...,x_s).

NOTE: These games are fine tuned for simplicity for the version with
HUGE, and NOT for use in the Confirmation of Consistency of SRP or
HUGE.
NOTE: For Con(SRP), we greatly prefer the Emulation Games in [1].
There is no HUGE involved in our Emulation Games.

Here R is an order invariant subset of Q^k x Q^k and x_1,...,x_s in
Q[-k,k]^k. UIG = upper image game.

The game is initialized by the first row:

x_1 ... x_s

Your job is to create the second row from Q[-k,k]^k, resulting in:

x_1  x_2  x_3  ...  x_s
y_1  y_2  y_3  ...  y_s

according to the following rules and requirements. Recall that for S
containedin Q^k, S#  is the least set V^k containing S U {0,...,0}.

DEFINITION 1.1. x is balanced/+ over z_1,...,z_m, m >= 0, in Q[-k,k]^k
if and only if the following holds. Let p_1 < ... < p_t enumerate (W +
Z/k) intersect [-k,k], where W is the set of all coordinates of the
z_1,...,z_m together with 0. The coordinates of x lying strictly
between two adjacent p's are equally spaced. For S containedin Q^k,
S^<= is the set of all increasing (<=) elements of S.

Here are the rules (1,3) and requirements (2,4) for
UIG(k,R,x_1,...,x_s). Of course, we can implement the game so that 2,4
are verified incrementally, as an inconsequential change. In this
case, we can view 1-4 as all rules.

1. If x_i is in {y_1,...,y_i-1}#<= then y_i is x_i or (max(y_i) <
max(x_i) and y_i R x_i).
2. There is no y_i R y_j with max(y_i) < max(y_j).
3. Each y_i is balanced/+ over y_1,...,y_i-1.
4. If x_i = ush(x_j) then x_i = y_i if and only if x_j = y_j.

WIN UIG. UIG(k,R,x_1,...,x_s), for order invariant R containedin Q^k x
Q^k and x_1,...,x_s in Q[-k,k]^k, is winnable.

WIN UIG is obviously explicitly Pi02. Using the balancing, it is easy
to put WIN UIG in explicitly Pi01 form.

THEOREM 1.1. WIN UIG is equivalent to Con(SRP) over EFA.

2. FINITE GAMES ASSOCIATED WITH HUGE

From

https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
   #105, Second Link Only

we have the state of the art implicitly Pi01 sentence equivalent to
Con(HUGE) over WKL_0. We had to tweak this statement in order to
prepare our associated Finite Solitaire Game. Firstly, we find it more
convenient to restrict to Q^k<= instead of (-k,ininity)^k, as we have
in the games from section 1. Secondly, we need to drastically
specialize the conclusion there about limited 1-sections. We wound up
with a fairly satisfying version that involves some specific limited
sections (not 1-sections).

INTERNAL UPPER IMAGE.GAME.

Firstly, we make a tiny modification in UIG(k,R,x_1,...,x_s).

1-4. Same.
5. If x_i = (0,z) and x_j = (ceiling(z)+(2k+1)/k,z+1), then x_i = y_i
if and only if x_j = y_j.

We call this game IUIG(k,R,x_1,...,x_s). IIUS is read "internal upper
image game".

WIN IUIG. IUIG(k,R,x_1,...,x_s), for order invariant R containedin Q^k
x Q^k and x_1,...,x_s in Q[-k,k]^k, is winnable.

WIN IUIG is obviously explicitly Pi02. Using the balancing, it is easy
to put WIN IUIG in explicitly Pi01 form.

THEOREM 2.1. WIN IUIG is equivalent to Con(HUGE) over EFA.

There are MAJOR OPPORTUNITIES here for Templating, as we can view 1-4
as a Game Framework, where an additional SEMILINEAR RULE is being
added, e.g., 5. Also we know that 5 can be replaced by instances where
ceiling(x_j)+3/2 is replaced by specific rationals. Of course, then we
have to put an inequality on z. The upshot of this is that such
instances of 5 become low level semi linear. There are several other
opportunities for Templating. The idea is that instances of the
Template would go from SRP to HUGE and beyond.

More ambitiously, we can take rues 1-3 as the Game Framework, and try
to Template 4 and 5, perhaps even combined into a single rule. The
plan would be to use a small dimension k, and tweak rule 5, or even
both rules 4,5 into very rudimentary linear inequality conditions, and
get a workable Template that has a chance of being analyzed - the
analysis needing at least HUGE and probably into the highest of all
large large cardinals.

************************************************************************
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 818th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16

Harvey Friedman