[FOM] 754: Large Cardinals and Emulations/34

[Harvey Friedman]

We continue with the organized presentation of Emulation Theory.

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.
here/starting over
      3.3. EMBEDDING.
      3.4. TRANSLATIONS.
4. STEP MAXIMAL EMULATION IN Q^k.
5. SUBMAXIMAL EMULATION IN Q^k
6. GREEDY EMULATION IN Q^k.
7. UP GREEDY EMULATION IN Q^k.
8. FINITE EMULATION.
      8.1. WEAKLY MAXIMAL EMULATION IN Q^[0,1]^k
      8.2. WEAKLY STEP MAXIMAL EMULATION IN Q^k.
      8.3. WEAKLY SUBMAXIMAL EMULATION IN Q^k.
      8.4. WEAKLY GREEDY EMULATION IN Q^k
      8.5. WEAKLY UP GREEDY EMULATION IN Q^k.

NOTE: HUGE cardinals appear in sections 7 and 8.5.

3.2. USABILITY
starting over

We strive to turn Emulation Theory into a deep rich theory which can
only be properly developed by going beyond the usual ZFC axioms for
mathematics. The key first step is to bring in a standard general
notion of invariance.

DEFINITION 3.2.1. f::A into B if and only if f is a function
whose domain is a subset of A and range is a subset of B. f is finite
if and only if dom(f) is finite. S
containedin Q[0,1]^k is f_1,...,f_n-invariant if and only if for all 1
<= i <= n,
i. f_i::Q[0,1]^k into Q[0,1]^k.
ii. For all x in dom(f_i), x in S iff f_i(x) in S.

In Emulation Theory, a main goal is to determine what we call the
"usability" of functions.

DEFINITION 3.2.2. (f_1,...,f_n) is ME usable if and only if there
exists k such that the following holds. For all r >= 1 and subsets of
Q[0,1]^k, some maximal r-emulation is f_1,...,f_n-invariant.

A determination of the ME usable (f_1,...,f_n) or just f is way beyond
anything that we can approach at this point. But we do have a growing
body of partial results.

To begin with, Drop Equivalence and MED/1-3 can easily be put into the
usability framework.

DEFINITION 3.2.3. Let x,y in Q[0,1]^k, x_k = y_k. DROP(x) =
{(x_1,...,x_k-1,z): 0 <= z < x_k-1}. DROP(x,y) is the bijection
f:DROP(x) into DROP(y) given by f((x_1,...,x_k-1,z)) =
(y_1,...,y_k-1,z}.

So here is the utterly straightforward restatement of MED/1-3 into the
usability framework.

MED/1'. DROP((1,1/2,...,1/k),(1/2,...,1/k,1/k)) is ME usable.

MED/2'. Let x,y in Q[0,1]^k. The following are equivalent.
i. DROP(x,y) is ME usable.
ii. x_k = y_k and (x_1,...,x_k-1),(y_1,...,y_k-1) are order equivalent
and (for all 1 <= i <= k) (if x_i < x_k or y_i < y_k, then x_i = y_i).

MED/3'. Let x[1],...,x[n],y[1],...,y[n] in Q[0,1]^k. The
following are equivalent.
i. (DROP(x[1],y[1]),...,DROP(x[n],y[n])) is ME usable.
ii. Each DROP(x[i],y[i]) is ME usable.
iii. Each x[j],y[j] obeys MED/2'ii.

Actually, MED/2, MED/3 are a bit sharper than MED/2', MED/3', as they
state the equivalence for each particular r >= 1. We can also reflect
that added sharpness in the usability approach by introducing
r-usability. However, we will refrain from introducing this extra
parameter. We will, however, comment from time to time about the r
that are actually used.

There is a consequence of ME usability that is more technical, but
easier to use when obtaining non ME usability results.

NOTE: In the Introduction, we will treat order theoretic subsets of
Q^k and also order invariant subsets of Q[0,1]^k. The former are
defined by quantifier free formulas in <,= with constants allowed,
whereas the latter are defined by quantifier free formulas in <,= with
constants not allowed, and we take the extension over Q[0,1]^k.

DEFINITiON 3.2.4. (f_1,...,f_n) is MOI usable if and only if there
exists k such that the following holds. For all r >= 1 and order
invariant V containedin Q[0,1]^kr, some maximal S with S^r containedin
V, is (f_1,...,f_n)-invariant.

MOI is read "maximal order invariant".

THEOREM 3.2.1. If (f_1,...,f_n) is ME usable then (f_1,...,f_n) is MOI usable.

