[FOM] 634: Fixed Point Minimization 1

[Harvey Friedman]

THIS POSTING IS SELF CONTAINED

Fixed Point Minimization presented here may look like it is very different
from all my previous attempts to move to functions, but having worked
on Concrete Incompleteness virtually nonstop since 1967, I see that
everything is related to everything else.

Recall that I am trying to move from the previous relation stuff

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

to functions for two reasons. One is to get better explicitly Pi01. The
other is to get better HUGE. And of course hopefully both at once:
really good explicitly Pi01 corresponding to HUGE.

Well, this now looks like it is happening. Of course, There are now
many new things that need more rounds of checking.

It looks like things may well be at last stabilizing, with Proposition
A for relations, and implicitly Pi01, and the below for functions,
implicitly Pi01, explicitly Pi01, HUGE, and both.

There is one more avenue that I would like to follow, before getting
immersed in checking/writing. Right now, I am in several dimensions
and only order. I need to look at sets of nonnegative integers (i.e.,
one dimension) with addition. This is needed for continued discussions
with a colleague who senses some possible connections with
mathematical physics.

FIXED POINT MINIMIZATION 1
by
Harvey Friedman
October 19, 2015

1. FIXED POINT MINIMIZERS

DEFINITIION 1.1. Q,Z+,N is the set of all rationals, positive
integers, nonnegative integers, respectively. We use p,q,x,y,z for
rationals and tuple of rationals, and k,n,m,r,s,t for positive
integers, unless indicated otherwise.

DEFINITION 1.2. A relation on Q^k is an R containedin Q^2k. Let R be a
relation on Q^k. R is reflexive if and only if each x R x. .x is
related to y if and only if x R y.

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 the lexicographically least fixed point of f that is related
to x.

THEOREM 1.1. Let 0 in D containedin Q be well ordered. Every reflexive
relation on Q^k has a unique fixed point minimizer with domain D^k.

DEFINITION 1.4. Let x,y in Q^k and E containedin Q^k. x,y are order
equivalent if and only if for all 1 <= i,j <= k, x_i < x_j iff y_i <
y_j. E is order invariant if and only if for all order equivalent x,y
in Q^k, x in E iff y in E. R is an order invariant relation on Q^k if
and only if R is an order invariant subset of Q^2k. E|<=p = E
intersection {x in Q^k: max(x) <= p}.

DEFINITION 1.5. Let x,y in Q^k. min(1,x) = (min(1,x_1),...,min(1,x_k)).

PROPOSITION 1.1. Every reflexive order invariant relation on Q^k has a
fixed point minimizer with min(1,f(1,...,k)) = min(1,f(2,...,k+1)).

It is easily seen that Proposition 1.1 is implicitly Pi01 via the
Goedel Completeness Theorem. The argument for this also shows that the
fixed point minimization can be taken to have a certain level of
concreteness.

THEOREM 1.2. (WKL_0). In Proposition 1.1, if the given relation has
such a fixed point minimizer then it has such a fixed point minimizer
that is delta-0-2 in the sense of recursion theory.

THEOREM 1.3. Propositions 1.1, 1.2 are provably equivalent to Con(SRP) over
WKL_0. For fixed k, Propositions 1.1, 1.2 are provable in SRP. For small
fixed k, Propositions 1.1, 1.2 are independent of ZFC, assuming Con(SRP). These
results hold if we require that f be delta-0-2 in the sense of
recursion theory.

For this new statement, I expect to be able to make exact calculations
of the strength for any fixed k. Such exact calculations are
incomparably more difficult for Proposition A.

SRP is ZFC + {there exists a limit ordinal with the k-stationary Ramsey
property}_k. SRP+ = ZFC + (forall n)(therexists a limit ordinal with
the k-stationary Ramsey property).

NOTE: This is the same if we use k-subtle or k-ineffable.

2. UPPER SHIFT

DEFINITION 2.1. The upper shift, ush:Q^k into Q^k, is defined as
follows. ush(x) is the result of adding 1 to all nonnegative
coordinates of x.

PROPOSITION 2.1. Every reflexive order invariant relation on Q^k has a
fixed point minimizer with f(ush(x)) = ush(f(x)).

Although Proposition 2.1 is implicitly Pi01, there is a problem seeing
this via the Goedel Completeness Theorem. We can fix this as follows.

PROPOSITION 2.2. Every reflexive order invariant relation on Q^k has a
fixed point minimizer with f(ush(x)) = ush(f(x)), x in dom(f)|<=k.

THEOREM 2.3. (WKL_0). The following can be seen via the Goedel
Completeness Theorem. Proposition 2.2 is implicitly Pi01. In
Proposition 2.2, if the given relation has such a fixed point
minimizer then it has such a fixed point minimizer that is delta-0-2
in the sense of recursion theory.

THEOREM 2.4. Propositions 2.1, 2.2 are provably equivalent to Con(SRP) over
WKL_0. This is also the case for any fixed k that is not tiny. These
results hold if we require that f be delta-0-2 in the sense of
recursion theory.

