[FOM] 733: Large Cardinals and Emulations/28

[Harvey Friedman]

We now have a better way to get to HUGE than we had previously.

We also now have a more thematic way to give explicitly finite forms.

We combine these two developments to get, for the first time,
satisfactory explicitly Pi01 sentences corresponding to HUGE.

At this point, we are going to streamline the Table of Contents below
to take into account these new developments. Note that we are not
going to change sections 1 and 2. We still have the lead statement
from 2.1, At the moment these new developments look so strong and
unifying that we are temporarily going to remove the existing sections
3-6.

The Lead Statement has been stable for a long time, and is this
implicitly Pi01 statement corresponding to SRP n section 2.1.1

MED. (maximal emulation drop). For subsets of Q[0,1]^k, some maximal
emulation (r-emulation) is drop equivalent from (1,1/2,...,1/k) to
(1/2,...,1/k,1/k).

which is discussed in dimension k = 3 only, in the Introduction.

The new implicitly Pi01 form, corresponding to SRP, in section 2.3 reads

GES/1. (greedy emulation shift). Every finite subset of Q^k has a
greedy emulation (r-emulation) containing its upper shift.

The new implicitly Pi01 form, corresponding to HUGE, in section 2.4 reads

UGES/2. (upper greedy emulation shift). Every finite subset of Q^k has
an up greedy emulation (r-emulation) whose upper bounded elementary
subsets are closed under the upper shift.

One new explicitly finite form, corresponding to SRP, in section 3 reads

FMED/1. (finite maximal emulation drop). For finite subsets of
Q[0,1]^k, some finitely maximal emulation (r-emulation) is drop
equivalent from (1,1/2,...,1/k) to (1/2,...,1/k,1/k).

The other new explicitly finite form, corresponding to SRP, in section 3 reads

FGES/1. (finite greedy emulation shift). For finite subsets of Q^k,
some finitely greedy emulation (r-emulation) contains its upper shift
|<=k.

These two independent ideas - one to make things explicitly finite,
the other to push things up to HUGE - are combined below.

EMULATION THEORY
OUTLINE

1. INTRODUCTION.
2. INFINITE EMULATION.
   2.1.  MAXIMAL EMULATION IN Q[0,1]^k.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020107.html
      2.1.1. TRANSLATION.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020107.html
      2.1.2. EMBEDDING.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020137.html
   2.2. STEP MAXIMAL EMULATION IN Q^k.
http://www.cs.nyu.edu/pipermail/fom/2016-November/020170.html
   2.3. GREEDY EMULATION IN Q^k.
here
   2.4. UP GREEDY EMULATION IN Q^k.
here
3. FINITE EMULATION.
here

1. INTRODUCTION

After informal discussion with metaphors, the Introduction leads with
the implicitly Pi01 statement

MED/1. For finite subsets of Q[0,1]^3, some maximal emulation is drop
equivalent from (1,1/2,1/3) to (1/2,1/3,1/3).

provable in SRP, and elaborates on this, saying in dimension 3, with
r-emulation and other 3-tuples, culminating in a complete
characterization of what finite sets of pairs of 3-tuples can be used.
It is conjectured that the stronger statements in 3 dimensions are
independent of ZFC.

2. INFINITE EMULATION
2.1. MAXIMAL EMULATION IN Q[0,1]^k

The Lead is implicitly Pi01 and reads

MED/?. For For finite subsets of Q[0,1]^3, some maximal emulation is
drop equivalent from (1,1/2,...,1/k) to (1/2,...,1/k,1/k).

which is equivalent to Con(SRP) over WKL_0. This is put in section
2.1.1. Elaborations as in the Introduction are given in section 2.1.1.
These are special cases of translation equivalence for lines and
boxes. Translation equivalence for lines and boxes are addressed in
some generality, but the treatment still falls short of a complete
characterization as we have for drop equivalence. The drop equivalence
can also be viewed as a special case of embeddings, which are treated
in section 2.1.2, with further characterization results. Everything
here corresponds to SRP.

2.2. STEP MAXIMAL EMULATION IN Q^k

Step maximality allows us to move from Q[0,1] to Q and to use all of
the nonnegative integers at once. Also we expect to exploit the
sharper step maximality more than we have to date to obtain some
stronger characterization statements again corresponding to SRP.

2.3. GREEDY EMULATION IN Q^k

DEFINITION 2.3.1. For S containedin Q^k and x a tuple from Q, S|<x =
{y in S: max(y) < max(x)}. fld(S) is the set of all coordinates of
elements of S. The upper shift of x in Q^k is the result of adding 1
to each nonnegative coordinate of x. The upper shift of a subset of
Q^k is the set of the upper shifts of its elements. U. indicates
disjoint union.

