[FOM] 635: Fixed Point Minimization 2

Wed Oct 21 23:52:58 EDT 2015

We continue from http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html

It is arguably preferable to avoid the lexicographic minimization used
there in favor of the minimization of max(x).

Of course, the advantage of lexicographic minimization is that it is
deterministic, whereas minimization of max(x) is not. So it seems
important to have both versions.

Using minimization instead of lexicographic minimization is going to
add some MORE LAYERS to be checked.

What i want to do here is to restate all of the definitions. The
results are the same as before. There are also some small changes.

Note that what we called fixed point minimizers in
http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html are now
called lex fixed point minimizers. We reserve the old expression
"fixed point minimizers" for these new minimizers that minimize
max(x).

##############

We now give the altered definitions incorporating both minimizers and
lex minimizers. We omit the previous definitions that remain
unchanged, but still listed here. We also present the Templates taking
into account both kinds of minimizers. In the interest of brevity, the
Propositions and Theorems are not listed, as they are unchanged from
http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html and now
cover both kinds of minimizers. Also see that I now use non-decreasing
instead of non-increasing, which I like better. I had fooled myself
into thinking that I needed to use non-increasing. Actually, either
can be used.

DEFINITION 1.3. Let R be a relation on Q^k. A fixed point minimizer
for R is a function f:D^k into D^k, 0 in D containedin Q, where each
f(x) is a fixed point of f related to x, where no fixed y of f related
to x has max(y) < max(x). A lex fixed point minimizer for R is a
function f:D^k into D^k, 0 in D containedin Q, where each f(x) is the
lexicographically least fixed point of f related to x.

Accordingly, we  restate one of the implicitly Pi01 HUGE cardinal
statements, and also the explicitly Pi01 HUGE cardinal statement.

DEFINITION 3.1. x in Q^k is non-decreasing if and only if x_1 <= ... <= x_k.

DEFINITION 3.2. Let R be a relation on Q^k. A fixed point <= minimizer
for R is an f:D^k into D^k, 0 in D containedin Q, where each f(x), x
non-decreasing, is a fixed point of f related to x, where no fixed
point y of f related to x has max(y) < max(x).

DEFINITION 3.3. Let R be a relation on Q^k. A lex fixed point <=
minimizer for R is an f:D^k into D^k, 0 in D containedin Q, where each
f(x), x
non-decreasing, is the lexicographically least fixed point of f related to x.

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

TEMPLATE A. Let H:Q^2k into Q^2k be definable in (Q,<)  - i.e., order
theoretic. Every reflexive order invariant relation on Q^k has a (lex) fixed
point minimizer closed under H.

TEMPLATE B. Let H:Q^2k into Q^2k be definable in (Q,<) - i.e., order
theoretic. Every reflexive order invariant relation on Q^k has a (lex) fixed
point <= minimizer closed under H.

TEMPLATE C. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
reflexive order invariant relation on Q^k has a (lex) fixed point minimizer
closed under H.

TEMPLATE D. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
reflexive order invariant relation on Q^k has a (lex) fixed point <=
minimizer closed under H.

DEFINITION 5.2. Let R be a relation on Q^k and E containedin Q . An E
fixed point minimizer for R is a function f:D^k into D^k, 0 in D
containedin Q^k, where f(x) is a fixed point of f related to x, where
no fixed point y of f related to x has max(y) < max(x). An E fixed
point
<= minimizer for R is a function f:D^k into D^k, 0 in D containedin
Q^k, where f(x) is a fixed point of f related to x, where no fixed
point y of f related to x has max(y) < max(x).

DEFINITION 5.3. Let R be a relation on Q^k and E containedin Q. An E
lex fixed point minimizer for R is a function f:D^k into D^k, 0 in D
containedin Q^k, where f(x) is the lexicographically least fixed point
of f related to x, provided x in pi(f[E^k]). An E lex fixed point
<= minimizer for R is a function f:D^k into D^k, 0 in D containedin
Q^k, where f(x) is the lexicographically least fixed point of f
related to x, provided x in pi(f[E^k]) is non-decreasing.

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

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

Harvey Friedman