[FOM] 671: Pi01 Incompleteness/SRP,HUGE/15

[Harvey Friedman]

THIS POSTING SUPERSEDES
http://www.cs.nyu.edu/pipermail/fom/2016-April/019779.html AND IS SELF
CONtAINED

We have greatly improved the  "magnificent" story told in 670: Pi01
Incompleteness/SRP,HUGE/14, in various ways. In particular, we have
found a proof in Z of the "MAGNIFICENT ONE" (called EMS below).The
natural proof uses SRP+ and gives some more nice information. That
additional information can only be obtained using SRP.

So the bottom line is that

i. Very substantial number of serious mathematical minds should be
captured by the Magnificent One - EMS (section 1). EMS is provable in
Z, and may or may not really need seriously set theoretic methods.
ii. Once captured by the Magnificent One, it does not seem possible to
resist being captured by the inevitable variants that raise the
foundational issues surrounding the status of ZFC and large cardinal
theory. In fact, below see three columns starting with EMS, each
ending with exclamation marks indicating the arrival at an implicitly
Pi01 statement provably equivalent to Con(SRP) over WKL_0

EMS                 EMS           EMS
ESMS,SEMS   NEMS         EMS(<=n)
SESMS!!!!        NESMS!!!!   NEMS(<=n)!!!!

Each step down each column is of the compelling kind that happens at
least hundreds of times every day across the spectrum of mathematics,
worldwide, regardless of area.

Our favorite implicitly Pi01 statement equivalent to Con(SRP) over
WKL_0 is NEMS(<=n). But we believe that EMS will capture significantly
more serious mathematical minds than NEMS(<=n).

We could just go from EMS to EMS(<=n) to NEMS(<=n). I.e., the reader
can simply look at sections 1,4. This is the quickest route to large
cardinals, corresponding to the third column above. However, we also
offer the first two columns, as direct strengthenings of EMS suggested
by the original and most natural proof of EMS, before moving entirely
to right endpoints. Obviously, we will prominently invite the reader
to explore all three paths in the Introduction.

By the way, "maximal embedded" should have been "embedded maximal".

While writing this, there appears to be some further rich
opportunities to add to the ammunition. We start with the "Magnificent
One", EMS. We then give this sharper version SEMS motivated by our
original proof that used large cardinals (before we found a proof in
ZFC), and naturalness considerations. Then we show that SEMS
corresponds to large cardinals.

What I am thinking of is a THEORY of improvements of EMS, or even more
broadly, a THEORY of EMS like statements, that inexorably lead to SEMS
and/or even sharper statements than SEMS, which similarly correspond
to large cardinals. I am thinking of a result like this: there is a
strongest simple improvement that is not absurd, and this strongest
simple improvement corresponds to large cardinals.

There are two moving parts here: the maximal square and the embedding.
There should be two developments here. One is "notions of maximal
square stronger than just a maximal square" and the other is "nice
embedding, nice being stronger than pointwise fixing exactly the
negative rationals".

I won't try to take this up in this already long posting. But if I get
anywhere, you will see it in followup postings.

1. Embedded Maximal Squares
2. Strong Embedded Step Maximal Squares
3. Naturally Embedded Step Maximal Squares
4. Naturally Embedded Maximal Squares (<=n)
5. Cubes and Cliques.

1. EMBEDDED MAXIMAL SQUARES

DEFINITION 1.1. N,Z,Q are the set of all nonnegative integers,
integers, and rationals, respectively. We use n,m,r,s,t for positive
integers and p,q for rationals, with and without subscripts, unless
otherwise indicated. x,y in Q^k are order equivalent if and only if
for all 1 <= i,j <= n, x[i] < x[j] iff y[i] < y[j]. 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.

EX: (-1/2,3,3/2) and (-7,-5/2,-6) are order equivalent.

THEOREM 1.1. Order equivalence on Q^k is an equivalence relation with
finitely many equivalence classes. x,y in Q^k are order equivalent if
and only if there is an increasing bijection h:Q into Q which sends x
to y under the coordinstewise (diagonal) action. Let V containedin
Q^k. The following are equivalent.
i. V is fixed under all increasing bijections h:Q into Q with the
coordinatewise (diagonal) action.
ii. V is the union of equivalence classes of Q^k under order equivalence.
iii. V is first order definable over (Q,<) without parameters.
iv. V is order invariant.

DEFINITION 1.2.  Let V containedin Q^k. A square in V is a set S^2
containedin V. A maximal square in V is a square in V that is not a
proper subset of any square in V. A self embedding of V is a one-one
h:Q into Q which preserves V under the coordinatewise (diagonal)
action. I.e., for all p_1,...,p_k, (p_1,...,p_k) in V iff
(h(p_1),...,h(p_k)) in V. An automorphism of V is a surjective self
embedding of V.

EMBEDDED MAXIMAL SQUARES. EMS. In every order invariant subset of Q^k,
some maximal square has a self embedding that pointwise fixes exactly
the negative rationals.

