[FOM] 673: Pi01 Incompleteness/SRP,HUGE/16
Harvey Friedman
hmflogic at gmail.com
Sun May 1 23:27:44 EDT 2016
THIS IS A RESTATEMENT OF
http://www.cs.nyu.edu/pipermail/fom/2016-April/019785.html
This posting is just to fine tune the "Magnificent Story".
The main change, driven by the STORYLINE is that I am going to stick
with just the one ambient space Q, and not use Q|<=n. The restrictions
|<=n are used for the maximality notion only. In section 4 the idea of
using restricted ambient spaces Q|<=n in mentioned as an option in
passing.
This overall simplification is mathematically of little consequence.
But intellectually, arguably of serious consequence. As you can see
from the series 1-15, I have been wavering between using only one
ambient space and nuanced maximality, versus using these restricted
ambient spaces and just maximality.
Here are the advantages of using just one ambient space Q (actually the Q^k).
i. The characterization of the all important crucial notion of order
invariant set is better for for subsets of Q^k than for subsets of
Q^k|<=n for some significant number of mathematicians on the abstract
side of things. Specifically, one of the characterizations of order
invariant subsets of Q^k is that they are the subsets of Q^k that are
fixed under all increasing surjections from Q to Q. HOWEVER, it is NOT
the case that the order invariant subsets of Q^k|<=n are exactly the
subsets of Q^k|<=n that are fixed under all increasing surjections
from Q to Q. The obvious counterexample in one dimension is {n}.
ii. I start with the "Magnificent One", EMS, trying to draw all
serious mathematical minds into the foundational abyss. This is my
best shot.
iii. So there are four major statements. EMS, which, unfortunately or
fortunately maybe, has its natural proof using large cardinals, but an
unnatural proof within Z = Zermelo set theory.
iv. The natural proof of EMS actually proves the refinement SESMS, and
it is argued, at this time INFORMALLY, that this is the canonical
strongest simple refinement of EMS. Now SESMS is independent of ZFC
(corresponds to large cardinals).
v. Cutting out the amorphous fat in the self embedding in SESMS give
us the immediate consequence NESMS. Still independent of ZFC
(corresponds to large cardinals).
vi. NOW, a very weak part of NESMS, which we call NEPMS, already is
independent of ZFC (corresponds to large cardinals).
vii. The reader is instructed that there are four main statements:
EMS naturally strengthened to SESMS naturally weakened to NESMS
naturally weakened to NEPMS.
the last three of which are independent of ZFC and correspond to large
cardinals. All of them are implicitly Pi01 via the Goedel Completeness
Theorem.
The reader is advised that they should go forward in this list of
four, ignoring any that they want, as long as they end with NEPMS.
PRONUNCIATIONS: EMS (ems). SESMS (ses-mis). NESMS (nes-mis). NEPMS (nep-mis).
1. Embedded Maximal Squares
2. Strong Embedded Step Maximal Squares
3. Naturally Embedded Step Maximal Squares
4. Naturally Embedded Point Maximal Squares
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.
MAXIMAL SQUARES. MS. Every subset of Q^k has a maximal square.
THEOREM 1.2. MS is provable in RCA_0.
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.3. 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.4. 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.5. 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.
STEP MAXIMAL SQUARE. SMS. Every subset of Q^k has a step maximal square.
THEOREM 2.2. SMS is provably equivalent to (for all x containedin
omega)(the omega-th Turing jump of x exists) over RCA_0. SMS for order
invariant subsets of Q^k is provably equivalent to "the set of true
sentences of arithmetic exists" over RCA_0.
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.
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 in SMS, 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. This function cuts out the amorphous fat in the self
embedding in SESMS.
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 POINT MAXIMAL SQUARES
For step maximal squares, we have used maximality in the various
V|<=n. We think of these as point maximality for each point n in N.
It is remarkable that maximality in only a single V|<=n suffices to
obtain independence from ZFC and correspondence with large cardinals.
NATURALLY EMBEDDED POINT MAXIMAL SQUARES. NEPMS. In any order
invariant V containedin Q^k, some maximal S^2 containedin V|<=n is
partially self
embedded by p if p < 0; p+1 if p = 0,...,n-1.
Note that we are not even requiring that S be a maximal clique or even
a clique. All of the action in the statement lives in Q^k|<=n.
An expositional option is to use the ambient space Q^k|<=n instead of
Q^k. There is one point that should be kept in mind. The order
invariant subsets of Q^k|<=n would need to be defined with a little
care. Note that the Galois theoretic characterization of order
invariant subsets of Q^k as the subsets of Q^k fixed under all
increasing bijections from Q into Q, fails with Q replaced by Q|<=n.
Even in one dimension, the Galois theoretic approach would make {n} an
order invariant subset of Q|<=n, which would ruin our entire
development.
THEOREM 4.1. NEPMS(<=n) are implicitly Pi01 via the Goedel
Completeness Theorem.
THEOREM 4.2. NEPMS(<=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 NEPMS. 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 POINT MAXIMAL CUBES. NEMC(<=n). In every order
invariant V containedin Q^k, some maximal S^r containedin V|<=n is
partially self
embedded by p if p < 0; p+1 if p = 0,...,n-1.
NATURALLY EMBEDDED POINT MAXIMAL CLIQUES. NEPMQ. In every order
invariant graph G on Q^k, some maximal clique in G|<=n 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
671: Pi01 Incompleteness/SRP,HUGE/15 4/30/16 12:03AM
672: Refuting the Continuum Hypothesis? 5/1/16 1:11AM
Harvey Friedman
More information about the FOM
mailing list