[FOM] 663: Pi01 Incompleteness/SRP,HUGE/8
Harvey Friedman
hmflogic at gmail.com
Thu Feb 25 15:59:56 EST 2016
Things seem to be falling into place now, with four major statements.
1. Lead Proposition. Lives in Q. Unchanged. Corresponds to SRP.
2. Lead Finite Proposition. Lives in Z+ and corresponds to SRP. As in
http://www.cs.nyu.edu/pipermail/fom/2016-February/019533.html with
some improved friendly notation.
3. Lead HUGE Proposition. Lives in Q and corresponds to HUGE. Notation
changed from earlier.
4. Lead Finite HUGE Proposition. Lives in Z+.
2,3,4 are at least approaching the magic line. I will be continuing
http://www.cs.nyu.edu/pipermail/fom/2015-November/019360.html taking
up the notion of "magic line".
1. LEAD PROPOSITION
LEAD PROPOSITION. For all order invariant V containedin Q[0,n]^k, some
maximal S^2 containedin V is partially embedded by the function p if p
< 1; p+1 if p = 1,...,n-1.
Just remember that partial embeddings use if and only if, and work
within the domain of the partial embedding.
THEOREM 1.1. Lead Proposition is provably equivalent to Con(SRP) over WKL_0.
2. LEAD FINITE PROPOSITION
DEFINITION 2.1. As is standard, the f:A into B are the functions with
domain A and range containedin B, and the partial f:A into B are the
functions whose domain is contained in A and whose range is contained
in B. We say that f sends A to B to C if and only if A,B containedin
dom(f) and f[A] containedin B and f[B] contained in C. A function is
without x if and only if x is not a coordinate of any of its arguments
or values.
Recall p stands for rationals, and i,k,n stand are positive integers.
DEFINITION 2.2. [p] = {i: i <= p}. For A containedin N, A! = {n!: n in A}.
DEFINITION 2.3. Let R containedin [n]^k. A fixed point minimizer for R
is a partial f:[n]^k into [n]^k, where every f(x) is the
lexicographically least y = f(y) with R(x,y). For sections 3,4, A <=
fixed point minimizer for R is a partial f:[n]^k into [n]^k, where
every f(x), x_1 <= ... <= x_k, is the lexicographically least y = f(y)
with R(x,y).
LEAD FINITE PROPOSITION. Every reflexive order invariant R containedin
[n!]^2k has a fixed point minimizer sending [n/8k]!^k to (A intersect
A-1)^k to [n!]^k, without (8k)!-1.
Obviously Lead Finite Proposition is explicitly Pi01.
THEOREM 2.1. Lead Finite Proposition is provably equivalent to
Con(MAH) over EFA.
Recall MAH is ZFC + {there exists an n-Mahlo cardinal}_n.
3. LEAD HUGE PROPOSITION
LEAD HUGE PROPOSITION. Every reflexive order invariant R containedin
Q^2k has a <= fixed point minimizer f:A^k into A^k with comparable
nontrivial partial embeddings f_n...n|<n-1.
Here f_n...n is obtained from f by fixing the first k-1 arguments to
be n. f_n...n|<n-1 is the restriction of f_n...n to (-inifnity,n-1).
Comparable means agree where both defined. Nontrivial means not the
identity.
THEOREM 3.1. Lead Huge Proposition is provably equivalent to Con(HUGE)
over WKL_0.
4. LEAD FINITE HUGE PROPOSITION
LEAD FINITE HUGE PROPOSITION. Every reflexive order invariant R
containedin [n!]^2k has a <= fixed point minimizer sending [n/8k]!^k
to A^k to [n!]^k, with comparable nontrivial partial embeddings
f_j!...j!|<(j-1)!, 8k < j < n/8k.
THEOREM 4.1. Lead Finite Huge Proposition is provably equivalent to
Con(HUGE) over EFA.
5. REPEAT OF NOTES ON LEAD FINITE PROPOSITION
Assuming that this remains the Lead Finite Proposition, it suggests a
number of very interesting weakenings to be investigated. Here are
some:
1. Modifying. the punch line.
1a. Removing "without {(8k)-1}!". Certainly provable in PRA, but EFA might
require some thought.
1b. Removing A-1. Should be provable in EFA.
2. Keeping the punch line. Changing n!.
The interesting thing is to make n! a function of k. The higher the
function of k that n is, the stronger the statement.
2a. Replace n! with k!!. Should be about Z_2.
2b. Replace n! with k!...!. r factorials, r outside quantifier Should
be about Z_r, where there are r factorials.
2c. Replace n! with k!...!, where there are k !'s. Should be around ZC.
2d. Ackerman function of k. Should be around ZFC.
2e. <epsilon_0 recursive functions of k. Should climb through the
Mahlo cardinal hierarchy.
2f. Probably one has some delicate low level stuff going through
fragments of PA.
But first let's see how long the Lead Finite Proposition lasts. As
usual, I think it will last forever (smile).
6. NOW WHAT?
To update https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
87. Mathematically Natural Concrete Incompleteness, June 21, 2015, 60
pages. Supersedes 1/15/15, 1/10/15, 1/13/15 versions.
incorporating these substantially improved statements. Will again have
proofs of the statements from large cardinals.
Then get a working manuscript of the reversal for Lead Proposition for
experts, to make sure that it implies Con(SRP), over RCA_0.
I have been exactly here before, but before doing the update, I saw
that I could do better, and the above sections 1-5 is the current
situation.
Let's see how I break the potentially infinite loop on this nearing 50
year effort.
**********************************************************
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 663rd 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
Harvey Friedman
More information about the FOM
mailing list