[FOM] 759: Large Cardinals and Emulations/39
Harvey Friedman
hmflogic at gmail.com
Mon Apr 10 01:11:41 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
http://www.cs.nyu.edu/pipermail/fom/2017-March/020414.html
Large Cardinals and Emulations/38
3.4. TRANSLATION USABILITY.
here
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.4. TRANSLATION USABILITY
DEFINITION 3.4.1. A translation is a function f::Q[0,1]^k into
Q[0,1]^k where f(p)-p is constant.
THEOREM 3.4.1. Two translations are equal if and only if they have the
same domain and range.
Proof: Let f,g be translations with the same domain and range. Then
fog^-1 is a translation from dom(f) onto dom(f). By the boundedness of
Q[0,1], fog^-1 is constant on dom(f). Hence f = g on dom(f) = dom(g).
Hence f = g. QED
In light of Theorem 3.4.1, we think of translation usability of sets.
DEFINITION 3.4.1. A,B are ME translation usable if and only if the
unique translation from A onto B is ME usable.
We only consider very special sets A,B here. A reasonable goal is to
determine which finite A,B are ME translation usable. We have not
achieved this. Of course, the results in sections 3.2, 3.3 for finite
finite functions apply here to give partial results.
DEFINITION 3.4.2. A box in Q[0,1]^k is a Cartesian product of k
rational intervals in Q[0,1]. An initial box is a box where the non
degenerate intervals all contain 0.
Recall that rational intervals in Q[0,1] include emptiest, and
singletons. Also recall that two subsets of Q[0.1]^k are order
equivalent if and only if they have the same elements up to order
equivalence of k-tuples.
MAXIMAL EMULATION BOX/1. MEB/1. Two infinite initial boxes in Q[0,1]^k
are translation usable if and only if the unique translation is order
preserving.
LEMMA 3.4.2. (RCA_0) Let T be the unique translation from infinite
initial box A = I_1 x ... x I_k onto infinite initial box B = J_1 x
... x J_k, and T is order preserving. The two boxes have the same non
degenerate intervals in the same positions. Let f::Q[0,1] into Q[0,1]
be the identity on the union of the non degenerate intervals, and map
each singleton in A onto the corresponding singleton in B. Then f is a
function. Furthermore f is strictly increasing. In addition T maps
coordinstewise according to f.
Proof: Let T,A,B be as given, and let T be addition by (c_1,...,c_k).
Then the corresponding intervals of A,B must be translated by
c_1,...,c_k, respectively. Hence the non degenerate intervals must be
the same in the same positions. Let I* be the union of the non
degenerate intervals. Suppose {x} appears in positions i,j in A. Then
some {y} appears in positions i,j in B because T is order preserving.
So f is univalent at singletons of A that are not in I*. Also if {x}
appears in position i in A and x in I*, then since T is order
preserving, {x} must also appear in position i in B. Hence f is well
defined and is the identity on I*. Now suppose {x} appears in position
i and {y} appears in position j, all in A. Since T is order
preserving, for the {x'} in position i in B and {y'} in position j in
B, we must have x < y iff x' < y'. Hence f is strictly increasing. It
is also clear that T is acting coordinstewise via f. QED
THEOREM 3.4.3. (WKL_0) MEB/1 if and only if Con(SRP).
Proof: We first prove MEB/1 in WKL_0 + Con(SRP). Let A,B containedin
Q[0,1]^k be infinite initial boxes, where the translation T is order
preserving. Let f::Q[0,1] into Q[0,1] be the associated strictly
increasing function. From Lemma 3.4.2, we se that f is a finite
extension of the identity function on some non degenerate interval
containing 0. By MEE/5, f is ME embed usable. Hence T is ME usable.
I.e., A,B are ME translation usable.
Now look at the initial boxes {1/1} x {1/2} x ... x {1/(k-1)} x
Q[0,1/k) and {1/2} x {1/3} x ... x {1/k} x Q[0,1/k). By MEB/1, they
are ME translation usable, and therefore MED/1. Hence Con(SRP), over
RCA_0. QED
DEFINITION 3.4.3. A line segment in Q[0,1]^k is the open line segment
between two distinct endpoints x,y in Q[0,1]^k, in the usual sense,
intersect Q[0,1]^k, with or without the two endpoints.
Note that the boxes {1/1} x {1/2} x ... x {1/(k-1)} x Q[0,1/k) and
{1/2} x {1/3} x ... x {1/k} x Q[0,1/k) are the line segments from
(1/1,...,1/(k-1),0) to (1/2,...,1/(k-1),1/k), and from
(1/2,...,1/k),0) to (1/2,...,1/k,1/k), left closed, right open.
DEFINITION 3.4.4. A spike in Q[0,1]^k is a left closed right open line
segment in Q[0,1]^k whose left endpoint is in the middle of one of the
2k (k-1)-dimensional walls and which is perpendicular to that wall.
MAXIMAL EMULATION LINES/1. MEL/1. Two spikes in Q[0,1]^k in Q[0,1]^k
are ME translation usable if and only if the unique translation is
order preserving.
THEOREM 3.4.4. (WKL_0) MEL/1 if and only if Con(SRP).
Proof: It is not had to see that MEB/1 implies MEL/1 implies MED/1. QED
************************************************************************
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 758th 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
Harvey Friedman
More information about the FOM
mailing list