[FOM] 675:Embedded Maximality and Pi01 Incompleteness/1
Harvey Friedman
hmflogic at gmail.com
Sat May 7 00:45:43 EDT 2016
In http://www.cs.nyu.edu/pipermail/fom/2016-May/019792.html we used
embeddings in maximal squares in order invariant sets
to achieve perfectly mathematical implicitly Pi01 sentences equivalent
to Con(SRP).
In earlier abstracts in the series, we achieved considerable
mathematical naturalness using fixed point minimizers for Con(HUGE).
It has been a while since the Con(HUGE) statements have been improved
on, as we are currently concentrating on the Con(SRP) statements.
***********************
There has been a stack of breakthrough ideas that bring
http://www.cs.nyu.edu/pipermail/fom/2016-May/019792.html to a new
level. I had the new ideas here some time ago in weaker form, through
what I called continuations and emulations, but these ideas were not
perfected as they are here, and I was also distracted by the CRUCIAL
BREAKTHROUGH some time ago of bringing in explicitly given partial
self embeddings.
EMBEDDED MAXIMALITY
by
Harvey M. Friedman
May 5, 2016
Abstract. Two subsets of Q^k are similar if they have the same two
element subsets up to isomorphism. In each equivalence class of the
subsets of Q^k under similarity, some inclusion maximal set is
partially self embedded by p if p < 0; p+1 if p in N. In each
equivalence class of the subsets of Q^k|<=n under similarity, some
inclusion maximal set is partially self embedded by p if p < 0; p+1 if
p = 0,...,n-1. Our proof of these statements use far more than the
usual ZFC axioms for mathematics. For the second statement, we know
that ZFC is not sufficient. ZFC does prove that in each equivalence
class of the subsets of Q^k under similarity, some maximal element is
partially self embedded by p if p < 0; p+1 if p = 0,...,n-1. Related
results are presented involving only finite subsets of N^k.
1. INTRODUCTION
...
SRP is ZFC + {there exists an ordinal with the SRP[k]}_k. SRP+ is ZFC
+ (for all k)(there exists an ordinal with the SRP[k]). RCA_0, WKL_0
are our first two systems for Reverse Mathematics. EFA is Exponential
Function Arithmetic. Z is Zermelo set theory.
2. ENDPOINT EMBEDDED MAXIMALITY
DEFINITION 2.1. N,Z,Q is the set of all nonnegative integers,
integers, rationals, respectively. We use k,n,m for positive integers
and p,q for rationals, with and without subscripts, unless indicated
otherwise. Q^k|<=n is the set of all elements of Q^k whose maximum
coordinate is <= n. Let A,B contaeindin Q^k. fld(A) is the set of all
coordinates of elements of A. A,B are isomorphic if and only if there
exists an increasing bijection h:fld(A) into fld(B) such that for all
p_1,...,p_k in dom(h), (p_1,...,p_k) in A iff (h(p_1),...,h(p_k)) in
B. A,B are similar if and only if every subset of A of cardinality <=
2 is isomorphic to some subset of B of cardinality <= 2, and vice
versa.
THEOREM 2.1. Similarity on subsets of Q^k and Q^k|<=n have the same
finite number of equivalence classes.
DEFINITION 2.2. Let A containedin Q^k. h is a partial self embedding
of A if and only if
i. h:Q into Q is partial and strictly increasing.
ii. For all p_1,...,p_k in dom(h), (p_1,...,p_k) in A iff
(h(p_1),...,h(p_k)) in A.
EMBEDDED MAXIMALITY. EM. In each equivalence class of the subsets of
Q^k under similarity, some inclusion maximal set is partially self
embedded by p if p < 0; p+1 if p in N.
ENDPOINT EMBEDDED MAXIMALITY. EEM. In each equivalence class of the
subsets of Q^k|<=n under similarity, some inclusion maximal set is
partially self embedded by p if p < 0; p+1 if p = 0,...,n-1.
WEAK EMBEDDED MAXIMALITY. WEM. In each equivalence class of the
subsets of Q^k under similarity, some inclusion maximal set is
partially self embedded by p if p < 0; p+1 if p = 0,...,n-1.
The "Endpoint" in "Endpoint Embedded Maximality" refers to the right
endpoint n in EEM.
THEOREM 2.2. EEM, WEM are implicitly Pi01 via the Goedel Completeness Theorem.
THEOREM 2.3. EEM is provably equivalent to Con(SRP) over WKL_0. WEM is
provable in Z.
We do not know if EM is provable in ZFC. Our proof of EM immediately proves EEM.
3. FINITE EMBEDDED MAXIMALITY
DEFINITION 3.1. [t] = {0,...,t}. A,B containedin [kt]^k are strongly
similar if and only if A x {(t!,2t,...,kt)} and B x {(t,2t,...,kt)}
are similar. Let X be a family of subsets of [kt]^k. S is a weakly
maximal element of X if and only if S in X, and every superset of S in
X is strongly similar to S.
FINITE EMBEDDED MAXIMALITY. FEM. In each equivalence class of the
subsets of [k(8k)!]^k under similarity, some weakly maximal set is
partially self embedded by m if m < (8k)!; m+(8k)! if m =
(8k)!,2(8k)!,...,(k-1)(8k)!.
Obviously, FEM is in explicitly finite form.
THEOREM 3.1. FEM is 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 675th 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
673: Pi01 Incompleteness/SRP,HUGE/16 5/1/16 11:27PM
674: Refuting the Continuum Hypothesis?/2 5/4/16 2:36AM
Harvey Friedman
More information about the FOM
mailing list