Proof in RCA_0: Let f_1,...,f_n::Q[0,1]^k into Q[0,1]^k and V
containedin Q[0,1]^kr be order invariant. For E^r containedin V, let
alpha(E) be the least order invariant subset of V containing E^r. Let
V' be maximal among the various alpha(E). Let alpha(E) = V'. It now
suffices to prove that every maximal r-emulation S of E is a maximal S
containedin Q[0,1]^k with S^r containedin V.

Let S be a maximal r-emulation of E. Since S^r,E^r have the same
elements up to order equivalence, we have alpha(S) = alpha(E) = V'. In
particular, S^r containedin V.

Let S U {x} containedin Q[0,1]^k have (S U {x})^r containedin V. Now
alpha(S U {x})  contains alpha(S) = V' and so alpha(S U {x}) =
alpha(S) = V' by the maximality of V'. Hence S U {x} is an r-emulation
of E, and so x in S. QED

In one dimension, everything is clear.

LEMMA 3.2.2. Let E,S containedin Q[0,1]. S is a maximal r-emulation of
E if and only if
i. r <= |E| and S = Q[0,1].
ii. r > |E| = |S|.

Proof: If r <= |E| then the r-emulations of E are the sets of
cardinality >= r., and so the unique maximal r-emulation of E is
Q[0,1]. If r > |E| then the r-emulations of E are the sets of
cardinality |E|, and so these are also the maximal r-emulations of E.
QED

MAXIMAL EMULATION USABILITY/1. MEU/1. Let f_1,...,f_n::Q[0,1] into
Q[0,1]. (f_1,...,f_n) is ME usable if and only if for all r >= 0 there
exists r element S containedin Q[0,1] which is f_1,...,f_n-invariant.

Proof: In RCA_0. Suppose (f_1,...,f_n) is ME usable. Let r >= 0. Let
|E| = r. Let S be a maximal (r+1)-emulation of E that is
(f_1,...,f_n)-invariant. By Lemma 3.2.2, |S| = r.
Now suppose for all r >= 0 there exists r element S which is
f_1,...,f_n-invariant. Let r >= 1 and E containedin Q[0,1], |E| = r-1.
By Lemma 3.2.2, let |S| = |E| be f_1,...,f_r-invariant.   and r >= 0.
First assume r <= |E|. Then Q[0,1] is a maximal r-emulation of E that
is f_1,...,f_n-invariant. Now assume r > |E|. Let |S| = |E| be
f_1,...,f_n-invariant. By Lemma 3.2.2, S is a maximal r-emulation of
E. QED

We can naturally ask for a simplification of the necessary and
sufficient condition in MEU/1 if f_1,...,f_n are restricted.

THEOREM 3.2.3. If there are infinitely many points not moved by any of
f_1,...,f_n::Q[0,1] into Q[0,1] then (f_1,...,f_n) is ME usable. If
f_1,...,f_n::Q[0,1] into Q[0,1] are order theoretic then (f_1,...,f_n)
is ME usable.

Proof: In RCA_0. By MEU/1, since every subset of the complement of the
union of the sets of points moved is f_1,...,f_n-invariant. Also order
theoretic f::Q[0,1] into Q[0,1] move at most finitely many points. QED

NOTE: I am looking for a good spot to give a brief account of the
crucially important notions of order invariant and order theoretic
subsets of Q[0,1]^k and Q^k. I am thinking of putting it in the
Introduction, saying there that the notion is clarifying and
represents the most concrete functions under consideration in the
entire manuscript. (Order invariant is the same as 0-definable over
(Q,<), and order theoretic is the same as definable over (Q,<). The
official definitions do not use predicate calculus).

Determining the higher dimensional ME usable f seems far too
difficult. A more reasonable goal is to determine the order theoretic
ME usable f. Determining the finite ME usable f has "almost" been
achieved. Before presenting this, we first give two basic necessary
conditions for ME usability - and in fact for MOI usability. These
will be used later.

DEFINITION 3.2.5.  Let f_1,...,f_n::Q[0,1]^k into Q[0,1]^k.
(f_1,...,f_n) is order respecting if and only if for all x in
dom(f_i), x,f_i(x) are order equivalent. u point separates
(f_1,...,f_n) if and only if 0 < u < 1 is a real number such that each
f_i maps [0,u]^k into [0,u]^k and [u,1]^k into [u,1]^k.  (f_1,...,f_n)
is point separating if and only if some u point separates
(f_1,...,f_n).

