UPDATE. The writing is under reasonable control for Embedded Maximal
Squares. The proof that it implies Con(SRP) over WKL_0, or just that
it is independent of ZFC, is too delicate for half measures, and so
the writeup will be at the same level of detail as the BRT book
online.
*********************************
There has been substantial progress in the explicitly Pi01 form of
Embedded Maximal Squares. The one(x) in
http://www.cs.nyu.edu/pipermail/fom/2016-March/019585.html were
heavily quantitative. This new one(s) is qualitative. When stated
qualitatively, it is explicitly Pi-0-3. When bounds are introduced, it
becomes explicitly Pi01.
We only modify section 2 of
http://www.cs.nyu.edu/pipermail/fom/2016-March/019585.html Sections
1,3 remain the same.
2. EMBEDDED FINITELY MAXIMAL SQUARES AND POWERS
Recall for comparison:
EMBEDDED MAXIMAL SQUARES. For all order invariant V containedin Q^k,
some maximal S^2 containedin V|<=n is partially embedded by the
function p if p < 0; p+1 if p = 0,...,n-1.
EMBEDDED MAXIMAL POWERS. For all order invariant V containedin Q^k,
some maximal S^r containedin V|<=n is partially embedded by the
function p if p < 0; p+1 if p = 0,...,n-1.
The new finite forms are:
EMBEDDED FINITELY MAXIMAL SQUARES. For all order invariant V
containedin Q^k, some finitely n-order maximal S^2 containedin V|<=n
is partially embedded by the function p if p < 0; p+1 if p =
0,...,n-1.
EMBEDDED FINITELY MAXIMAL POWERS. For all order invariant V
containedin Q^k, some finitely n-order maximal S^r containedin V|<=n
is partially embedded by the function p if p < 0; p+1 if p =
0,...,n-1.
Here are the two supporting definitions.
DEFINITION 2.1. A,B containedin Q^k are n-order equivalent if and only
if A x {(0,...,n)} and B x {(0,...,n)} have the same elements up to
order equivalence.
DEFINITION 2.2. S^r containedin V|<=n is finitely n-order maximal if
and only if S is finite and every finite S^r containedin S'r
containedin V|<=n is n-order equivalent to S^r.
Note that these statements are explicitly Pi03. Moreover, we can bound
the magnitudes of the numerators and denominators in S and in
Definition 2.2 to put them in explicitly Pi01 form.
THEOREM 2.1. Embedded Finitely Maximal Squares and Embedded Finitely
Maximal Powers are provably equivalent to Con(SRP) over EFA.
We can also use graphs.
A NEW POINT. Various kinds of finitists and formalists may deny that
the above two statements are meaningful. However, if we use specific
numbers for k,n,r, then it becomes much harder to deny that the above
two statements are meaningful. We are expecting to be able to give a
lower bound, as a function of k,n,r, on the size of any proof in ZFC
of Embedded Finitely Maximal powers for k,n,r.
CONJECTURE. Any proof in ZFC of Embedded Finitely Maximal Powers with
k = n = r = 100 has at least 2^1000 bits even if we use any reasonable
sugaring of ZFC.
***********************************************
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 668th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html
600: Removing Deep Pathology 1 8/15/15 10:37PM
601: Finite Emulation Theory 1/perfect? 8/22/15 1:17AM
602: Removing Deep Pathology 2 8/23/15 6:35PM
603: Removing Deep Pathology 3 8/25/15 10:24AM
604: Finite Emulation Theory 2 8/26/15 2:54PM
605: Integer and Real Functions 8/27/15 1:50PM
606: Simple Theory of Types 8/29/15 6:30PM
607: Hindman's Theorem 8/30/15 3:58PM
608: Integer and Real Functions 2 9/1/15 6:40AM
609. Finite Continuation Theory 17 9/315 1:17PM
610: Function Continuation Theory 1 9/4/15 3:40PM
611: Function Emulation/Continuation Theory 2 9/8/15 12:58AM
612: Binary Operation Emulation and Continuation 1 9/7/15 4:35PM
613: Optimal Function Theory 1 9/13/15 11:30AM
614: Adventures in Formalization 1 9/14/15 1:43PM
615: Adventures in Formalization 2 9/14/15 1:44PM
616: Adventures in Formalization 3 9/14/15 1:45PM
617: Removing Connectives 1 9/115/15 7:47AM
618: Adventures in Formalization 4 9/15/15 3:07PM
619: Nonstandardism 1 9/17/15 9:57AM
620: Nonstandardism 2 9/18/15 2:12AM
621: Adventures in Formalization 5 9/18/15 12:54PM
622: Adventures in Formalization 6 9/29/15 3:33AM
623: Optimal Function Theory 2 9/22/15 12:02AM
624: Optimal Function Theory 3 9/22/15 11:18AM
625: Optimal Function Theory 4 9/23/15 10:16PM
626: Optimal Function Theory 5 9/2515 10:26PM
627: Optimal Function Theory 6 9/29/15 2:21AM
628: Optimal Function Theory 7 10/2/15 6:23PM
629: Boolean Algebra/Simplicity 10/3/15 9:41AM
630: Optimal Function Theory 8 10/3/15 6PM
631: Order Theoretic Optimization 1 10/1215 12:16AM
632: Rigorous Formalization of Mathematics 1 10/13/15 8:12PM
633: Constrained Function Theory 1 10/18/15 1AM
634: Fixed Point Minimization 1 10/20/15 11:47PM
635: Fixed Point Minimization 2 10/21/15 11:52PM
636: Fixed Point Minimization 3 10/22/15 5:49PM
637: Progress in Pi01 Incompleteness 1 10/25/15 8:45PM
638: Rigorous Formalization of Mathematics 2 10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2 10/27/15 10:38PM
640: Progress in Pi01 Incompleteness 3 10/30/15 2:30PM
641: Progress in Pi01 Incompleteness 4 10/31/15 8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1 11/3/15 11:57PM
644: Fixed Point Selectors 1 11/16/15 8:38AM
645: Fixed Point Minimizers #1 11/22/15 7:46PM
646: Philosophy of Incompleteness 1 Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1 11/30/15 6:52PM
648: Necessary Irrelevance 1 12/21/15 4:01AM
649: Necessary Irrelevance 2 12/21/15 8:53PM
650: Necessary Irrelevance 3 12/24/15 2:42AM
651: Pi01 Incompleteness Update 2/2/16 7:58AM
652: Pi01 Incompleteness Update/2 2/7/16 10:06PM
653: Pi01 Incompleteness/SRP,HUGE 2/8/16 3:20PM
654: Theory Inspired by Automated Proving 1 2/11/16 2:55AM
655: Pi01 Incompleteness/SRP,HUGE/2 2/12/16 11:40PM
656: Pi01 Incompleteness/SRP,HUGE/3 2/13/16 1:21PM
657: Definitional Complexity Theory 1 2/15/16 12:39AM
658: Definitional Complexity Theory 2 2/15/16 5:28AM
659: Pi01 Incompleteness/SRP,HUGE/4 2/22/16 4:26PM
660: Pi01 Incompleteness/SRP,HUGE/5 2/22/16 11:57PM
661: Pi01 Incompleteness/SRP,HUGE/6 2/24/16 1:12PM
662: Pi01 Incompleteness/SRP,HUGE/7 2/25/16 1:04AM
663: Pi01 Incompleteness/SRP,HUGE/8 2/25/16 3:59PM
664: Unsolvability in Number Theory 3/1/16 8:04AM
665: Pi01 Incompleteness/SRP,HUGE/9 3/1/16 9:07PM
666: Pi01 Incompleteness/SRP,HUGE/10 13/18/16 10:43AM
667: Pi01 Incompleteness/SRP,HUGE/11 3/24/16 9:56PM
Harvey Friedman