THEOREM 1.2. EMS is provable in ZFC, and in fact in Z = Zermelo set
theory. Moreover, WKL_0 + Con(RTT) suffices, where RTT is Russell's
theory of types in modern form.

There is a version of EMS for automorphisms.

AUTOMORPHIC MAXIMAL SQUARES. AUMS. In every order invariant subset of
Q^k, some maximal square has an automorphism that pointwise fixes
exactly the rationals < sqrt(2).

THEOREM 1.3. AUMS is provable in ZFC, and in fact in Z and in WKL_0 + Con(RTT).

EMS and AUMS are very concrete in the following sense.

THEOREM 1.4. EMS and AUMS are implicitly Pi01 via the Goedel
Completeness Theorem.

2. STRONG EMBEDDED STEP MAXIMAL SQUARES.

Our original proof of EMS uses far more than ZFC, and appears to
really be the natural proof of EMS. According to Theorem 1.2, we
managed to cut down the high powered set theoretic apparatus to live
within Z. At this point, we do not have any idea as to how much of the
remaining set theoretic apparatus is really needed.

Our original proof of EMS provides a maximal square and a self
embedding with some very natural additional properties. This results
in the stronger statement, Strong Embedded Maximal Squares, or SEMS.
For SEMS, we know that it is necessary and sufficient to go well
beyond ZFC in order to give a proof. This explains why our original
proof of EMS used such heavy set theoretic assumptions. It actually
gave more information than is required for EMS - information that we
now know cannot be obtained in ZFC alone.

This original proof gives a self embedding that additionally maps each
nonnegative integer to its successor, and also what we call a step
maximal square.

DEFINITION 2.1. Let V containedin Q^k. V|<=n = {x in V: max(x) <= n}.
A step maximal square in V is an S^2 such that for all n in N, S^2|<=n
is a maximal square in V|<=n.

THEOREM 2.1. Every step maximal square in V containedin Q^k is a
maximal square in V. The converse is false even for some order
invariant V containedin Q^4.

EMBEDDED STEP MAXIMAL SQUARES. ESMS. In every order invariant subset
of Q^k, some step maximal square has a self embedding that pointwise
fixes exactly the negative rationals.

STRONG EMBEDDED MAXIMAL SQUARES. SEMS. In every order invariant subset
of Q^k, some maximal square has a self embedding that pointwise fixes
exactly the negative rationals and sends each nonnegative integer to
its successor.

STRONG EMBEDDED STEP MAXIMAL SQUARES. SESMS. In every order invariant
subset of Q^k, some step maximal square has a self embedding that
pointwise fixes exactly the negative rationals, and maps each
nonnegative integer to its successor.

Note that ESMS and SEMS arise from using the two additional properties
arising from our original proof of EMS, separately. SESMS uses them
jointly.

THEOREM 2.2. ESMS, SESMS are implicitly Pi01 via the Goedel
Completeness Theorem.

THEOREM 2.3. ESMS is provable in ZFC, and in fact in Z = Zermelo set
theory. Moreover, WKL_0 + Con(RTT) suffices, where RTT is Russell's
theory of types in modern form.

We do not know if SEMS is provable in ZFC.

THEOREM 2.4. SESMS is provably equivalent to Con(SRP) over WKL_0.

Actually, a very weak form of step maximality can be used in SESMS to
get independence from ZFC. The most natural context for this is to use
the ambient spaces Q^k|<=n rather than the present Q^k. This is taken
up in sections 4,5. Of course, the right endpoint idea is already been
used in Definition 2.1.

3. NATURALLY EMBEDDED STEP MAXIMAL SQUARES

Note that we have said nothing about the naturalness of the self
embeddings thus far. For SESMS, we know that the self embedding cannot
even be required to be recursive, let alone natural. We don't know
this for the other statements of sections 1,2. Even SMS (no self
embedding at all), the maximal square cannot be required to be
recursive.

However, if we allow partial self embeddings, then we can have
naturalness. In fact, we will always use the extremely natural partial
function p if p < 0; p+1 if p in N. The domain of this function is
Q|<0 union N.

DEFINITION 3.1. Let V containedin Q^k. A partial self embedding of V
is a partial one-one h:Q into Q which preserves V under the
coordinatewise (diagonal) action. I.e., for all p_1,...,p_k in dom(h),
(p_1,...,p_k) in V iff (h(p_1),...,h(p_k)) in V.

NATURALLY EMBEDDED MAXIMAL SQUARES. NEMS.  In every order invariant
subset of Q^k, some maximal square is partially self embedded by p if
p < 0; p+1 if p in N.

NATURALLY EMBEDDED STEP MAXIMAL SQUARES. NESMS.  In every order
invariant subset of Q^k, some step maximal square is partially self
embedded by p if p < 0; p+1 if p in N.

THEOREM 3.1. NESMS is implicitly Pi01 via the Goedel Completeness Theorem.

