[FOM] 636: Fixed Point Minimization 3

[Harvey Friedman]

In http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html and
http://www.cs.nyu.edu/pipermail/fom/2015-October/019262.html

we tried to be too cute in the HUGE statements, and use an incorrect
simplification of f(ush(x)) = ush(f(x)) for the first of two
equations. I.e., we wrote

for all blah blah blah there exists a blah blah blah where
i. f(x+1) = f(x)+1, min(x) >= 0.
ii. f(k+.5,x) = (k+.5,x+1), (0,x) in dom(f)|<=k-1.

The guard min(x) >= 0 has to also apply to f(x), and so this can be
fixed, say, by

i. f(x+1) = f(x)+1, min(x,f(x)) >= 0.
ii. f(k+.5,x) = (k+.5,x+1), (0,x) in dom(f)|<=k-1.

I now prefer no guard at all, as an intermediate step to a new
combination of the two equations, resulting in a single guarded
equation, with the guard on the argument and not on the value.

This intermediate form, which has its merits, reads

i. f(ush(x)) = ush(f(x).
ii. f(k+.5,x) = (k+.5,x+1), (0,x) in dom(f)|<=k-1.

The final form,

f(ush(0,x)) = ush(f(0,x)) = f(k+.5,x), (0,x) in dom(f)|<=k-2.

Recall that ush is the upper shift, which is the result of adding 1 to
all nonnegative coordinates.

So we have

IMPLICITLY Pi01 HUGE. Every reflexive order invariant relation on Q^k
has a fixed point <= minimizer, where
f(ush(0,x)) = ush(f(0,x)) = f(k+.5,x), (0,x) in dom(f)|<=k-2.

EXPLICITLY Pi01 HUGE. Every reflexive order invariant relation on Q^k has a
{0,...,k,k+.5} finite fixed point <= minimizer, where
f(ush(0,x)) = ush(f(0,x)) = f(k+.5,x), (0,x) in dom(f)|<=k-2.

For comparison, we have

IMPLICITLY Pi01 SRP. Every reflexive order invariant relation on Q^k
has a fixed point minimizer, where f(ush(x)) = ush(f(x)).

EXPLICITLY Pi01 SRP. Every reflexive order invariant relation on Q^k has a
{0,...,k,k+.5} finite fixed point minimizer, where f(ush(x)) =
ush(f(x)), max(x) <= k.

In all four, we can use as a variant, "... lex fixed point ..."
instead of "... fixed point ...". In the last two, we can also add
"<=" like we have in the first two.

Assuming the Fixed Point Minimization 1-3 development remains stable
for a little while, I will make a comprehensive restatement
consolidating all of the changes.

So at present, two developments are in play in Pi01 Incompleteness:

1. Maximal roots in Q[0,n]^k.
2. Fixed point minimizers in Q^k.

For explicitly Pi01, and for HUGE, and for both together, only 2 is in play.

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

Harvey Friedman