DEFINITION 2.3.2. S is a greedy r-emulation of E containedin Q^k if
and only if S is an r-emulation of E containedin Q^k where no S|<x U.
{x} is an r-emulation of E containedin Q[0,1]^k, x in E U fld(S)^k. S
is a greedy emulation of E containedin Q^k if and only if S is a
greedy 2-emulation of E containedin Q^k.

GES/1. (greedy emulation shift). Every finite subset of Q^k has a
greedy emulation (r-emulation) containing its upper shift.

THEOREM 2.3.1. GES/1 is provably equivalent to Con(SRP) over WKL_0.
This is true even for some fixed dimension k.

2.4. UP GREEDY EMULATION IN Q^k.

In up greedy emulation, the focus is on the increasing x in Q^k.

DEFINITION 2.4.1. x in Q^k is increasing if and only if for all 1 <= i
<= k, x_i <= x_i+1. S is an up greedy r-emulation of E containedin Q^k
if and only if S is an r-emulation of E containedin Q^k where no S|<x
U. {x} is an r-emulation of E containedin Q^k, x in E U fld(S)^k
increasing. S is an up greedy emulation of E containedin Q^k if and
only if S is an up greedy 2-emulation of E containedin Q^k.

DEFINITION 2.4.2. Let S containedin Q^k. The elementary subsets of S
are the subsets of S that are quantifier free definable in (Q,<,S),
with parameters allowed.

UGES/1. Every finite subset of Q^k has an up greedy emulation
containing its upper shift.

UGES/2. Every finite subset of Q^k has an up greedy emulation
(r-emulation) whose upper bounded elementary subsets are closed under
the upper shift.

THEOREM 2.4.1. UGES/1 is provably equivalent to Con(SRP) over WKL_0.
UGES/2 is provably equivalent to Con(HUGE) over WKL_0.

3. FINITE EMULATION

Here we use an essentially uniform method of converting all of the
main statements in section 2 to explicitly Pi02 statements. These are
then easily converted to explicitly Pi01 statements using obvious
upper bounds.

The essential idea is to define the E,S minimum elements of Q^k for S
containedin Q^k. There are only finitely many E,S minimum elements.

DEFINITION 3.1. Let E,S containedin Q^k be finite.y is E,S-minimal if
and only if y in (S x Q^k\S x E)^k and there is no such z <lex y order
equivalent to y. Here for order equivalence, we flatten out to a
(3k)^k tuple from Q via concatenation.

E,S-minimality is finitary as seen by the following.

LEMMA 3.1. For fixed E,S, there are finitely many E,S-minimal y. We
can replace Q^k\S by fld(S)^k\S.

DEFINITION 3.2. S is a finitely maximal r-emulation of finite E
containedin Q[0,1]^k if and only if S is a finite r-emulation of E
where no S U. {x} is an r-emulation of E containedin Q[0,1]^k, x
E,S-minimal. We make the same definition with Q[0,1] replaced by Q.

FMED/1. For finite subsets of Q[0,1]^k, some finitely maximal
emulation (r-emulation) is drop equivalent from (1,1/2,...,1/k) to
(1/2,...,1/k,1/k).

DEFINITION 3.3. S is a finitely greedy r-emulation of finite E
containedin Q^k if and only if S is a finite r-emulation of E where no
S|<x U. {x} is an r-emulation of E containedin Q^k, x E,S-minimal. S
is a finitely greedy emulation of finite E containedin Q^k if and only
if S is a finitely greedy 2-emulation of finite E containedin Q^k.

FGES/1. Every finite subset of Q^k has a finitely greedy emulation
(r-emulation) containing its upper shift |<=k.

DEFINITION 3.4. S is a finitely up greedy r-emulation of finite E
containedin Q^k if and only if S is a finite r-emulation of E where no
S|<x U. {x} is an r-emulation of E containedin Q^k, x E,S-minimal and
increasing. S is a finitely up greedy emulation of finite E
containedin Q^k if and only if S is a finitely up greedy 2-emulation
of finite E containedin Q^k.

FUGES/1. Every finite subset of Q^k has a finitely up greedy emulation
(r-emulation) containing its upper shift |<=k.

FUGES/2. Every finite subset of Q^k has a finitely up greedy emulation
(r-emulation) S where each ush(S)|<=i, i <= k, is an elementary subset
of S with parameter i+(1/2i).

FMED/1, FGES/1, FUGES/1, FUGES/2 are explicitly Pi02 and become
explicitly Pi01 by placing an upper bound. We can use this method for
converting other implicitly Pi01 statements from section 2 to
explicitly Pi01.

THEOREM 3.1. FMED/1, FGES/1, FUGES/1 are provably equivalent to
Con(SRP) over EFA. FUGES/2 is provably equivalent to Con(HUGE) over
EFA.

************************************************************************
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 733rd 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/2316  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

Harvey Friedman