[FOM] 670: Pi01 Incompleteness/SRP,HUGE/14
Harvey Friedman
hmflogic at gmail.com
Thu Apr 28 01:40:30 EDT 2016
We have discovered a MAGNIFICENT version of our Lead Propositions
which we prove using Con(SRP).
I have previously only claimed PERFECTLY MATHEMATICALLY NATURAL
statements which are provably equivalent to Con(SRP).
HOWEVER, we have come to no opinion as to whether this MAGNIFICENCE
can be proved in ZFC, or whether it is provably equivalent to
Con(SRP).
So this new magnificent version is going to be our new Lead
Proposition - as the lead into the versions that are merely perfectly
mathematical natural, and for which we KNOW are provably equivalent to
Con(SRP).
Thus the choice of this new magnificent Proposition drives the
narrative for all of the previous Lead Propositions. This is why we
have slightly modified them below. See Theorem 2.3.
In fact, the proof that we give of the MAGNIFICENT ONE actually
provides some specific natural information that we KNOW is independent
of ZFC.
1. MAXIMAL EMBEDDED SQUARES, CUBES, CLIQUES IN Q,Q|<=n
In this section we use everywhere defined embeddings (referred to embeddings).
MAXIMALEMBEDDED SQUARES (Q). Every order invariant subset of Q^k has a
maximal square with an embedding fixing exactly the negative
rationals.
MAXIMAL EMBEDDED CUBES (Q). Every order invariant subset of Q^k has a
maximal r-cube with an embedding fixing exactly the negative
rationals.
MAXIMAL EMBEDDED CLIQUES (Q). Every order invariant graph on Q^k has a
maximal clique with an embedding fixing exactly the negative
rationals.
Note that these Propositions do not use right endpoints, partial
embeddings, or special maps. Here the embeddings are everywhere
defined.
It is also natural to use the Q^k||<=n. Since our statements are
purely order theoretic, the choice of positive integer n is of no
consequence.
Here Q^k|<=n = (Q intersect (-infinity,n])^k. Order invariant subsets
of Q^k|<=n are subsets V of Q^k|<=n where for order equivalent x,y in
Q^k|<=n, x in V iff y in V.
MAXIMALEMBEDDED SQUARES (Q|<=n). Every order invariant subset of
Q^k|<=n has a maximal square with an embedding fixing exactly the
negative rationals.
MAXIMAL EMBEDDED CUBES (Q|<=n). Every order invariant subset of
Q^k|<=n has a maximal r-cube with an embedding fixing exactly the
negative rationals.
MAXIMAL EMBEDDED CLIQUES (Q|<=n). Every order invariant graph on
Q^k|<=n has a maximal clique with an embedding fixing exactly the
negative rationals.
THEOREM 1.1. All six are implicitly Pi01 via the Goedel Completeness Theorem.
THEROEM 1.2. RCA_0 proves
i. Maximal Embedded Squares (Q) if and only if Maximal Embedded Cliques (Q).
ii. Maximal Embedded Squares (Q|<=n) if and only if Maximal Embedded
Cliques (Q|<=n).
iii. Maximal Embedded Squares (Q|<=n) if and only if Maximal Embedded
Cliques (Q|<=n).
iv. Maximal Embedded Cubes (Q|<=n) implies Maximal Embedded Cubes (Q).
v. Maximal Embedded Squares (Q|<=n) implies Maximal Embedded Squares (Q).
THEOREM 1.3. All six are provable in SRP+. In fact, they are provable
in WKL_0 + Con(SRP). The same holds if we additionally require that
the embedding is +1 on N.
We do not know whether any or all of these six are provable in ZFC.
2. MAXIMAL NATURALLY EMBEDDED SQUARES, CUBES, CLIQUES IN Q,Q|<=n
In the proof of the six Propositions of section 1, we did not
construct a natural maximal object or a natural embedding. We do not
know if that can be done.
However, our proof of Maximal Embedded Cubes (Q) does construct a very
natural embedding that is partially defined. We refer to this as a
partial embedding. Specially, that proof establishes all of the nine
Propositions presented in this section. We know that the fourth,
fifth, and sixth are independent of ZFC; see Theorem 2.3.
MAXIMAL NATURALLY EMBEDDED SQUARES (Q). Every order invariant subset
of Q^k has a maximal square partially embedded by p if p < 0; p+1 if p
in N.
MAXIMAL NATURALLY EMBEDDED CUBES (Q). Every order invariant subset of
Q^k has a maximal r-cube partially embedded by p if p < 0; p+1 if p in
N.
MAXIMAL NATURALLY EMBEDDED CLIQUES (Q). Every order invariant graph on
Q^k has a maximal clique partially embedded by p if p < 0; p+1 if p in
N.
MAXIMAL NATURALLY EMBEDDED SQUARES (Q|<=n). Every order invariant
subset of Q^k|<=n has a maximal square partially embedded by p if p <
0; p+1 if p = 0,...,n-1.
MAXIMAL NATURALLY EMBEDDED CUBES (Q|<=n). Every order invariant subset
of Q^k|<=n has a maximal r-cube partially embedded by p if p < 0; p+1
if p = 0,...,n-1.
MAXIMAL NATURALLY EMBEDDED CLIQUES (Q|<=n). Every order invariant
graph on Q^k|<=n has a maximal clique partially embedded by p if p <
0; p+1 if p = 0,...,n-1.
THEOREM 2.1. The last three are implicitly Pi01 via the Goedel
Completeness Theorem.
THEOREM 2.2. All six are provable in SRP+. In fact, they are provable
in WKL_0 + Con(SRP).
THEOREM 2.3. the last three are provably equivalent to Con(SRP) over WKL_0.
We do not know if any or all of the first three are provable in ZFC.
We now consider the following weakened forms of the first three.
MAXIMAL NATURALLY EMBEDDED SQUARES (Q,limited). Every order invariant
subset of Q^k has a maximal square partially embedded by p if p < 0;
p+1 if p = 0,...,n-1.
MAXIMAL NATURALLY EMBEDDED CUBES (Q,limited). Every order invariant
subset of Q^k has a maximal r-cube partially embedded by p if p < 0;
p+1 if p = 0,...,n-1.
MAXIMAL NATURALLY EMBEDDED CLIQUES (Q,limited). Every order invariant
graph on Q^k has a maximal clique partially embedded by p if p < 0;
p+1 if p = 0,...,n-1.
THEOREM 2.4. These three are provable in Z = Zermelo set theory. In
fact, in WKL_0 + Con(RTT).
Here RTT is Russell's theory of types in modern form.
There is a straightforward adaption of Theorem 1.2 for this section.
***********************************************
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 670th 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
Harvey Friedman
More information about the FOM
mailing list