[FOM] 666: Pi01 Incompleteness/SRP,HUGE/10

Fri Mar 18 10:43:20 EDT 2016

We are in the process of sketching detailed proofs of the claims in

http://www.cs.nyu.edu/pipermail/fom/2016-March/019550.html

starting with the all important Lead Proposition. For the reader's
convenience, we copy the four statements from
http://www.cs.nyu.edu/pipermail/fom/2016-March/019550.html

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.

LEAD FINITE PROPOSITION. Every reflexive order invariant R containedin
N^2k has a fixed point minimizer f sending [n]!^k to some A^k
containedin dom(f) intersect dom(f)-1, without (8k)!-1. We can require
that f live below (8kn)!.

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.

LEAD FINITE HUGE PROPOSITION. Every reflexive order invariant R
containedin N^2k has a <= fixed point minimizer f sending [n]!^k to
some A^k containedin dom(f), with comparable nontrivial partial
embeddings f_j!...j!||<(j-1)!, 8k < j <= n. We can require that f live
below (8kn)!.

***************************

I have been focusing on the Lead Proposition. The reversal is very
delicate and being hard fought, and there have been some scary
moments. The fight continues. I have a nice new replacement for the
Lead Proposition in case something goes wrong. I am working with
rather small k,n, which I find very satisfying.

In the meantime, I found a very good way of talking about finite
approximations to maximal S^2 containedin V. I now view this new
finite form as the new LEAD FINITE PROPOSITION. This is, like the Lead
Proposition, at the level of SRP.

DEFINITION 1. The height of a rational p, H(p), is the maximum of the
magnitudes of the numerator and denominator in its reduced form
(standard). H(x), The height of x in Q^k, H(x), is
max(H(x_1),...,H(x_k)). The height of finite S containedin Q^k, H(S),
is the maximum of the H(x), x in S. S//r = {x in S: H(x) <= r}.

The notion of height of a rational is standard. I'm not sure that this
notion of height of a rational vector is standard. The results would
be the same if I used, e.g., the height of x as the sum of the heights
of the coordinates of x.

DEFINITION 2. Let V containedin Q^k. S^2 containedin V is k-maximal if
and only if there is no H(x) <= k with (S disjointunion {x})^2
containedin V.

(NEW) LEAD FINITE PROPOSITION. For all order invariant V containedin
Q[0,n]^k//(8kn)!, some k-maximal S^2 containedin V extends to a
#(S)-maximal S'^2 containedin V that is partially embedded by the
function p if p < 1; p+1 if p = 1,...,n-1.

Compare the above with

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.

The above is explicitly P01. It 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 666th 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

Harvey Friedman