[FOM] 669: Pi01 Incompleteness/SRP,HUGE/13

[Harvey Friedman]

The writing of the proof of equivalence of Embedded Maximal Squares,
Embedded Maximal Powers, Embedded Maximal Cliques, with Con(SRP) is
well under control. The structure of the proof will be similar to
those of the big proofs in the BRT book online. Namely, for the
reversal, the derivation of Con(SRP) from these three, there will be
about 12 sections. Each section ends with a Theorem. Each section uses
only the ending Theorem of the previous section. This way, the proof
can be checked modularly. As is usual, as the sections ensue, we
slowly but deliberately morph into a model of SRP. And, as in the BRT
book, the proof of the Lead Propositions from WKL_0 + Con(SRP) is a
reasonable Math Colloquium talk of one hour. Actually one proves the
Lead Proposition in such a talk from SRP+, comments on WKL_0 +
Con(SRP), and blackboxes the large cardinal theory.

It has taken some time to get a good outline of this paper so that the
details do not get totally out of control. It has to be divided up
just right, with just the right technical definitions, and there are a
lot of moving parts. But when all is well and done, assuming that I
don't run into any problems, the paper should come under 100 pages and
be easily completely checked by a small team - or even one person who
is willing to put in more time than is to be expected.

In this posting I want to show just how completely natural both
Embedded Maximal Squares (Powers) and Embedded Finite Maximal Squares
(Powers) are from three points of view:

i. The combinatorial point of view we have been emphasizing.
ii. The automorphism action point of view, inspired from elementary
Galois theory.
iii. The model theoretic point of view, applied to (Q,<).

In this posting, I will not touch the other Propositions presented in
http://www.cs.nyu.edu/pipermail/fom/2016-March/019585.html which use
fixed point minimizers. Of course, at this time I get a huge bonus
from working with fixed point minimizers -- namely the stuff
corresponds with the far far far more powerful HUGE cardinal
hierarchy. But under the current standards for this 50 year project -
perfect naturalness short of dealing directly with what mathematicians
are actually doing at this point in history - fixed point minimizers
are significantly less perfectly natural than maximal squares, powers,
and cliques. After the Embedded Maximal Squares, Powers, Cliques, and
Embedded Finite Maximal Squares, Powers, Cliques have been written up,
I will attack the HUGE cardinal situation in earnest in order to go
from natural to perfectly natural there as well.

The feedback from math icons has taken another turn for the better. In
addition to the Lead Propositions being viewed as completely natural,
it now appears that the Lead Finite Propositions are being viewed as
completely natural also. Furthermore, it looks like there will be
serious consideration given to the idea that these Leads are part of a
wider thematic subject which I provisionally call

*SYMMETRY IN MAXIMAL OBJECTS*
*SYMMETRIC MAXIMAL OBJECT THEORY*
*SMOT*

So from this point of view, the idea is being discussed that these
developments, although *apparently* not directly applicable at this
point to what mathematicians are actually now doing, nonetheless can
be viewed as ITS OWN APPLICATION. My own view is that I am necessarily
going well beyond ZFC to develop a seriously interesting thematic
mathematical subject which is totally INEVITABLE in the ongoing
history of mathematics.