THEOREM 3.2. NESMS is provably equivalent to Con(SRP) over WKL_0.

We do not know if NEMS is provable in ZFC.

4. NATURALLY EMBEDDED MAXIMAL SQUARES (<=n)

We now restart the investigation using Q|<=n instead of Q. Thus we are
restarting with a right endpoint. This supports a major simplification
- namely step maximality is no longer required for us to arrive at
independence from ZFC. We begin by adapting Definitions 1,2, 1.2 and
3.1 in this new context. To emphasize the new ambient spaces Q^k|<=n,
we will always carry them along with V (unless the ambient space is of
no consequence)..

DEFINITION 4.1. V containedin Q^k is order invariant if and only if
for all order equivalent x,y in Q^k|<=n, x in V iff y in V.

DEFINITION 4.1. V containedin Q^k|<=n is order invariant if and only
if for all order equivalent x,y in Q^k|<=n, x in V iff y in V. A
square in V is a set S^2 containedin V. A maximal square in V is a
square in V that is not a proper subset of any square in V. A self
embedding of V containedin Q^k|<=n is a one-one h:Q|<=n into Q|<=n
which preserves V under the coordinatewise (diagonal) action. I.e.,
for all p_1,...,p_k, (p_1,...,p_k) in V iff (h(p_1),...,h(p_k)) in V.
A partial self embedding of V containedin Q^k|<=n is a partial one-one
h:Q|<=n into Q|<=n which preserves V under the coordinatewise
(diagonal) action. I.e., for all p_1,...,p_k in dom(h), (p_1,...,p_k)
in V iff (h(p_1),...,h(p_k)) in V.

EMBEDDED MAXIMAL SQUARES (<=n). EMS(<=n). In every order invariant
subset of Q^k|<=n, some maximal square has a self embedding that
pointwise fixes exactly the negative rationals.

NATURALLY EMBEDDED MAXIMAL SQUARES (<=n). NEMS(<=n). In every order
invariant subset of Q^k, some maximal square is partially self
embedded by p if p < 0; p+1 if p = 0,...,n-1.

THEOREM 4.1. EMS(<=n), NEMS(<=n) are implicitly Pi01 via the Goedel
Completeness Theorem.

THEOREM 4.2. EMS is provable in ZFC, and in fact in Z = Zermelo set
theory. Moreover, WKL_0 + Con(RTT) suffices, where RTT is Russell's
theory of types in modern form.

THEOREM 4.3. NEMS(<=n) is provably equivalent to Con(SRP) over WKL_0.

5. CUBES AND CLIQUES

All of the statements considered here about squares have two equally
natural variants.

In the first variant, we replace "square" by "r-cube". Whereas a
square is an S^2, and r-cube is an S^r. Thus a square is a 2-cube.

In the second variant, we use graphs and cliques.

The adaptation from squares to r-cubes is so transparent that there is
no need to give the corresponding definitions.

For the adaptation of squares to cliques, we will give the
corresponding definitions.

DEFINITION 5.1. A graph on a set A is a pair G = (A,E), where E
containedin A^2 is irreflexive and symmetric. A clique in G is a
subset of A where any two distinct elements x,y have x E y. A maximal
clique in G is a clique in G which is not a proper subset of any
clique in G.

DEFINITION 5.2. An order invariant graph on Q^k is a graph G =
(Q^k,E), where E containedin Q^2k is order invariant. An order
invariant graph on Q^k|<=n is a graph G = (Q^kl|<=n,E), where E
containedin Q^2k|<=n is order invariant. If G is a graph (Q^k,E) then
G|<=n is the graph (Q^k|<=n,E|<=n). A step maximal clique in G is a
clique S in G where for all n in N, S|<=n is a maximal clique in
G|<=n.

All results are the same for these variants.

We will just present the obvious variants for EMS and NEMS(<=n). The
others are analogous.

EMBEDDED MAXIMAL CUBES. EMC. In every order invariant subset of Q^k,
some maximal r-cube has a self embedding that pointwise fixes exactly
the negative rationals.

EMBEDDED MAXIMAL CLIQUES. EMQ. In every order invariant graph on Q^k,
some maximal clique has a self embedding that pointwise fixes exactly
the negative rationals.

NATURALLY EMBEDDED MAXIMAL CUBES (<=n). NEMC(<=n). In every order
invariant subset of Q^k|<=n, some maximal r-cube is partially self
embedded by p if p < 0; p+1 if p = 0,...,n-1.

NATURALLY EMBEDDED MAXIMAL CLIQUES (<=n). EMQ(<=n). In every order
invariant graph on Q^k|<=n, some maximal clique is partially self
embedded by p if p < 0; p+1 if p = 0,...,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 671st 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
669: Pi01 Incompleteness/SRP,HUGE/13  4/17/16  2:51PM
670: Pi01 Incompleteness/SRP,HUGE/14  4/28/16  1:40AM

Harvey Friedman