EMULATION THEORY FOR MATH LOGIC
I make a good start here in developing Emulation Theory for Math
Logic. Already we see that there are some very natural developments
that arise in Emulation Theory for Math Logic that are not nearly as
natural in Emulation Theory for Non Math Logic - and vice versa. We
expect to make further postings on this from time to time. Our main
priority remains Emulation Theory for Non Math Logic = Emulation
Theory.
In Emulation Theory for Non Math Logic, I have taken great pains to
avoid such atrocities as
universal sentences
indiscernibles
strong indiscernibles
If any of these are present in Emulation Theory for Non Math Logic,
Emulation Theory would be dead on arrival. But even so, I could wait
to about the year 2100 to get the point of Emulation Theory across to
Non Math Logic, just from Emulation Theory for Math Logic - something
that would probably happen by 2100 with the pure math community (and
no other community). However, having to wait that long is definitely
undesirable.
For Math Logic, we do not use Emulations. Instead the key notions are:
universal properties and (strong) indiscernibles. But we will be using
the name Emulation Theory for Math Logic. For everybody who isn't a
mathematical logician, we will be using Emulations.
Of course, this will be confusing for mathematical logicians. But the
alternative will prove more confusing given the aims of Emulation
Theory.
DEFINITION 1. Q[0,1] consists of the rationals in [0,1]. A universal
condition phi in subsets of Q[0,1]^k is a condition (sentence) of the
form (forall x_1,...,x_n in S)(psi), where psi is a quantifier free
formula in <,= and the distinct kn variables x_1,...,x_n. Here each
x_i consists of k variables, and no parameters are allowed in psi. A
realization of phi is an S containedin Q[0,1]^k which obeys S. A
maximal realization of phi is a realization of phi which is not a
proper subset of a realization of phi.
THEOREM 1. Every universal condition in subsets of Q[0,1]^k has a
maximal realization. In fact, a low level computable maximal
realization.
Proof: As expected, enumerate the elements of Q[0,1]^k without
repetition, and process them in order, throwing them into the subset
of Q[0,1]^k being created according to whether they can be added while
remaining a realization of phi. This greedy algorithm obviously
creates a low level computable maximal realization of phi. QED
DEFINITION 2. p_1,...,p_n are indiscernibles for S containedin
Q[0,1]^k if and only if p_1,...,p_n in Q[0,1], and if we apply the
predicate S to k numbers from p_1,...,p_n, repetitions allowed, and
also a second time to k numbers from p_1,...,p_n, repetitions allowed,
both in the same numerical order (not necessarily the same numerical
order of subscripts), then we get the same truth value.
THEOREM 2 (Ramsey). For all k,n, every S containedin Q[0,1]^k has some
indiscernibles p_1,...,p_n.
Proof: Frank Ramsey, 1930. QED
THEOREM 3. (Ramsey). For all k,n and universal conditions in subsets
of Q[0,1]^k, some maximal realization has indiscernibles 1/2,...,1/n.
Proof: Immediate from Theorems 1,2. QED
THEOREM 4. (Not Just Ramsey). For all k,n and universal conditions in
subsets of Q[0,1]^k, some maximal realization has indiscernibles
1,1/2,...,1/n.
Proof: As was done with Emulation Theory for Non Math Logic. In ACA'
=my notation for just beyond ACA_0, based on "for all n the n-th
Turing jump of emptyset exists". The presence of the indiscernible 1
makes this not just Ramsey. QED
THEOREM 5. For universal conditions in subsets of Q[0,1]^k, some
maximal realization has indiscernibles 0,1.
Proof: The only issue is that (0,...,0) in S iff (1,...,1) in S.
Suppose that {(0,...,0),(1,...,1)} is a realization. Then we can build
the maximal realization starting with {(0,...,0),(1,...,1)}.
Now suppose that {(0,...,0),(1,...,1)} is not a realization. If
{(0,...,0)} is not a realization then any maximal realization has
indiscernibles 0,1. Suppose {(0,...,0)} is a realization. Then we can
build the maximal realization starting with {(1/2,...,1/2)}, and
(0,...,0),(1,...,1) will be missing. QED
THEOREM 6. The following is false. For universal conditions in subsets
of Q[0,1]^2, some maximal realization has indiscernibles 0,1/2,1.
Proof: (p,q),(r,r) in Q[0,1]^2 is bad if and only if p < q < r. Let S
be a maximal subset of Q[0,1]^2 with no bad (p,q),(r,r) in S, where
also S has indiscernibles 0,1/2,1. Note that there is no bad
(0,1),(r,r), (r,r) in Q[0,1]^2. Hence (0,1) in S. Hence (0,1/2) in S.
Also there is no bad (p,q),(0,0), (p,q) in Q[0,1]^2. Hence (0,0) in S.
Therefore (1,1) in S and (0,1/2),(1,1) is bad. This is a
contradiction. QED
THEOREM 7. Let p_1,...,p_n in Q[0,1]. The following are equivalent.
i. For universal conditions in subsets of any Q[0,1]^k, some maximal
realization has indiscernibles p_1,...,p_n.
ii. 0,1 are not both among the p's, or all p's are among 0,1.
Proof: Immediate from Theorems 4,5,6. This is proved in ACA'. QED
DEFINITION 3. p_1,...,p_n are strong indiscernibles for S containedin
Q[0,1]^k if and only if p_1,...,p_n in Q[0,1], and if I apply the
predicate S to <= k numbers from p_1,...,p_n, repetitions allowed,
occupying some or all of the k positions, and also a second time,
repetitions allowed, occupying the same positions, both in the same
numerical order (not necessarily the same numerical order of
subscripts), and I also fill in the remaining positions for both using
the same numbers from Q[0,1] in the same positions, all of which are
less than all of the p's used for both, then I get the same truth
value.
This strong indiscernibles notion is very familiar from higher set
theory in the context of ordinals. As is well known, in the context of
a suitable large cardinal, for any S, we can always find such strong
indiscernibles. This is definitely not the case for any countably
infinite linearly ordered set such as Q[0,1].
PROPOSITION A. For universal conditions in subsets of any Q[0,1]^k,
some maximal realization has strong indiscernibles 1,1/2,...,1/k.
PROPOSITION B. Let p_1,...,p_n in Q[0,1]. The following are equivalent.
i. For universal conditions in subsets of any Q[0,1]^k, some maximal
realization has strong indiscernibles p_1,...,p_n.
ii. 0,1 are not both among the p's, or all p's are among 0,1.
Propositions A,B, and also Theorem 7 are implicitly Pi01 by Goedel's
Completeness Theorem.
THEOREM 8. Propositions A,B is provably equivalent to Con(SRP) over WKL_0.
Proof: This is proved as in Emulation Theory for Non Math Logic. QED
As in Emulation Theory for Non Math Logic, i implies ii is provable in
RCA_0. In fact, i implies ii in Proposition B because i implies ii in
Theorem 7.
We now remind the reader what Proposition A looks like for everybody
outside Mathematical Logic.
EVERYBODY ELSE'S PROPOSITION A MED. For subsets of Q[0,1]^k, some
maximal emulation is drop equivalent at (1,1/2,...,1/k),
(1/2,...,1/k,1/k).
Actually, Proposition A is quite a bit sharper than MED (read maximal
emulation drop). The proof of the reversal in Theorem 8 for MED is
considerably more difficult. I have to work harder for Non Math Logic.
************************************************************************
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 753rd 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
Harvey Friedman