[FOM] 760: Large Cardinals and Emulations/40

Thu Apr 13 23:53:34 EDT 2017

NOTE: THIS IS EXPECTED TO CONCLUDE THE PRESENTATION OF THE SCOPE OF
EMULATION THEORY IN THIS PHASE. WE NOW PLAN TO MOVE INTO WRITING MODE
FOR THE REST OF 2017.

We now have a new baby version of the lead statement for the
Introduction and in section 3.1. Presently, the lead statement uses
drop equivalence.

Drop equivalence is tricky enough (of course trivial compared to what
one sees in the first few seconds of a typical math talk) that we
focused on it in the introductory section 2.

But now we have this new expositional tool, namely POINT EQUIVALENCE.
I.e., S contaiendin Q[0,1]^k is equivalent at x,y in Q[0,1]^k if and
only if x in S iff y in S.

So the Baby Lead in 2 dimensions (only 2 dimensions in the Introduction), are

MAXIMAL EMULATION POINT/1. MEP/1. For finite subsets of Q[0,1]^2, some
maximal emulation is equivalent at (1,1/2), (1/2,1/3).

and then the list of pairs statement, which asserts that a finite list
of pairs can be used here if and only if any one can be used. This is
followed by a complete description of what pairs can be used, and
therefore what finite lists of pairs can be used. At this point, then
allude to r-emulations and also dimension k instead of just emulations
(2-emulations) and dimension 2.

Some non obvious ideas are needed to prove MEP/1 and extensions,
particularly because of the endpoint 1. The relatively weak system
ACA' is enough for all of this.

Then we stay in dimension 2 and transition to DROP EQUIVALENCE, for
the Adult Lead:

MAXIMAL EMULATION DROP/1. MED/1. For finite subsets of Q[0,1]^2, some
maximal emulation is drop equivalent at (1,1/2), (1/2,1/2).

and then the list of pairs statement, which asserts that a finite list
of pairs can be used if and only if any one can be used. This is
followed by a complete description of what pairs can be used, and
therefore what finite lists of pairs can be used.  At this point, then
allude to r-emulations and also dimension k instead of just emulations
(2-emulations) and dimension 2.

MED/1 and extensions in dimension 2 use transfinite recursions of
uncountable length, and we believe this is necessary, at least for the
extensions. Probably the analogous development in dimension 3 cannot
be handled in ZFC.

I think that now the Introduction does its job extremely well, which
this introduction of POINT EQUIVALENCE. So I will keep the special
section 2 on Drop Equivalence. The general architecture of Emulation
Theory becomes extremely accessible from the Introduction now, more so
than before.

###########

EMULATION THEORY
Below will organize, as FOM postings, the contents of a ms. to be
placed on my website, and to appear in some form in a planned volume
in honor of Putnam. This ms. will contain proofs other than reversals.
Reversals will appear in a much expanded ms. later as a high priority,
and will form the book CONCRETE MATHEMATICAL INCOMPLETENESS, when
combined with the BOOLEAN RELATION THEORY ms. currently on my website.

1. INTRODUCTION.
http://www.cs.nyu.edu/pipermail/fom/2017-February/020299.html
2. DROP EQUIVALENCE IN LINEAR ORDERINGS.
http://www.cs.nyu.edu/pipermail/fom/2017-February/020300.html
3. MAXIMAL EMULATION IN Q[0,1]^k
http://www.cs.nyu.edu/pipermail/fom/2017-February/020300.html
      3,1, DROP EQUiVALENCE.
http://www.cs.nyu.edu/pipermail/fom/2017-February/020301.html
      3.2. USABILITY.
http://www.cs.nyu.edu/pipermail/fom/2017-March/020393.html
      3.3. EMBED USABILITY.
http://www.cs.nyu.edu/pipermail/fom/2017-March/020394.html
http://www.cs.nyu.edu/pipermail/fom/2017-March/020411.html
http://www.cs.nyu.edu/pipermail/fom/2017-March/020414.html
http://www.cs.nyu.edu/pipermail/fom/2017-April/020434.html
      3.4. TRANSLATION USABILITY.
http://www.cs.nyu.edu/pipermail/fom/2017-April/020435.html
4. STEP AND # MAXIMAL EMULATION IN Q^k.
here
5. GREEDY AND UP GREEDY EMULATION IN Q^k.
here
6. FINITE EMULATION.
here

###########

4. STEP AND # MAXIMAL EMULATION IN Q^k

So far, we have only considered emulations of E containedin Q[0,1]^k.
We now use Q^k.

