[FOM] 637: Progress in Pi01 Incompleteness 1

Sun Oct 25 20:45:58 EDT 2015

SUMMARY OF WHERE WE ARE WITH Pi01 INCOMPLETENESS.

1. Order invariant relations and maximal roots. This yields implicitly
Pi01 for SRP. Uses order invariant relations.See
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87 The very first sentence of the Abstract is the lead statement:

Every order invariant R containedin Q^2k has a maximal nonnegative
root, where S[1...n]>n = S[0...n-1]>n.

We prefer a slight change in the presentation.

Every order invariant relation on Q^k has a nonnegatively maximal
root, where S[0...n-1]>n = S[1...n]>n.

I have taken the position that relations are not going to be as good
as functions for generating explicitly Pi01 sentences, or for getting
to HUGE. This could change, but that has been my position for some
time. Hence we have 2-3 below. However, there are other benefits of
moving to functions, such as EQUATIONAL PUNCH LINES, which can be
easily tweaked to get up through HUGE.

2. Constrained Function Theory.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019253.html Here we
use PUD (purely universally definable) sets of partial functions, and
get implicitly Pi01 for SRP. The idea here is that any PUD set of
partial functions with an extension property (it's an r.e. condition)
has a very good element (satisfying certain equations). We now prefer
the punch line equation f(ush(x)) = ush(f(x)). Here ush is the upper
shift, which is adding 1 to all nonnegative coordinates.  (Punch line
has, e.g., f:D^k into D^k, 0 in D, with this equation).

3. Fixed Point Minimization.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019264.html Here we
obtain implicitly Pi01 for SRP and for HUGE. We also get explicitly
Pi01 for SRP and HUGE. Uses order invariant relations only, and not
PUD. Here the key idea is the natural notion of a fixed point
minimizer for a relation. The preferred statements read that every
reflexive order invariant relation has a fixed point minimizer with
f(ush(x)) = ush(f(x)). We also weaken the notion of minimizer and
essentially strengthen the equation to get to HUGE. This approach also
lends itself to explicitly Pi01, by weakening the requirement for
fixed point minimizers to involve tuples readily built from the
"generators" 0,...,k (and 0,...,k,k+.5).

NOTE: Again I tried to be too cute and combine into one triple
equation. That works for the lex case but not the plain case. In any
case, I now prefer to simply have two equations. The first equation is
f(ush(x)) = ush(f(x)), where ush is the upper shift. This is also my
preferred equation for the SRP version, where we don't have any second
equation. It is important also to have an order theoretic equation,
for this, I now find it best to use "reductions" of the upper shift
which are order theoretic. A reduction here is obtained by making a
function the identity at any desired places. Thus we maintain
unguarded equations, which we prefer.

For the second equation in the HUGE statements, we again prefer
unguarded equations. f(k+.5,p,0,...,0) = (min(k,p+1),0,...,0). There
is a slight problem about the case k <= 2, which may cause me to set
things up a little differently, but this is a minor point.

I think there is room for a new really good idea for combining these
equations or somehow make the pair of these equations nicer. However,
even as they stand now, they suggest a lot of Templating projects at
the HUGE level.

I didn't go to HUGE with approach 2, nor did I go to explicitly Pi01.
It looks like the same moves I am making in approach 3 will also work
for approach 2.

I see various advantages and disadvantages to 2 versus 3. And within
3, using, or not using, lex.

4. Various unexpected difficulties arose in connection with the
upgrade approaches, and that is now put on permanent hold, in favor of
2,3 above.

5. The TEMPLATING is working very well, but we have not had the time
to confirm some complete analyses of some very natural templates. The
Templates that we have or expect to have complete analyses of, are for
2,3 as they relate to SRP. Complete analyses of Templates relating to
HUGE is something we have not begun to tackle. We have also claimed a
rather strong complete analysis of templating for 1.

6. After postings in this series covering 1-3,5 settle down
reasonably, I will upgrade
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87 covering these new developments as well as the previously covered
1. The 1) part will also include from
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87 the step maximal roots for order invariant relations on Q^k.

7. In the works. using subsets of N and addition. This represents the
FIRST TIME I am in serious communication with a strong mathematician
way outside mathematical logic who is actually wrapping his head
around various specific versions of PI01 incompleteness - in the realm
of subsets of N and addition. There are rough connections with some
mathematical physics that is currently being explored with this expert
in mathematical physics. This is definitely going somewhere, but not
at all clear just how far this is going to go.

8. After 6, and some settling down on 7, I will then go into proof
checking and proof writing mode. You will then see a lot more SILENCE.
2016 looks to be the year for this.

9. In this "progress" series, we will make individual postings on the
above items, one at a time, in preparation for the new manuscript 6.

**********************************************************
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 637th 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

Harvey Friedman