A NEW POINT (modified from
http://www.cs.nyu.edu/pipermail/fom/2016-April/019677.html)
Various kinds of finitists and formalists may deny that Embedded
Maximal Squares, Powers, Cliques and even Embedded Finite Maximal
Squares, Powers, Cliques are meaningful or matter of fact. However, if
we use specific numbers for k,n,r in Embedded Finite Maximal Powers,
with specific a priori height bounds on the maximal object, then it
becomes much harder to deny that the statement is 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 with height bound 1000!! has at least 52! bytes (deck
of cards permutations) even if we use
sugared ZFC. If we use unsugared SRP then 16! suffices. If we use
sugared SRP then we get Colloquium Talk Range.

What is Colloquium Talk Range? That needs to be clarified on several
fronts. At one extreme is fully formalized proofs in proof assistants,
now and in the future. At the other is a study of effective
mathematical communication, even if not fully formal, but still
obviously correct (at several levels). This is much shorter, but by
how much?

Actually, detailed investigation of the relationship between sizes of
sugared and unsugared proofs is warranted. Any literature?

*********************************

Here we give the Combinatorial, Automorphism Action, and Model
Theoretic versions of the main definitions. We will only give the
Combinatorial version for graphs. We think that almost anyone who
tolerates graphs/cliques will prefer the combinatorial versions. Are
we right about that?

1. COMBINATORIAL (squares, powers)

We use these six notions:

x,y in Q^k are order equivalent.
V containedin Q^k is order invariant.
S^r containedin V is maximal.

x,y in Q^k are n-order equivalent.
S^r containedin V is order maximal.
S^r containedin V is n-order maximal.

The first group is for Embedded Maximal Squares, Powers. The second
group is for Embedded Finite Maximal Squares, Powers.

DEFINITION 1.1. x,y in Q^k are order equivalent if and only if for all
1 <= i <= k, x_i < x_j iff y_i < y_j. x,y in Q^k are n-order
equivalent if and only if (x,0,...,n),(y,0,...,n) are order equivalent
elements of Q^k+n+1. V containedin Q^k is order invariant if and only
if for all order equivalent x,y in Q^k, x in V iff y in V.

DEFINITION 1.2. A,B containedin Q^k are order equivalent if and only
if every element of A is order equivalent to an element of B and vice
versa. A,B containedin Q^k are n-order equivalent if and only if every
element of A is n-order equivalent to an element of B and vice versa.

DEFINITION 1.3. Let V containedin Q^k. S^r containedin V is maximal if
and only if every S'^r containedin V that includes S^r is S^r.  S^r
containedin V is order maximal if and only if every S'^r containedin V
that includes S^r is order equivalent to S^r.  S^r containedin V is
n-order maximal if and only if every S'^r containedin V that includes
S^r is n-order equivalent to S^r.

DEFINITION 1.4. For V containedin Q^k, V|<=n = {x in V: max(x) <= n}.

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.

EMBEDDED FINITE MAXIMAL SQUARES (weak). For all order invariant V
containedin Q^k,
some finite 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 FINITE MAXIMAL POWERS (weak). For all order invariant V
containedin Q^k,
some finite order maximal S^r containedin V|<=n is partially embedded by the
function p if p < 0; p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL SQUARES. For all order invariant V containedin Q^k,
some finite 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 FINITE MAXIMAL POWERS. For all order invariant V containedin Q^k,
some finite 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.

Note that these four finite statements are explicitly Pi03. We can a
priori upper bound the magnitudes of the numerators and denominators
in S (heights) and obtain explicitly Pi01 statements.

THEOREM 1.1. Embedded Maximal Squares, Powers are provably equivalent
to Con(SRP) over WKL_0. Embedded Finite Maximal Squares, Powers (weak)
are provable in EFA, Embedded Finite n-Maximal Squares, Powers, are
provably equivalent to Con(SRP) over EFA.

2. COMBINATORIAL (graphs, cliques)

DEFINITION 2.1. A graph G on X is an (X,E), where E containedin X^2
that is irreflexive and symmetric. E is called the edge or adjacency
relation. A clique in G is a subset of X where any two dissent
elements are adjacent. A maximal clique is a clique which is not the
proper subset of clique.

DEFINITION 2.2. A graph G on Q^k is order invariant if and only if the
adjacency relation E containedin Q^2k is order invariant.

DEFINITION 2.3. Let G be a graph on Q^k. G|<=n is the graph
(Q^k|<=n,E|<=n). S is an order maximal clique in G|<=n if and only if
S is a clique in G|<=n and every clique in G|<=n containing S is order
equivalent to S. S is an n-order maximal clique in G|<=n if and only
if S is a clique in G|<=n and every clique in G|<=n containing S is
n-order equivalent to S.

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.

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

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

Note that these two finite statements are explicitly Pi03. We can a
priori upper bound the magnitudes of the numerators and denominators
in S (heights) and obtain explicitly Pi01 statements.

THEOREM 2.1. Embedded Maximal Cliques are provably equivalent to
Con(SRP) over WKL_0. Embedded Finite Maximal Cliques (weak) is
provable in EFA, Embedded Finite n-Maximal Cliques is provably
equivalent to Con(SRP) over EFA.

3. AUTOMORPHISM ACTION

We use these five notions:

Q automorphism.
Q,n automorphism..
V containedin Q^k is fixed under all Q automorphisms.
S^r containedin V is Q automorphically maximal.
S^r containedin V is Q,n automorphically maximal.

DEFINITION 3.1. A Q automorphism is an automorphism of (Q,<). I.e., an
increasing bijection of Q. A Q,n automorphism is a Q automorphism that
fixes 0,1,...,n. V containedin Q^k is fixed under all Q automorphisms
if and only if the forward image of V under the coordinstewise
(diagonal) action of any Q automorphism is V

DEFINITION 3.2. Let V contaiendin Q^k. S^r containedin V is Q
automorphically maximal if and only if for every S^r containedin S'^r
containedin V, the union of the images of S^r under Q automorphisms
with the coordinstewise (diagonal) action includes S'^r. S^r
containedin V is Q,n automorphically maximal if and only if for every
S^r containedin S'^r containedin V, the union of the images of S^r
under Q,n automorphisms with the coordinstewise (diagonal) action
includes S'^r.

EMBEDDED MAXIMAL SQUARES. For all V containedin Q^k, fixed under all Q
automorphisms, 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 V containedin Q^k, fixed under all Q
automorphisms, some maximal S^r containedin V|<=n is partially
embedded by the function p if p < 0; p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL SQUARES (weak). For all V containedin Q^k,
fixed under all Q automorphisms, some finite Q automorphically maximal
S^2 containedin V|<=n is partially embedded by the function p if p <
0; p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL POWERS (weak). For all V containedin Q^k,
fixed under all Q automorphisms, some finite Q automorphically maximal
S^r containedin V|<=n is partially embedded by the function p if p <
0; p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL SQUARES. For all V containedin Q^k, fixed
under all Q,n automorphisms, some finite Q automorphically maximal S^2
containedin V|<=n is partially embedded by the function p if p < 0;
p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL POWERS. For all V containedin Q^k, fixed under
all Q,n automorphisms, some finite Q automorphically maximal S^r
containedin V|<=n is partially embedded by the function p if p < 0;
p+1 if p = 0,...,n-1.

Note that these four finite statements are explicitly Pi03. We can a
priori upper bound the magnitudes of the numerators and denominators
in S (heights) and obtain explicitly Pi01 statements.

THEOREM 3.1. Embedded Maximal Squares, Powers are provably equivalent
to Con(SRP) over WKL_0. Embedded Finite Maximal Squares, Powers (weak)
are provable in EFA, Embedded Finite n-Maximal Squares, Powers, are
provably equivalent to Con(SRP) over EFA.

4. MODEL THEORETIC

We only use 0-definable subset of Q^k. I don't quite see a good way to
define order maximal and n-order maximal, other than the combinatorial
definition, from the model theoretic point of view.

EMBEDDED MAXIMAL SQUARES. For all 0-definable 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 0-definable 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.

EMBEDDED FINITE MAXIMAL SQUARES (weak). For all 0-definable V
containedin Q^k, some finite 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 FINITE MAXIMAL POWERS (weak). For all 0-definable V
containedin Q^k, some finite order maximal S^r containedin V|<=n is
partially embedded by the function p if p < 0; p+1 if p = 0,...,n-1.

EMBEDDED FINITE MAXIMAL SQUARES. For all 0-definable V containedin
Q^k, some finite 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 FINITE MAXIMAL POWERS. For all 0-definable V containedin Q^k,
some finite 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.

Note that these four finite statements are explicitly Pi03. We can a
priori upper bound the magnitudes of the numerators and denominators
in S (heights) and obtain explicitly Pi01 statements.

THEOREM 4.1. Embedded Maximal Squares, Powers are provably equivalent
to Con(SRP) over WKL_0. Embedded Finite Maximal Squares, Powers (weak)
are provable in EFA, Embedded Finite n-Maximal Squares, Powers are
provably equivalent to Con(SRP) over EFA.

***********************************************
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 669th 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
668: Pi01 Incompleteness/SRP,HUGE/12  4/7/16  6:33PM

Harvey Friedman