NOTE: We are going to introduce several new kinds of emulation, two in
this section, and two in sections 5 (and also some in section 6). We
want to have as much in the way of uniform presentations as we can so
that they can be readily compared. We didn't quite set up the
presentation of maximal emulations in Q[0,1]^k in section 3 with this
in mind. So we start with an altered presentation of maximal
emulations in Q[0,1]^k that will be used in the ms.

DEFINITION 3.?. S is an r-emulation of E containedin Q[0,1]^k if and
only if S containedin Q[0,1]^k and S^r,E^r have the same elements
(kr-tuples) up to order equivalence. S is a maximal r-emulation of E
containedin Q[0,1]^k if and only if S is an r-emulation of E
containedin Q[0,1]^k, where there is no r-emulation S U. {x} of E
containedin Q[0,1]^k.

DEFINITION 4.1. We replace Q[0,1]^k throughout with Q^k in Definition
3.?. S is a step maximal r-emulation of E containedin Q^k if and only
if S is an r-emulation of E containedin Q^k, where there is no
r-emulation S|<=n U. {x} containedin Q^k|<=n of E containedin Q^k

Recall the convention that k,n,m,r,s,t range over positive integers
unless stated otherwise.

THEOREM 4.1. Every step maximal r-emulation of E containedin Q^k is a
maximal r-emulation of E contaiendin Q^k. Every subset of Q^k has a
step maximal r-emulation.

Proof: Left to the reader. QED

We now consider the most general kind of drop equivalence. We didn't
put this in section 3.1, but we will in the ms. Instead of dropping
only from the last coordinate, we drop from any nonempty set of
coordinates. Thus we consider pairs of marked tuples, where we mark
the zero or more coordinates that we are dropping from. Of course, we
now drop all the way down to -infinity.

DEFINITION 4.2. Let S containedin Q^k and x,y in Q^k be marked. S is
drop equivalent at x,y just in case if we replace all marked
coordinates of x,y by a single value smaller than all marked
coordinates, resulting in x',y', then x' in S iff y' in S.

STEP MAXIMAL EMULATION/1. SME/1. Let A be a finite set of pairs of
marked elements of Q^k. The following are equivalent.
i. For finite subsets of Q^k, some step maximal r-emulation is drop
equivalent at all pairs from A.
ii. For finite subsets of Q^k and (x,y) in A, some step maximal
r-emulation is drop equivalent at x,y.

In fact, we can give a necessary and sufficient condition for drop equivalence.

DEFINITION 4.3. Two marked k-tuples from Q are related if and only if
i. Their marked coordinates of x are at the same positions as the
marked coordinates of y.
ii. The unmarked coordinates of x and the unmarked coordinates of y
form two order equivalent tuples.
iii. If any given unmarked coordinate less than all marked
coordinates, then p and the corresponding unmarked coordinate is the
same.

STEP MAXIMAL EMULATION//2. SME/2. Let A be a set of pairs of related
marked k-tuples from Q, where the set of all rationals appearing in
these tuples is of order type <= omega. The following are equivalent.
i. For subsets of Q^k, some step maximal r-emulation is drop
equivalent at each pair in A.
ii. The tuples in each pair are similar.

STEP MAXIMAL EMULATION/3. SME/3. For finite subsets of Q^k, some step
maximal r-emulation is embedded by all of the functions f_i(p) = p if
p < i; p+1 if p = i,i+1,i+2,.., i >= 0.

THEOREM 4.2. STEP/1,2,3 are provably equivalent to Con(SRP) over WKL_0.

# maximal emulation is a weaker form of maximal emulation which
supports stronger forms of symmetry.

DEFINITION 4.4. For S contained Q^k, S# is the least set of the form
(A U {0})^k containing S. The upper shift of S containedin Q^k is
obtained by adding 1 to all nonnegative coordinates of elements of S.
The upper shift at p of S containedin Q^k is obtained by adding 1 to
all coordinates of elements of S that are at least p.

DEFINITION 4.5. S is a # maximal r-emulation of E containedin Q^k if
and only if S is an r-emulation of E containedin Q^k, where there is
no r-emulation S U. {x} containedin S# of A containedin Q^k.

# MAXIMAL EMULATION/1. #ME/1. For finite subsets of Q^k, some #
maximal r-emulation contains its upper shift.

THEOREM 4.3. #ME/1 is provably equivalent to Con(SRP) over WKL_0.

