[FOM] 755: Large Cardinals and Emulations/35
Harvey Friedman
hmflogic at gmail.com
Sun Mar 12 00:33:52 EST 2017
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.
Large Cardinals and Emulations/34
3.3. EMBED USABILITY.
here
3.4. TRANSLATION USABILITY.
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.3. EMBEDDING
This is an edited, adapted, and corrected version of what is
essentially in http://www.cs.nyu.edu/pipermail/fom/2016-October/020137.html
under Embedding, and with some proof sketches added.
DEFINITION 3.3.1. f_1,...,f_n embeds S containedin Q[0,1]^k if and
only if f_1,...,f_n::Q[0,1] into Q[0,1], and for all p_1,...,p_k in
dom(f_i), (p_1,...,p_k) in S iff (f_i(p_1),...,f_i(p_k)) in S.
(f_1,...,f_n) is ME embed usable if and only if f:_1,...,f_n::Q[0,1]
into Q[0,1], and for subsets of Q[0,1]^k and r >= 1, some maximal
r-emulation is f_1,...,f_n-embedded.
THEOREM 3.3.1. Let f_1,...,f_n::Q[0,1] into Q[0,1]. (f_1,...,f_n) is
ME embed usable if and only if for all k, (f_1<k>,...,f_n<k>) is ME
usable, where f_i<k>(p_1,...,p_k) = (q_1,...,q_k) if and only if each
f_i(p_i) = q_i.
Proof: Obviously S containedin Q[0,1]^k is f_i-embedded if and only if
S is f_i<k>-invariant. QED
THEOREM 3.3.2. Every ME embed usable (f_1,...,f_n) is strictly
increasing and point separating.
Proof: Let (f_1,...,f_n) be ME embed usable. Then (f_1<2>,...,f_n<2>)
is ME usable. By Theorems 3.2.3, 3.2.4, (f_1<2>,...,f_n<2>) is order
respecting and point separating. Suppose 0 <= p < q <= 1 lie in
dom(f). Then f_i<2>(p,q) = (f_i(p),f_i(q)) and (p,q) are order
equivalent, and so f_i(p) < f_i(q). Let u be separating for
(f_1<2>,...,f_n<2>). Then each f_i<2> maps [0,u]^2 into [0,u]^2 and
[u,1]^2 into [u,1]^2. By looking at arguments (p,p), we see that each
f_i maps [0,u] into [0,u] and [u,1] into [u,1]. Hence (f_1,...,f_n) is
point separating. QED
MAXIMAL EMULATION EMBEDDING/1. MEE/1. Let f_1,...,f_n::Q[0,1] into
Q[0,1] be finite, where (f_1,...,f_n) does not alter 0. (f_1,...,f_n)
is ME embed usable if and only if each f_i is strictly increasing.
Proof of MEE/1. This follows immediately from MEU/2 and Theorem 3.3.1. QED
MAXIMAL EMULATION EMBEDDING/2. MEE/2. Finite f::Q[0,1] into Q[0,1] is
ME usable if and only if it is strictly increasing, and
i. There is no 0 < p,q < 1 such that f maps 0 to p and q to 1.
ii. There is no 0 < p,q < 1 such that f maps p to 0 and 1 to q.
We now prove MEE/2 in ACA'.
DEFINITION 3.3.2. f::Q[0,1]^k into Q[0,1]^k is t-balanced if and only
if the following holds.
i. f is strictly increasing.
ii. fld(f) is of the form 0 = p_-t < ... < p_-1 < p_1 < ... < p_t, =
1, t >= 2.
iii. f(0) > 0 and f(1) < 1.
iv. f[{p_-t,...,p_-1] containedin {o_-t,...,p_-1}
v. f[{p_1,...,p_t}] containedin {p_1,...,p_t}.
vi. For all 1 <= i,j <= t, f(p_i) = p_j if and only if f(p_-i) = p_-j.
Note that we do not use the subscript 0.
LEMMA 3.3.3. Let f::Q[0,1] into Q[0,1] be finite, strictly increasing,
f(0) > 0, and f(1) < 1. Then f extends to a t-balanced g::Q[0,1] into
Q[0,1], for some t >= 2.
Proof: Will be in the ms. QED
LEMMA 3.3.4. Every t-balanced f::Q[0,1] into Q]0,1] is embed usable.
Proof: In ACA'. Let f,t be as given, and E containedin Q[0,1]^k, r >=
1. We build a series of maximal emulations of E in the sense of the
Q[-n,n]^k, for positive integers n. This time we start with a maximal
emulation in Q[-1,1]^k. We extend it to a maximal emulation in
Q[-2,2]^k, and so forth. Let n_1 < n_2 ... < n_t be indiscernibles
from Z+ for the resulting maximal emulation S containedin Q^k in the
following sense. Given any two k-tuples from +-{n_1,...,n_t}, whose
absolute values are order equivalent, with the same signs (+,-) in the
same positions, membership in S is equivalent. Now use the maximal
r-emulation S' = S intersect Q[-n_t,n_t]^k and form
(Q[-n_t,n_t],<,S',-n_t,...,-n_1,n_1,...,n_t). Let f' be the unique
isomorph of f with field +-{n_1,...,n_t}. Then clearly S' is
f'-invariant since according to t-balanced, applying f is imply a
matter of adjusting subscripts symmetrically among the negative and
positive subscripts. Now take an isomorphic copy (Q[0,1],<,S,0,...,1),
obtaining a maximal r-emulation of E which is f-invariant. QED
LEMMA 3.3.5. The if part of MEE/2 holds.
Proof: in ACA'. Assume i,ii. By MEE/1, we can assume that f alters
both 0 and 1. By taking the inverse of f if necessary, we can assume
that f(0) > 0. Hence f(1) < 1. Now apply Lemmas 3.3.3 and 3.3.4. QED
LEMMA 3.3.6. Let 0 < p < q < 1 and f(0) = p and f(q) = 1. Then f is
not ME embed usable.
Proof: We show that f is not MOI usable, and therefore not ME usable,
by Theorem 3.2.1. Assume f is MOI usable and k,r = 2. We say that
(a,b),(c,d) in Q[0,1]^2 is bad if and only if
i. a < b and c > d.
ii. a < d and b < c.
Let S containedin Q[0,1]^2 be maximal with no bad (a,b),(c,d) in S.
Since there is no bad (p,1),(c,d), we see see that (p,1) in S. Hence
(0,q) in S. But (0,q),(p,1) is bad, contradicting the choice of S. QED
Proof of MEU/2. In ACA'. By Lemma 3.3.5, it suffices to assume
f::Q[0,1] into Q[0,1] is finite, strictly increasing, and i or ii is
false. By taking inverses, we can assume that i is false.Let 0 < p,q <
1, where f maps 0 to p and q to 1. If p < q then f is not ME usable by
Lemma 3.3.6, If p > q then f is not ME usable by Theorem 3.3.2 (point
separation). p = q is impossible since f is strictly increasing. QED
TO BE CONTINUED
************************************************************************
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 755th 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 3/10/17 2:17AM
754: Large Cardinals and Emulations/34
Harvey Friedman
More information about the FOM
mailing list