[FOM] 757: Large Cardinals and Emulations/37
Harvey Friedman
hmflogic at gmail.com
Mon Mar 27 02:39:02 EDT 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.
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
continued 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.
3.3. EMBED USABILITY
continued from http://www.cs.nyu.edu/pipermail/fom/2017-March/020394.html
http://www.cs.nyu.edu/pipermail/fom/2017-March/020411.html
We now update our inventory of versions of MEE from 756: Large
Cardinals and Emulations/36. MEE/2 completely handles the finite case,
with MEE/1 handling a lot of the multiple finite case. All of the
seven versions below are implicitly Pi01 via the Goedel Completeness
Theorem.
MAXIMAL EMULATION EMBEDDING/3. MEE/3. A bicontinuous order theoretic
f::Q[0,1] into Q[0,1] is ME embed 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.
MAXIMAL EMULATION EMBEDDING/4. MEE/4. Every strictly increasing
continuous order theoretic f::Q[0,1] into Q[0,1] not altering 0,1 is
ME embed usable.
MAXIMAL EMULATION EMBEDDING/5. MEE/5. An f::Q[0,1] into Q[0,1]
finitely extending the identity on some [0,p) U (q,1] is ME embed
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.
MEE/3,4 are provable in ZC and we expect that they are not provable in
WZC. MEE/3 was proved in ZC in
http://www.cs.nyu.edu/pipermail/fom/2017-March/020411.html MEE/5 is
provably equivalent to Con(SRP) over WKL_0.
Recall dominating (regressive) means p in dom(f) implies f(p) >= p
(f(p) <= p). MEE/3,4 are provable in ZC and likely not in WZC (MEE/3
proved in http://www.cs.nyu.edu/pipermail/fom/2017-March/020411.html).
We will show that MEE/5 is provably equivalent to Con(SRP) over WKL_0.
MAXIMAL EMULATION EMBEDDING6. MEE/6. An order theoretic f::Q[0,1] into
Q[0,1] is ME embed 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 do not know anything about the status of MEE/6 other than that
it immediately implies MEE/5, and therefore implies Con(SRP) over
WKL_0.
We believe that MEE/6 is refutable in RCA_0, and that there are some
natural categories of order theoretic f for which MEE/6 is provably
equivalent to Con(SRP) over WKL_0, in addition to MEE/5. Our ignorance
here is rather astounding.
We now prove MEE/4 in ZC.
LEMMA 3.1.13. (RCA_0) Let f_1,...,f_n::Q[0,1) into Q[0,1) be strictly
increasing, strictly dominating, finite, and defined at 0. There are
respective extensions f_1',...,f_n'::Q[0,1) into Q[0,1) with these
same properties, which are Q[0,1] isomorphic.
Proof: Will appear in the ms. QED
LEMMA 3.3.14. (RCA_0) Let f::Q[0,1] into Q[0,1] be strictly
increasing, finite, and with no fixed points. Then f is uniquely
decomposed into f_1 U. ... U. f_n, from left to right, n >= 0, where
the f's are nonempty and alternate between strictly regressive and
strictly dominating. There are respective extensions f_1',...,f_n' of
f_1,...,f_n, so that f' = f_1' U. ... U. f_n' and f_1',...,f_n' have
these same properties, and where all of the strictly regressive ones
are reverse Q[0,1] isomorphic to all of the strictly dominating ones.
Proof: Will appear in the ms. QED
LEMMA 3.3.15. (RCA_0) Let f::Q[0,1] into Q[0,1] be order theoretic,
strictly increasing, continuous, and not alter 0,1. Then f can be
extended to a strictly increasing continuous function which is Q[0,1]
isomorphic to a function of the form G U. h, where
i. G is the identity on [0,1/(2n+1) U (1/2n,1/(2n-1) U ... U (1/2,1],
n >= 1, h is finite with no fixed points, h = h_1 U. h_2 U. ... U.
h_2n, h's from left to right, alternating between strictly regressive
and strictly dominating, starting with strictly regressive, all of the
strictly regressive ones are reverse Q[0,1] isomorphic to all of the
strictly dominating ones, where all of the endpoints except 0,1 lie in
fld(h).
Proof: Will appear in the ms. QED
REGARDING PROOF OF MEE/3 IN ZC in
http://www.cs.nyu.edu/pipermail/fom/2017-March/020411.html The way we
presented it, we were not clear about the choice of cardinal lambda.
We use there a finite set of first order indiscernibles for
(V(lambda),epsilon), where the indiscernibles are ordinals < lambda,
using the Erdos Rado theorem. This is just fine in ZFC where we take
lambda to be beth_omega. However, this is way more than ZC. To keep it
in ZC we need to replace ordinals with well orderings. As an
approximate step that goes a little bit beyond ZC, we can use
transfinite recursion along an initial well ordering of V(omega +
omega) and still apply Erdos Rado. We can stay within ZC by using the
V(omega + n), n < omega, which are handled adequately within ZC.
LEMMA 3.3.16. (ZC) Let f be as in i of Lemma 3.3.15. Then f is ME embed usable.
Proof: We think of lambda in terms of an initial well ordering of
V(omega + omega) for application of the Erdos Rado theorem. Let f = G
U. h, where G is the identity on [0,1/(2n+1) U (1/2n,1/(2n-1) U ... U
(1/2,1], n >= 1, h is finite with no fixed points, h = h_1 U. h_2 U.
... U. h_2n as in i of Lemma 3.3.15.
Let D = -Q(0,1] U +-({1} x lambda x Q[0,1))) U {1} x Q(0,1) U +-({2} x
lambda x Q[0,1))) U {2} x Q(0,1) U ... U +-({n} x lambda x Q[0,1))) U
Q(0,1]. Here +-({i} x lambda x Q[0,1)) = -({i} x lambda x Q[0,1)) U
({i} x lambda x Q[0,1)), where -({i} x lambda x Q[0,1)) = {-x: x in
{i} x lambda x Q[0,1) and x not= (0,0,0)}, and where the minus sign
remains outside. <D orders D as follows. First this union is from left
to right. -Q[0,1) is ordered with the usual ordering on negative
rationals, and Q(0,1] is by the usual ordering on rationals. {i} x
lambda x Q[0,1) is ordered lexicographically, and -({i} x lambda x
Q[0,1)) is by the reverse after removing -.
As before, we need an associated well ordering <#. We use a recursive
ordering Q[0,1)' of type omega with least element 0. First -Q[0,1) by
Q[0,1)' after removing -. Then Q[0,1) by Q[0,1)'. Finally, the signed
triples. First by the ordinal. Then by the integer. Then by whether
the signed triple is negative or positive (negative before positive).
Then by the rational after removing - (using Q[0,1)'). Finally let
<#^k be the ordering on D^k first by the max of the k coordinates
according to <#, and then lexicographically on the k coordinates
according to <#.
Let E containedin Q[0,1]^k and r >= 1. Let S* containedin D^k be the
greedy maximal r-emulation with respect to <#^k. Then S* is first
order definable over (V(omega+omega,epsilon) with no parameters. Let
kappa_1 < ... < kappa_t be indiscernibles for (V(omega+omega,epsilon),
where |h| = 2tn.
We now want to lift f::Q[0,1] into Q[0,1] to f*::D into D. We lift the
n+1 intervals of dom(G) to the intervals [-1,0), [0,1/(2n+1)) to the
interval [-1,0) in <D, and the interval (1/2,1] to (0,1] in <D. We now
lift the 2tn elements of fld(h). The 2t elements of fld(h_i) are
lifted to (i,-(kappa_t,0)), (i,-(kappa_t-1,0)), ...,
(i,-(kappa_1,0)), (i,(kappa_1,0)), ..., (i,(kappa_t,0)), from left to
right. The n-1 middle intervals in dom(G) are the corresponding open
intervals in <D. The function f is lifted by application.
We claim that our maximal r-emulation of E, S containedin D^k, is
f*-embedded. Here we crucially need the reverse isomorphisms from Lemma 3.3.15i.
Now look at the system (D,<D,S*,f*), Note that <D is a dense linear
ordering with left endpoint -1, right endpoint 1. We let D* be the
elements of D whose ordinal is < kappa_t, together with those whose
ordinal is kappa_t and rational is 0. Let <D* be <D restricted to D*.
Note that <D* is a dense linear ordering with the same endpoints, and
is also the initial segment of <# up through (n,kappa_t,0). Note that
f*::D* into D*. Also by the greedy construction of S*, we see that S*
intersect D*^k containedin D*^k is a maximal r-emulation of E.
We now form (D*,<D*,S* intersect D*^k,f*), pass to a countable
subsystem (D**,<D**,S* intersect D**^k,f*), and pull this back down to
(Q[0,1],<,S,f) as before by any strictly increasing bijection from
(D*,<D*) onto (Q[0,1],<). Then S is a maximal r-emulation of E which
is f-embedded. QED
Proof of MEE/4: In ZC .By Lemmas 3.3.15 and 3.3.16. QED
We now come to MEE/5.
LEMMA 3.3.17. (RCA_0) MEE/5 implies Con(SRP). The forward direction of
MEE/5 holds.
Proof: Assume MEE/5. The functions h_k:Q[0,1] into Q[0,1] are strictly
increasing finite extensions of the identity on [0,1/k) U (1,1]. Hence
MED/1, and so Con(SRP). We have already proved the forward direction
of MEE/5. QED
LEMMA 3.3.18. (RCA_0) Let f::Q[0,1] into Q[0,1] be as in MEE/5. Then f
can be extended to a strictly increasing function which is Q[0,1]
isomorphic or Q[0,1] reverse isomorphic to a function of the form G U.
h, where
i. G is the identity on [0,1/3) and finite h alters 1/2,1.
ii. G is the identity on (0,1/3] U (1/2,1] and finite h alters 1/3,1/2.
iii. f is finite and i,ii of MEE/5 hold.
LEMMA 3.3.19. (WKL_0 + Con(SRP)). Every f of form i,ii in Lemma 3.3.18
is ME embed usable.
Proof: For i, <# starts with the left endpoint of D and goes forward
transfinitely below a suitable large cardinal lambda. <# is according
to ordinal first, then element of Q[0,1) using an enumeration of type
omega. Then the greedy maximal r-emulation S* is definable over
V(lambda,epsilon) without parameters Let |h| = t. Assign to the
elements of fld(h) he first point whose ordinals are respectively the
first t strong indiscernibles < lambda. Cut S* back to the initial
segment of <# using ordinals < kappa_t plus the first point using
ordinal kappa_t.
For ii, <# starts with a copy of (1/2,1], using omega steps, and then
proceeds as in case i above starting with 0 and proceeding
transfinitely. Then argue the same way using the strong
indiscernibles.
For iii, use previous theorem. QED
Proof of MEE/5: In WKL_0 + Con(SRP). By Lemmas 3.3.17-3.3.19. QED
TO BE CONTINUED. We will next look at very special cases of piecewise
translations f::Q[0,1] into Q[0,1].
************************************************************************
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 757th 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
Harvey Friedman
More information about the FOM
mailing list