[FOM] 679:Symmetric Maximality and Pi01 Incompleteness/1
Harvey Friedman
hmflogic at gmail.com
Mon May 23 21:21:44 EDT 2016
THIS POSTING IS ENTIRELY SELF CONTAINED
We continue to polish
http://www.cs.nyu.edu/pipermail/fom/2016-May/019837.html Here are the
new decisions.
For Implicitly Pi01:
c. Change the wording to "agreeing at (0,...,k-1) and (1,...,k)".
Purely notational.
For explicitly Pi01:
We have now chosen to leverage off of the setup for the implicitly
Pi01 above. We now use the finite subspaces RPF[k;n,m] of RPF[k] under
r-similarity. We ask for a maximal element with the same conclusion
as before.
What's new here is that I use inclusion maximality both for the
implicitly and explicitly Pi01 statements.
1. IMPLICITLY Pi01
DEFINITION 1.1. Q,Z,N is the set of all rationals, integers,
nonnegative integers, respectively. We use p,q for rationals and
n,m,r,s,t for positive integers, with and without subscripts, unless
otherwise indicated. Let x,y be tuples from Q. x <,>,<=,>= y if and
only if every coordinate of x is <,>,<=,>= every coordinate of y. x,y
are order equivalent if and only if x,y are of the same length, and
for all 1 <= i,j <= lth(x), x[i] < x[j] iff y[i] < y[j].
DEFINITION 1.2. RPF[k] is the set of all partial f:Q^k|<=k into
Q^k|<=k such that for all x in dom(f), f(x) < x. f,g in RPF[k] are
similar if and only if every (x,y,gx,gy) is order equivalent to some
(x,y,fx,fy) . Maximality of elements of K containedin RPF[k] refers to
inclusion maximality of the functions as sets (graphs of the
functions)
Here RPF is read "regressive partial functions".
Note that similarity indicates a sameness in some of the order
theoretic patterns that appear in f,g.
THEOREM 1.1. Similarity on RPF[k] is an equivalence relation with
finitely many equivalence classes. Each has a maximal element.
So we have partitioned our space RPF[k] naturally into finitely many
parts, each of which has a maximal element. We claim that these
maximal elements can be chosen to exhibit a certain simple symmetry.
SYMMETRIC MAXIMALITY. SM. In every equivalence class of RPF[k] under
similarity, some maximal element agrees at (0,...,k-1) and (1,...,k).
THEOREM 1.2. Symmetric Maximality is provably equivalent to a Pi01
sentence via the Goedel Completeness Theorem.
THEOREM 1.3. Symmetric Maximality is provably equivalent to Con(SRP) over WKL_0.
There is an obvious generalization of similarity to r-similarity.
DEFINITION 1.3. f,g in RPF[k] are r-similar if and only if every
(x_1,...,x_r,g(x_1),...,g(x_r)) is order equivalent to some
(y_1,...,y_r,f(y_1),...,f(y_r)).
The above results hold with similarity replaced by r-similarity.
2. EXPLICITLY Pi01
DEFINITION 2.1. The height of a finite set of tuples from Q is the
least t such that the coordinates of all of its elements can be
expressed as a ratio between integers of magnitude <= t. RPF[k;n,m] is
the set of all f in RPF[k] such that the height of f|N^k is <= n and
the height of f is <= m.
FINITE SYMMETRIC MAXIMALITY. FSM. In every equivalence class of
RPF[k;(8k)!,(8k)!!] under k-similarity, some maximal element agrees at
(0,...,k-1) and (1,...,k).
Obviously Finite Symmetric Maximality is explicitly Pi01.
THEOREM 2.1. Finite Symmetric Optimality is provably equivalent to
Con(SRP) over EFA.
3. COMMENTS
This should now be enough for me to stop making any further
simplifications. The reversals are now stacked up quite high with
recent new ideas. I am still looking to the end of 2016 for a detailed
proof of the theorems in this posting.
***********************************************
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 679th 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
675: Embedded Maximality and Pi01 Incompleteness/1 5/7/16 12:45AM
676: Refuting the Continuum Hypothesis?/3 5/10/16 3:30AM
677:Embedded Maximality and Pi01 Incompleteness/2 5/17/16 7:50PM
678:Symmetric Optimality and Pi01 Incompleteness/1 5/19/16 1:22AM
Harvey Friedman
More information about the FOM
mailing list