[FOM] 636: Fixed Point Minimization 3
Harvey Friedman
hmflogic at gmail.com
Thu Oct 22 17:49:02 EDT 2015
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
More information about the FOM
mailing list