[FOM] 763: Large Cardinals and Emulations/42
Harvey Friedman
hmflogic at gmail.com
Mon May 8 02:18:03 EDT 2017
There have been some substantial conceptual/expositional breakthroughs
as I prepare the Putnam volume paper CONCRETE MATHEMATICAL
INCOMPLETENESS: Emulation Theory. .
Given any relational structure whatsoever, in the usual sense in
elementary logic, there exists a corner of Emulation Theory which we
call Basic Emulation Theory/M or BET/M. This has a very precise and
very easy to understand meaning. If the structure M is countable and
comes with a recursive definition, then sharp motivating questions of
algorithmic decidability and incompleteness immediately arise. If the
structure is uncountable with a Borel definition, then we also have
sharp motivating questions of a descriptive set theoretic nature.
We have, only considered BET/M where M is the structure (Q[0,1],<).
This BET/M lends itself very readily to sharp motivating questions of
algorithmic decidability, and above all, incompleteness. Large
cardinals of the SRP hierarchy (stationary Ramsey property)
immediately arise in this BET/M.
BET/M is based on the usual notion of maximal which is maximality
under inclusion. We go somewhat beyond BET by modifying the notion of
maximality first by merely strengthening it, and then by more
substantially modifying it. This leads to incompleteness from HUGE =
hierarchy of huge cardinals, near the very upper end of the large
cardinal hypotheses. We have yet to try to systematize these variants
of Basic Emulation Theory like we have Basic Emulation Theory, but
expect to do so at some point.
In particular, we are now in the process of using basic pieces of the
present form of BET which we describe below, in order to restate our
present way of giving explicitly Pi01 sentences equivalent to
Con(SRP), again driven by using more subtle notions of maximality than
the crude inclusion maximality that drives BET. I hope to report on
this later.
There has also been a conceptual breakthrough in the form of a
FINITENESS CONDITION that is sufficient to be able to use a given
binary relation on Q[0,1]k in BET/M, where M = (Q[0,1],<). This
condition is surprisingly elegant. It is immediately clear that our
Drop Equivalence obeys this Finiteness Condition. The sufficiency of
the Finiteness Condition + Order Preserving is provably equivalent to
Con(SRP) over WKL_0.
1. BET/M.
2. M = (Q[0,1],<).
1. BET/M
Let M be any relational structure (D,...) in the usual sense of model
theory, where D is a nonempty set and ... consists of named constants,
named relations of various finite rarities, and named functions of
various rarities, all in and on and into D. We assume that ... is set
sized.
We use M^k for D^k with the informal view that M is the underlying
space. x,y in M^k are equivalent if and only if they obey the same
unested atomic formulas. I.e., each x_i = x_j iff y_i = y_j, x_i = c
iff y_i = c, R(x_i1,...,x_ik) iff R(y_i1,...,y_ik), F(x_j1,...xj_im) =
xb.
S is an emulation of E containedin M^k if and only if S containedin
M^k and E^2,S^2 have the same elements (2k tuples) up to equivalence.
S is a maximal emulation of E containedin M^k if and only if S is an
emulation of E containedin M^k which is not a proper subset of an
emulation of E containedin M^k.
BET/M is the study of the following Templates with M fixed.
BET/1. Let M be a relational structure and R containedin M^k x M^k.
For subsets of M^k, some emulation contains its image under R.
BET/1 is extremely general, and it is useful to reduce the generality,
as there are uncountably many objects involved even if M is countable.
BET/2. Let M be a relational structure and R contaiendin M^k x M^k be
quantifier free definable. For finite subsets of M^k, some emulation
contains its image under R.
The restriction to finite subsets of M^k has no effect if M has only
finitely many constants, relations, and functions. This is because
then every E containedin M^k has an emulation which is a finite subset
of E.
We want to focus on well behaved structures M. A rich family of well
behaved uncountable structures are those that are definable over the
ordered field of real numbers. For countable structures, a rich family
would be those definable over the structure (Q,Z,<,+). In the latter
case, we have the immediate algorithmic and incompleteness issues.
I.e., is BET/2 algorithmically decidable, and also is every instance
of BET/2 provable or refutable in ZFC? We can also raise these
questions for M 0-definable over the ordered field of real numbers, by
focusing on the quantifier free definable R without parameters.
NOTE: I now like to use emulations, which are merely 2-emulations, so
as to not clutter the statement with another parameter. But when I
state the main results I will mention that we can use r-emulations.
2. M = (Q[0,1],<)
We have been focusing on BET/M with M = (Q[0,1],<), where Q[0,1] = Q
intersect [0,1], where Q is the rationals with its usual ordering. We
have already written extensively about Drop Equivalence. We know also
have the much more general and very simple Finiteness Conditions.
Let R containedin Q[0,1]^k x Q[0,1]^k. The pruning of R is obtained by
taking all (x,y) in R with min(x) = min(y) and removing min(x)
entirely from (x,y). This pruning is now a subset of Q^<=k x Q^<=k.
More generally, we allow R containedin Q[0,]<=k x Q[0,1]^k.
FINITENESS CONDITION. The pruning of R contaienedin Q[0,1]^k x
Q[0,1]^k is a finite set in which 0 does not appear.
The iterated pruning of R containedin Q[0,1]^k x Q[0,1]^k is obtained
by applying pruning over and over again until we no longer get a new
relation. This must take at most k steps.
ITERATED FINITENESS CONDITION. The iterated pruning of R containedin
Q[0,1]^k x Q[0,1]^k is a finite set in which 0 does not appear.
NEW RESULT 1. Every order preserving R containedin Q[0,1] x Q[0,1]
with the finiteness condition is ME usable.
NEW RESULT 2. Every order preserving R containedin Q[0,1] x Q[0,1]
with the iterated finiteness condition is ME usable.
ME usable means "for finite subsets of Q[0,1]^k, some emulation
contains its image under R". Order preserving is the necessary
condition for usability that we have discussed many times: R(x,y)
implies x,y are order equivalent.
************************************************************************
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 763rd 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 3/12/17 12:34AM
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 4/10/17 1:11AM
759: Large Cardinals and Emulations/39 4/10/17 1:11AM
760: Large Cardinals and Emulations/40 4/13/17 11:53PM
761: Large Cardinals and Emulations/41 4/15/17 4:54PM
762: Baby Emulation Theory/Expositional 4/17/17 1:23AM
Harvey Friedman
More information about the FOM
mailing list