THEOREM 3.2.4. Every ME (MOI) usable (f_1,...,f_n) is order respecting.

Proof: In RCA_0. Let f_1,...,f_n::Q[0,1]^k into Q[0,1]^k be MOI usable
and consider x,f_i(x). We use r = 1. Let E = {y in Q[0,1}^k: x,y are
order equivalent}. Then there is exactly one maximal S with S
containedin E, Hence E is f_i-invariant. Therefore x in E iff f_i(x)
in E. Hence f_i(x) in E and x,f_i(x) are order equivalent. QED

THEOREM 3.2.5. In dimension k >= 2, every ME usable (f_1,...,f_k) is
point separating. In dimension 1, f(0) = 1 is ME usable but not point
separating.

Proof In RCA_0: Let (f_1,...,f_n) be ME usable in dimension k >= 2.
Let E = {(0,1/5*),(0,2/5*),(3/5,1*),(4/5,1*)}. The 2-emulations of E
consist of a set of at least two (p,q*), 0 <= p < q < 1, all with the
same p, and a set of at least two  (r,s*), r < s <= 1, all with the
same s, and where every q is less than every r. Therefore the maximal
2-emulations S of E take the following form. S = {(p,q*): p < q < u} U
{(r,s*): u <= r < s} or {(p,q*): p < q < u} U {(r,s*): u < r < s}, for
some 0 < p < r < 1. Let S be a maximal 2-emulation of E which is
f_1,...,f_k-invariant. Then S takes the above form, with real 0 < u <
1. Since each f_i is order respecting, and f_i[S] contianedin S, we
see that u separates each (f_1,...,f_n). QED

We now discuss the finite case.

DEFINITION 3.2.6. (f_1,...,f_n)::Q[0,1]^k into Q[0,1]^k alters p in
Q[0,1] if and only if there is some f_j(p) = q or f_j(q) = p, where p
not= q.

MAXIMAL EMULATION USABILITY/2. MEU/2. Let f_1,...,f_n::Q[0,1]^k into
Q[0,1]^k be finite, where (f_1,...,f_n) does not alter 0. Then
(f_1,...,f_n) is ME usable if and only if it is order respecting.

Proof: In ACA'. Let f_1,...,f_n be as given. Let E containedin
Q[0,1]^k and r >= 1. We find a maximal r-emulation of E that is
(f_1,...,f_n)-invariant. Let A be the set of all nonzero rationals
appearing in f_1,...,f_n. We can assume 1 in A. Let |A| = s << t. We
now build a maximal r-emulation of E in Q[0,t]^k as follows. First
take a maximal r-emulation of E in Q[0,1]^k. Then extend to a maximal
r-emulation of E in Q[0,2]^k. Continue inductively until we obtain a
maximal r-emulation S of E in Q[0,t]^k. Now let 0 < m_1 < ... < m_s <=
t be a set of indiscernibles in {1,...,t} in the sense that membership
in S of k-tuples drawn from the m's depend only on their order type.

We now have a system (Q[0,m_s],S intersect Q[0,m_s]^k,m_1,...,m_s).
Note that the second component is a maximal r-emulation of E in
Q[0,x]^k. Let h be any order preserving bijection from Q[0,m_s] onto
Q[0,1] which maps {m_1,...,m_s} onto A. The image of h on the second
component is a maximal r-emulation S* of E. To see that S* is
f_i-invariant, let x in dom(f_i). We verify that f_i(x) in S* iff x in
S*. Applying h^-1 to this equivalence gives a corresponding equivalent
statement using the indiscernibles m_1,...,m_s, and S. Since f_i(x),x
are order equivalent, the corresponding k-tuples from the m's are
order equivalent. By indiscernibility, this corresponding equivalence
is immediate. QED

By symmetry, we can replace 0 by 1 in MEU/2, obtaining an obviously
equivalent statement.

Note that if (f_1,...,f_n) is finite and does not alter 0,1, then
MEU/2 is a trivial consequence of Ramsey's Theorem applied simply to
any maximal r-emulation in Q[0,1]^k.

We opened this section 3.2 with Drop Equivalence as an infinite
instance of ME Usability. We do not have an appropriate general theory
of infinite ME Usability as we do for finite ME Usability. Instead we
view Drop Equivalence as a special case of ME Embedding and ME
Translation.

************************************************************************
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 754th 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 Everybody
753: Emulation Theory for Math Logic/1  3/10/17  2:17AM

Harvey Friedman