3. HUGE CARDINALS

DEFINITION 3.1. x in Q^k is non-increasing 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-increasing, is the lexicographically least fixed point of f that
is related to x.

THEOREM 3.1. If we restate Propositions 1.1, 1.2, 2.1, 2.2 with fixed
point >= minimizers instead of fixed point minimizers, then the same
results hold.

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

Although Proposition34.2 is implicitly Pi01, there is a problem seeing
this via the Goedel Completeness Theorem. We can fix this as follows.

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

THEOREM 3.4. (WKL_0). The following can be seen via the Goedel
Completeness Theorem. Proposition 3.3 is implicitly Pi01. In
Proposition 3.3, if the given relation has such a fixed point
minimizer then it has such a fixed point minimizer that is delta-0-2
in the sense of recursion theory.

THEOREM 3.5. Propositions .3.2, 3.3 are provably equivalent to
Con(HUGE) over WKL_0. This holds if we require that f be delta-0-2 in
the sense of recursion theory.

4. TEMPLATES

We first consider Proposition 1.1, which takes the form

PROPOSITION 1.1. Every reflexive order invariant relation on Q^k has a
fixed point minimizer with a condition.

 The particular condition  is

min(1,f(1,...,k)) = min(1,f(2,...,k+1)).

There are several kinds of templating that we consider.

a. Vector equations where the dimension is the variable k, using min
and max. Single or finitely many. No nesting of f.
b. Equations with specific k, using min and max. Single or finitely
many. No nesting of f.
c. Vector inequalities where the dimension is the variable k, with no
min and max. Single or finitely many. No nesting of f.
d. Inequalities with specific k, with no min and max. Single or
finitely many. No nesting of f.
e. Closure of the graph of f under an order theoretic function
(specific k's). Single or finitely many.

For further developments, we particularly like to use e).

Recall that the order theoretic sets are those definable over (Q,<)
with constants allowed. By quantifier elimination, these are just
Boolean combinations of inequalities between variables, with constants
allowed.

DEFINITION 4.1. Let E containedin Q^k and H:Q^k into Q^k. E is closed
under H if and only if for all x in E, H(x) in E. We treat functions
as graphs.

However, our equation

min(1,f(1,...,k)) = min(1,f(2,...,k+1))

is not quite covered by e). Instead, the condition

f(1,...,k) < 1 implies f(1,...,k) = f(2,...,k+1)

can be used to climb the SRP hierarchy, and it is equivalent to
closure under H:Q^2k into Q^2k where

H(x) = (2,...,k+1,x_k+1,...,x_2k) if (x_1,...,x_k) = (1,...,k) and
x_k+1,...,x_2k < 1; x otherwise.

Focusing on e) leads to these four Templates.

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 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 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 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 fixed point >=
minimizer closed under H.

We have seen that a variant of Proposition 1.1 falls under Template A.
We also have variants falling under Template B (see Theorem 3.1). It
is clear that Proposition 2.1, 2.2 fall under Template C. Propositions
3.2, 3.3 fall under Template D.

Thus we have shown that Templates A,B,C climb through at least the SRP
hierarchy, and Template D climbs through at least the HUGE hierarchy.

CONJECTURE. Every instance of Templates A,B,C is either provable in SRP
or refutable in RCA_0. If provable in SRP then provable in WKL_0 +
Con(SRP).

CONJECTURE. Every instance of Template 5.3 is provable in ZFC +
j:V(kappa + 1) into V(kappa + 1) or refutable in RCA_0.

5. FINITE FUNCTIONS

DEFINITION 5.1. Let V containedin Q^k. pi(V) is the set of all
permutations of elements of V.

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 the lexicographically least fixed point
of f that is related to x, provided x in pi(f[E^k]). 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 the lexicographically least fixed point of f that
is related to x, provided x in pi(f[E^k]) is non-increasing.

PROPOSITION 5.1.  Every reflexive order invariant relation on Q^k has
a {0,...,k} finite fixed point minimizer with min(1,f(1,...,k)) =
min(1,f(2,...,k+1)).

PROPOSITION 5.2.  Every reflexive order invariant relation on Q^k has
a {0,...,k} finite fixed point minimizer whose <=k composites with
f(ush(x)) = ush(f(x)), max(x) <= k.

There is an obvious a priori upper bound on the size of D. Since the
statement is purely order theoretic in parameters 1,...,k+1, we can in
fact a priori upper bound the numerators and denominators used in D.
Alternatively, we can move the entire statement into the positive
integers, and use another arithmetic progression instead of 1,...,k+1.
These considerations put Propositions 4.1, 4.2 in explicitly Pi01 form.

THEOREM 5.3. Propositions 5.1, 5.2 are provably equivalent to Con(SRP) over EFA.

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

The same considerations put Proposition 5.4 in explicitly Pi01 form.

THEOREM 5.5. Proposition 5.4 is provably equivalent to Con(HUGE) 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 634th 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

Harvey Friedman