[FOM] 645: Fixed Point Minimizers #1
Harvey Friedman
hmflogic at gmail.com
Sun Nov 22 19:46:03 EST 2015
THIS POSTING IS SELF CONTAINED
In http://www.cs.nyu.edu/pipermail/fom/2015-November/019350.html we
presented a reasonably unified
implicitly Pi01 corresponding to SRP
implicitly Pi01 corresponding to HUGE
explicitly Pi01 corresponding to SRP
explicitly Pi01 corresponding to HUGE
It was NOT done correctly and should be discarded. The fixes are not
as good as what we present HERE using a variant of our previous Fixed
Point Minimization.
So at this point here are the principal operational announcements for
Concrete Mathematical Incompleteness, starting with BRT:
1. Boolean Relation Theory. Implicitly Pi02 corresponding to SMAH. See
https://u.osu.edu/friedman.8/foundational-adventures/boolean-relation-theory-book/
This has been stable for some years.
2. Order invariant relations and maximal roots. Implicitly Pi01
corresponding to SRP. This has been stable for quite some time. See
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87
We prefer the following lead statement variant (stable for some time):
Every order invariant relation on Q^k has a nonnegatively maximal
root, where S[0...n-1]>n = S[1...n]>n.
3. Constrained subsets of N.
http://www.cs.nyu.edu/pipermail/fom/2015-November/019335.html
Implicitly and explicitly Pi01 corresponding to SRP. Implicitly and
explicitly Pi01 corresponding to SMAH. This uses (N,<,+) and multiple
passes.
4. Fixed Point Minimizers. Present posting. Implicitly/explicitly Pi01
corresponding to SRP/HUGE. All four combinations.
FIXED POINT MINIMIZERS #1
1. Fixed Point Minimizers - SRP
2. Fixed Point Minimizers - HUGE
3. Finitary Fixed Point Minimizers - SRP
4. Finitary Fixed Point Minimizers - HUGE
5. Lex Minimizers.
6. Templates.
1. FIXED POINT MINIMIZERS - SRP
DEFINITION 1.1. Q is the set of all rationals. We use n,m,r,s,t for positive
integers and p,q for rationals, unless indicated otherwise. x in Q^k
is positive if and only if all coordinates of x are > 0. For x,y in
Q^k, x <' y if and only if max(x) < max(y). For S
containedin Q^k,, S|<=p = S intersect (-infinity,p]^k. R is a relation
on Q^k if and only if R containedin Q^2k. x is related to y if and
only if x R y. Functions are treated as
relations.
DEFINITION 1.2. Let R be a relation on Q^k. A fixed point minimizer
for R is a function f:D^k into D^k, D containedin Q, where for all x R
x, f(x) is a fixed point of f related to x by R that is <' minimal
among the fixed points of f related to x by R.
DEFINITION 1.3. Let S containedin Q^k. An upper shift of S is a
subset of Q^k obtained by first fixing a coordinate p of an element of
S, and then adding 1 to all coordinates of elements of S that are >= p.
DEFINITION 1.4. x,y in Q^k are order equivalent if
and only if for all 1 <= i,j <= k, x_i < x_j iff y_i < y_j. E
containedin Q^k 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 containedin Q^2k is order invariant,
PROPOSITION 1.1. Every order invariant relation on Q^k has a fixed
point minimizer containing some upper shift.
THEOREM 1.2. Proposition 1.1 is provably equivalent to Con(SRP) over
WKL_0. There is a tiny k such that Proposition 1.1 for k is provably
equivalent to Con(SRP) over WKL_0.
SRP = ZFC + {there exists a cardinal with the k-SRP}_k.
The SRP hierarchy is intertwined with the subtle and the ineffable
cardinal hierarchies.
2. FIXED POINT MINIMIZERS - HUGE
DEFINITION 2.1. Let f:D^k into D^k, D containedin Q, and V containedin
Q^r. V is equational (in f) if and only if V is the set of solutions
to an equation in f and r variables, with constants from D. V is
initially equational (in f) if and only if each V|<=p, p in D, is
equational (in S).
PROPOSITION 2.1. Every not reflexive order invariant relation on Q^k has a fixed
point minimizer containing some initially equational upper shift.
DEFINITION 2.2. Let R be a relation on Q^k. A positive fixed point minimizer
for R is a function f:D^k into D^k, D containedin Q, where for
positive x R x, f(x) is a fixed point of f related to x by R that is
<' minimal among the fixed points of f related to x by R. A positive
upper shift of S containedin Q^k is a subset of Q^k obtained by first
fixing a coordinate p > 0 of an element of S, and then adding 1 to all
coordinates of elements of S that are >= p.
PROPOSITION 2.2. Every order invariant relation on Q^k has a positive fixed
point minimizer containing some initially equational (positive) upper shift.
THEOREM 2.3. Propositions 2.1 and (both forms of) Proposition 2.2 are
provably equivalent to Con(HUGE) over WKL_0. There is a tiny k such
that Propositions 2.1 and 2.2 for k are provably equivalent to
Con(HUGE) over WKL_0.
HUGE = ZFC + {there exists a nontrivial elementary embedding
j:V(lambda) into V(mu) such that j^(k)(kappa) exists}_k.
3. FINITARY FIXED POINT MINIMIZERS - SRP
DEFINITION 3.1.Let R be a relation on Q^k. A finitary fixed point minimizer
for R is a function f:S into S, S a finite subset of Q^k, where for x
R x, f(x) is a fixed point of f related to x by R that is <' minimal
among the fixed points of f related to x by R.
DEFINITION 3.2. For finite S containedin Q^k, ush(S) results from
S|<=k by adding 1 to all nonnegative coordinates of its elements.
We view ush(S) as a preferred kind of upper shift for finite S.
DEFINITION 3.3. f is k-full if and only if
i. f:S into S, for some finite S containedin Q^k.
ii. GEN(f,k) containedin S, where GEN(f,0) = {0,...,k}^k, and
GEN(f,i+1) is the least A^k containing GEN(f,i) union f[GEN(f,i)], 0
<= i <= k-1.
Thus we are treating 0,...,k as generators.
PROPOSITION 3.1. Every order invariant relation on Q^k has a k-full
finitary fixed point minimizer f containing ush(f).
Proposition 3.1 is obviously explicitly explicitly Pi02. Moreover, we
can put an obvious upper bound on the cardinality of f. This puts
Proposition 3.1 in explicitly Pi01 form using either the well known
decision procedure for (Q,<) or by directly upper bounding the
magnitudes of the numerators and denominators in the coordinates of
elements of S.
THEOREM 3.2. Proposition 3.1 is provably equivalent to Con(SRP) over EFA.
EFA = exponential function arithmetic.
4. FINITARY FIXED POINT MINIMIZERS - HUGE
DEFINITION 4.1.Let R be a relation on Q^k. A positive finitary fixed
point minimizer
for R is a function f:S into S, S a finite subset of Q^k, where for
positive x R x, f(x) is a fixed point of f related to x that is <'
minimal among the fixed points of f related to x.
DEFINITION 4.2. f is k*-full if and only if
i. f:S into S, for some finite S containedin Q^k.
ii. GEN(f,k) containedin S, where GEN(f,0) = {0,...,2k,k-+5}^k, and
GEN(f,i+1) is the least A^k containing GEN(f,i) union f[GEN(f,i)], 0
<= i <= 2k-1.
Thus we are treating 0,...,2k,k-+5 as generators.
PROPOSITION 4.1. Every order invariant relation on Q^k has a k*-full
finitary positive fixed point minimizer f containing ush(f), where
every defined f(k+.5,p,0,...,0) is (min(p+1,k),0,...,0).
Obviously Proposition 4.1 is explicitly Pi02. However, we
can easily upper bound the cardinality of the f, obtaining an
explicitly Pi01 form using the well known decision procedure for
(Q,<), or by directly bounding the numerators and denominators
involved.
THEOREM 4.2. Proposition 4.1 is provably equivalent to Con(HUGE) over
EFA. Proposition 4.1 for some fixed k is provably equivalent to
Con(HUGE) over EFA.
5. LEX MINIMIZERS
We can replace <' with the strict lexicographic ordering throughout,
and obtain the same results.
6. TEMPLATES
We now consider quantifier free sentences in fixed point minimizers.
TEMPLATE 6.1. Let phi be a propositional combination of sentences
F_i(p_1,...,p_k) rel q, F_i(p_1,...,p_k) rel F_j(q_1,...,q_k), where
p_1,...,p_k,q,q_1,...,q_k are rationals, and rel is among
<,<=,>,>=,=,not=. Every order invariant relation on Q^k has a fixed
point minimizer obeying phi.
Here we follow the convention that the sentences cited are
automatically false if at least one side is undefined.
THEOREM 6.2. Every instance of Template 6.1 is provable in SRP or
refutable in RCA_0. This is false for any SRP[k].
Note that we are not allowing nesting of the functions in Template
6.1. If we do allow nesting, then we believe that Theorem 6.2 still
holds.
**********************************************************
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 645th 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
637: Progress in Pi01 Incompleteness 1 10/25/15 8:45PM
638: Rigorous Formalization of Mathematics 2 10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2 10/27/15 10:38PM
640: Progress in Pi01 Incompleteness 3 10/30/15 2:30PM
641: Progress in Pi01 Incompleteness 4 10/31/15 8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1 11/3/15 11:57PM
644: Fixed Point Selectors 1 11/16/15 8:38AM
Harvey Friedman
More information about the FOM
mailing list