[FOM] 587: Finite Continuation Theory 6
Harvey Friedman
hmflogic at gmail.com
Wed Jul 1 23:39:07 EDT 2015
SUMMARY: We improve on
http://www.cs.nyu.edu/pipermail/fom/2015-June/018801.html , still
working with tuples from finite linear orderings. We then turn to
Continuation Theory for finite sets of nonnegative integers, using
ordinary +,<. Using a lot of previous experience, which was not in the
language of Continuations, we are able to do some very simple things.
So it is starting to look like Finite Continuation Theory is working
out best in the setting (N,<,+). The reader can SKIP to section 2
below.
******************************************
I am not happy with the complexity of i combined with adding on the c's, in the
PROPOSITION 1. Every k-system (A,<,R) has a k-continuation (A',<',R')
and c_0 <' ... <' c_n = max(A') such that
i. (Maximality). Every (x,y,c_0,...,c_n), x in R'^k, y in A'k\R', is
order equivalent to some (x',y',c_0,...,c_n), x' in R'^k, (A',<',R'
union {y'}) not k-continuing (A,<,R).
ii. (Symmetry). max(x) <' c_i implies ( (x,c_i,...,c_n-1) is in R' if
and only if (x,c_i+1,...,c_n) is in R'.
from http://www.cs.nyu.edu/pipermail/fom/2015-June/018801.html .
In the paper
[1] https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87
I went to great lengths to avoid towers of finite sets. There is only
one spot where there is a tower of length 2 (in section 7.2 regarding
bases, not maximal roots), and nowhere towers of length >= 3.
However, with the continuation approach, one already has a tower of
length 2 from the very beginning, and so the idea of towers just
becomes the idea of a series of successive continuations, when we
already have one continuation. And then the constants can be read off
as the max's of the continuations.
So we start over again. AND continue (no pun intended) with
Continuation Theory for finite sets of nonnegative integers.
1. FINITE CONTINUATION THEORY - finite linear orderings
DEFINITION 1.1. A k-system is an M = (D,<,R), where (D,<) is a
nonempty finite linear
ordering and R containedin D^k. dom(M) = D and max(M) is the greatest
element of D under <. x resides in M if and only if x is an element of
R. M|<=p is (D|<=p,<|<=p,R|<=p), p in D. M with x is (D,<,R union
{x}).
DEFINITION 1.2. Let (A,<,R) be a k-system. A k-continuation of (A,<,R)
is a k-system (A',<',R') such that
i. A containedin A', < containedin <', R containedin R', max(A) <' max(A')..
ii. Every element of R'^k is order equivalent to some element of R^k.
In successive k-continuations, each triple is k-continued by the next triple.
Note that in ii we are also using order equivalence between k^2-tuples
via concatenation of both length k lists of k-tuples.
PROPOSITION 1.1. Every k-system has successive k-continuations
M_1,...,M_k such that
i. (Maximality). Let i < k. For x in dom(M_i)^k, if M_i+1|<=max(M_i)
with x k-continues M_i, then x resides in M_i.
ii. (Symmetry). Let i <= j < r. For max(x) < max(M_i),
(x,max(M_i),...,max(M_j)) resides in M_r if and only if
(x,max(M_i+1),...,max(M_j+1)) resides in M_r.
NOTE: Full blown maximality is
For x in dom(M_i)^k, if M_i with x k-continues M_i, then x resides in M_i.
We can obviously impose this, but then we cannot impose Symmetry.
An obvious weakening is
For x in dom(M_i)^k, i < k, if M_i+1 with x k-continues M_i, then x
resides in M_i.
which is the weakening of our i where we use M_i+1 instead of
M_i+1|<=max(M_i). Then the statement is provable.
Proposition 1.1 is explicitly Pi02. There is an a priori triple
exponential upper bound on the size of the k-continuation relative to k
and |A|, yielding an explicitly Pi01 form.
THEOREM 1.2. Propositions 1.1 is provably equivalent to Con(SRP) over WKL_0.
2. FINITE CONTINUATION THEORY - N,<,+
DEFINITION 2.1. Let A containedin N be finite. B is a k-continuation
of A if and only if
i. B is a finite subset of N containing A.
ii. Every set of at most k linear inequalities in at most k variables,
in +,<, with coefficients from {0,...,k}, that has a solution in B has
a solution in A.
We now put a largeness condition on k-continuations.
DEFINITION 2.2. Let A,B containedin N be finite, B is a (V,+)-full
k-continuation of A if and only if
i. C is a k-continuation of A.
ii. For t in V union (A+A), if B|<t union {t} is a k-continuation of A
then t is in B.
A|<t = A intersect [0,t).
PROPOSITION 2.1. Let n,m >> k. Every finite A containedin N has k
successive ({1!,...,n!},+)-full k-continuations that exclude m!-1.
Proposition 2.1 is explicitly Pi04, and easily put in explicitly Pi03
form. It is harder to put it in explicitly Pi02 form, but this can be
done replacing >> with a double exponential expression, and another
double exponential expression for where the continuation sits.
THEOREM 2.2. Proposiiton 2.1 is provably equivalent to Con(SMAH) over ACA.
Here SMAH is ZFC with strongly Mathlo cardinals of finite order.
************************************************************
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 587th 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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html
528: More Perfect Pi01 8/16/14 5:19AM
529: Yet more Perfect Pi01 8/18/14 5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01 8/22/14 5:16PM
532: More General Theory/Perfect Pi01 8/23/14 7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14 1:17AM
534: Perfect Explicitly Pi01 8/27/14 10:40AM
535: Updated Perfect Explicitly Pi01 8/30/14 2:39PM
536: Pi01 Progress 9/1/14 11:31AM
537: Pi01/Flat Pics/Testing 9/6/14 12:49AM
538: Progress Pi01 9/6/14 11:31PM
539: Absolute Perfect Naturalness 9/7/14 9:00PM
540: SRM/Comparability 9/8/14 12:03AM
541: Master Templates 9/9/14 12:41AM
542: Templates/LC shadow 9/10/14 12:44AM
543: New Explicitly Pi01 9/10/14 11:17PM
544: Initial Maximality/HUGE 9/12/14 8:07PM
545: Set Theoretic Consistency/SRM/SRP 9/14/14 10:06PM
546: New Pi01/solving CH 9/26/14 12:05AM
547: Conservative Growth - Triples 9/29/14 11:34PM
548: New Explicitly Pi01 10/4/14 8:45PM
549: Conservative Growth - beyond triples 10/6/14 1:31AM
550: Foundational Methodology 1/Maximality 10/17/14 5:43AM
551: Foundational Methodology 2/Maximality 10/19/14 3:06AM
552: Foundational Methodology 3/Maximality 10/21/14 9:59AM
553: Foundational Methodology 4/Maximality 10/21/14 11:57AM
554: Foundational Methodology 5/Maximality 10/26/14 3:17AM
555: Foundational Methodology 6/Maximality 10/29/14 12:32PM
556: Flat Foundations 1 10/29/14 4:07PM
557: New Pi01 10/30/14 2:05PM
558: New Pi01/more 10/31/14 10:01PM
559: Foundational Methodology 7/Maximality 11/214 10:35PM
560: New Pi01/better 11/314 7:45PM
561: New Pi01/HUGE 11/5/14 3:34PM
562: Perfectly Natural Review #1 11/19/14 7:40PM
563: Perfectly Natural Review #2 11/22/14 4:56PM
564: Perfectly Natural Review #3 11/24/14 1:19AM
565: Perfectly Natural Review #4 12/25/14 6:29PM
566: Bridge/Chess/Ultrafinitism 12/25/14 10:46AM
567: Counting Equivalence Classes 1/2/15 10:38AM
568: Counting Equivalence Classes #2 1/5/15 5:06AM
569: Finite Integer Sums and Incompleteness 1/515 8:04PM
570: Philosophy of Incompleteness 1 1/8/15 2:58AM
571: Philosophy of Incompleteness 2 1/8/15 11:30AM
572: Philosophy of Incompleteness 3 1/12/15 6:29PM
573: Philosophy of Incompleteness 4 1/17/15 1:44PM
574: Characterization Theory 1 1/17/15 1:44AM
575: Finite Games and Incompleteness 1/23/15 10:42AM
576: Game Correction/Simplicity Theory 1/27/15 10:39 AM
577: New Pi01 Incompleteness 3/7/15 2:54PM
578: Provably Falsifiable Propositions 3/7/15 2:54PM
579: Impossible Counting 5/26/15 8:58PM
580: Goedel's Second Revisited 5/29/15 5:52 AM
581: Impossible Counting/more 6/2/15 5:55AM
582: Link+Continuation Theory 1 6/21/15 5:38PM
583: Continuation Theory 2 6/23/15 12:01PM
584: Finite Continuation Theory 3 6/26/15 7:51PM
585: Finite Continuation Theory 4 6/29/15 11:23PM
586: Finite Continuation Theory 5 6/20/15 1:32PM
Harvey Friedman
More information about the FOM
mailing list