[FOM] 667: Pi01 Incompleteness/SRP,HUGE/11

Thu Mar 24 21:55:49 EDT 2016

The writing is, so far, going well on the Lead Proposition, because
after some struggle, I finally have some real control on the
complexities involved in getting together a convincing set of notes.
If I was religious, I would ask you to pray for this.

There is now a stylistic improvement in the Lead Proposition. I got
very strong confirmation that this stylistic change is a very good
idea, from somebody very well known that I trust very much. So I am
going with this change in the Lead Proposition.

Also, there was an annoying typo in the Lead Finite Proposition, which
I correct here. I also make some stylistic changes in the Lead Finite
Proposition as well.

In addition, I also give the almost immediately equivalent
formulations in terms of graphs. I have found that for people who
don't like graphs, the version without graphs is far better. And for
people who do like graphs, the version with graphs ranges from being
somewhat better to far better. So I can accommodate this cultural
divide rather easily.

By the way, my ambition of getting the numerical parameters k,n to be
small is premature. This will come later, and will involve
considerable extra work to get to optimality.

1. EMBEDDED MAXIMAL SQUARES, POWERS, CLIQUES

EMBEDDED MAXIMAL SQUARES. For all order invariant V containedin Q^k,
some maximal S^2 containedin V is partially embedded by the function p
if p < 0; p+1 if p = 0,1,... .

EMBEDDED MAXIMAL POWERS. For all order invariant V containedin Q^k,
some maximal S^r containedin V is partially embedded by the function p
if p < 0; p+1 if p = 0,1,... .

EMBEDDED MAXIMAL CLIQUES. For all order invariant graphs on Q^k, some
maximal clique is partially embedded by the function p if p < 0; p+1
if p = 0,1,... .

THEOREM 1.1. Embedded Maximal Squares, Powers, and Cliques are
provable in WKL_0 + Con(SRP).

We do not know if they are provable in ZFC.

LIMITED 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.

LIMITED 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.

LIMITED EMBEDDED MAXIMAL CLIQUES. For all order invariant graphs G on
Q^k, some maximal clique in G|<=n is partially embedded by the
function p if p < 0; p+1 if p = 0,...,n-1.

Here |<=n limits the tuples to those whose maximum coordinate is <= n.
The above three are implicitly Pi01 via Goedel's Completeness Theorem.

THEOREM 1.2. Limited Embedded Maximal Squares, Powers, and Cliques are
provably equivalent to Con(SRP) over WKL_0.

When I am ready to look at specific numbers k,n, I expect the first
result to be with n = 2 and k arbitrary:

COMING SOON. For all order invariant V containedin Q^k, some maximal
S^2 containedin V|<=2 is partially embedded by the function p if p <
0; p+1 if p = 0,1.

Much harder will be to get control of k.

HOPEFULLY COMING EVENTUALLY. For all order invariant V containedin
Q^6, some maximal S^2 containedin V|<=2 is partially embedded by the
function p if p < 0; p+1 if p = 0,1.

2. LIMITED EMBEDDED k-MAXIMAL SQUARES AND CLIQUES

DEFINITION 1. The height of a rational number is the maximum of the
magnitudes of the numerator and denominator in its reduced form
(standard). The height of a tuple of rationals is the maximum of the
heights of its coordinates.

DEFINITION 2. Let V containedin Q^k. S^2 containedin V is k-maximal if
and only if
i. There is no x of height at most k with (S disjointunion {x})^2 containedin V.
ii. All elements of S have height at most (8k)!.

LIMITED EMBEDDED k-MAXIMAL SQUARES. For all order invariant V
containedin Q^k, some k-maximal S^2 containedin V|<=k extends to a
(8k)!-maximal S'^2 containedin V|<=k that is partially embedded by the
function p if p < 0, p+1 if p = 0,...,k-1.

LIMITED EMBEDDED k-MAXIMAL CLIQUES. For all order invariant graphs G
on Q^k, some k-maximal clique in G|<=k extends to a (8k)!-maximal
clique in G|<=k that is partially embedded by the function p if p < 0,
p+1 if p = 0,...,k-1.

These are obviously explicitly Pi01. They should be viewed as more or
less obvious finite approximate forms of Limited Embedded Squares and
Cliques.

THEOREM 2.1. Limited Embedded k-Maximal Squares and Cliques are
provably equivalent to Con(SRP) over EFA.

3. FIXED POINT MINIMIZERS

>From before, we have

LEAD HUGE PROPOSITION. Every reflexive order invariant R containedin
Q^2k has a <= fixed point minimizer f:A^k into A^k with comparable
nontrivial partial embeddings f_n...n||<n-1.

LEAD FINITE HUGE PROPOSITION. Every reflexive order invariant R
containedin N^2k has a <= fixed point minimizer f sending [n]!^k to
some A^k containedin dom(f), with comparable nontrivial partial
embeddings f_j!...j!||<(j-1)!, 8k < j <= n. We can require that f live
below (8kn)!.

The first is implicitly Pi01 via the Goedel Completeness Theorem. The
second is explicitly Pi01.

These are provably equivalent to Con(HUGE) over WKL_0 and EFA, respectively.

Here ||<n-1 restricts only the domain of functions to coordinates
<n-1. We always use |<n-1 for restricting every element to coordinates
<n-1.

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 667th 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

Harvey Friedman