# MAXIMAL EMULATION/2. #M#/2. Let f::Q[0,1] into Q[0,1] be order
theoretic. The following are equivalent.
i. For finite subsets of Q^k, some # maximal r-emulation is f-embedded.
ii. f is strictly increasing.

5. GREEDY AND UP GREEDY EMULATION IN Q^k.

Greedy emulations are a stronger form of # maximal emulations.

DEFINITION 5.1. A greedy r-emulation of E containedin Q^k is an
r-emulation S of E contaiendin Q^k, where there is no r-emulation
S|<=p U. {x} containedin S#|<=p of E containedin Q^k, p in Q.

GREEDY EMULATION/1. GE/1. For finite subsets of Q^k, some greedy
r-emulation contains its upper shift.

Reversals are much easier for greedy emulations than they are for any
of the previous kinds of maximal emulations. So we expect GE/1 to be
provably equivalent to Con(SRP) over WKL_0 already for k = 3.

DEFINITION 5.2. Q^k<= = {x in Q^k: x_1 <= ... <= x_k}. An up greedy
r-emulation of E containedin Q^k is an r-emulation S of E contaiendin
Q^k, where there is no r-emulation S|<=p U. {x} containedin S#|<=p of
E containedin Q^k, p in Q, x in Q^k<=.

Thus up greedy r-emulations are greedy r-emulations. There is no
change in the status of the statements corresponding to GE/1,2.

UP GREEDY EMULATION/1. UGE/1. For finite subsets of Q^k, some up
greedy r-emulation contains its upper shift.

THEOREM 5.1. GE/1, UGE/1 are provably equivalent to Con(SRP) over WKL_0.

DEFINITION 5.3. Let S containedin Q^k. The sections of S are the sets
{x in Q^k-i: x_j1 = p_1, ..., x_ji = p_i}, 1 <= i < k, j1,...,ji
distinct. The lower sections of S are the sets {x in Q^k-i: x_j1 =
p_1, ..., x_ji = p_i and max(x) < min(p_1,...,p_i)}, 1 <= i < k,
j1,...,ji distinct.

UP GREEDY EMULATION/2. UGE/2. For finite subsets of Q^k, the elements
and lower sections of some up greedy r-emulation include those of its
upper shift.

THEOREM 5.1. UGE/2 is provably equivalent to Con(HUGE) over WKL_0 .

Proofs of statements like UGE/2 have been given in section 5.4 of
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#86
Also there are arguments there that such statements are implicitly
Pi01 by general arguments.

6. FINITE EMULATION

Normally, every maximal r-emulation of E containedin Q[0,1]^k is
infinite. This tells us that. e.g.,

MAXIMAL EMULATION DROP/1. MED/1. For finite subsets of Q[0,1]^k, some
maximal r-emulation is drop equivalent at (1,1/2,...,1/k),
(1/2,...,1/k,1/k).

is implicitly Pi01 rather than explicitly Pi01. For explicit finite,
we need a statement of the form

FINITE MAXIMAL EMULATION. FME. For finite subsets of Q[0,1]^k, some
weakly maximal r-emulation is drop equivalent at (1,1/2,...,1/k),
(1/2,...,1/k,1/k).

We now define weak maximality. For comparison, we give the following
form of maximality:

S is a maximal r-emulation of E containedin Q[0,1]^k if and only if S
is an r-emulation of E containedin Q[0,1]^k, where every r-emulation S
U {x} of E containedin Q[0,1]^k is S.

DEFINITION 6.1. S is a weakly maximal r-emulation of E containedin
Q[0,1]^k if and only if S is an r-emulation of E containedin Q[0,1]^k,
where every r-emuation S U {x} x E of E^2 contianeidn Q[0,1]^2k is an
r-emulation of S x E containedin Q[0,1]^2k.

FINITE MAXIMAL EMULATION/1. FME/1. For finite subsets of Q[0,1]^k,
some finite weakly maximal r-emulation is drop equivalent at
(1,1/2,...,1/k), (1/2,...,1/k,1/k).

An a priori estimate can be placed on the size of the weakly maximal
r-emulation in terms of k and the size of the given finite subset of
Q[0,1]^k, so that FME/1 becomes explicitly Pi01.

THEOREM 6.1. FME/1 is provably equivalent to Con(SRP) over EFA
(exponential function arithmetic).

At this point, it is not clear just how to give an explicitly Pi01
statement along the lines of FME/1 that is equivalent to Con(HUGE).

************************************************************************
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 760th 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  12 00:34:34 EST 2017
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

Harvey Friedman