[FOM] 644: Fixed Point Selectors 1

Mon Nov 16 08:38:29 EST 2015

THIS POSTING IS SELF CONTAINED

We have found another closely related approach which has significant
advantages over earlier approaches. Specifically, the transitions from
the implicitly Pi01 SRP statements to the other three kinds: the
implicitly Pi01 HUGE statements, the explicitly Pi01 SRP statements,
and the explicitly Pi01 HUGE statements, are very smooth. This is
definitely a feature I have been seeking, in some form or other, since
1967.

How does this fit into the current inventory of Concrete Mathematical
Incompleteness, starting with BRT, which is implicitly Pi02?

https://u.osu.edu/friedman.8/foundational-adventures/boolean-relation-theory-book/
http://www.cs.nyu.edu/pipermail/fom/2015-October/019279.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019304.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019325.html
http://www.cs.nyu.edu/pipermail/fom/2015-October/019327.html
http://www.cs.nyu.edu/pipermail/fom/2015-November/019335.html

It is a too early to be discarding earlier approaches until we assess
the new Fixed Point Selection approach.

FIXED POINT SELECTORS 1
by
Harvey M. Friedman
November 16, 2015

1. Fixed point selectors.
2. Finitary fixed point selectors.

1. FIXED POINT SELECTORS

DEFINITION 1.1. Q,Z+,N is the set of all rationals, positive integers,
nonnegative integers, respectively. We use n,m,r,s,t for positive
integers and p,q for rationals, unless indicated otherwise. 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
sets of ordered pairs.

DEFINITION 1.2. 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,

DEFINITION 1.3. Let R be a relation on Q^k. A fixed point selector
for R is a function f:D^k into D^k, D containedin Q, where each
f(x) is a fixed point related to x with strictly smaller first
coordinate, provided this exists.

DEFINITION 1.4. Let S containedin Q^k. An upper shift of S is the
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.

PROPOSITION 1.1. Every order invariant relation on Q^k has a fixed
point selector containing some upper shift.

DEFINITION 1.5. Let S containedin Q^k. V containedin Q^r is
conjunctive (relative to S) if and only if V is the set of solutions
to some finite set of statements S(x_1,...,x_k), where each x_i is
among the variables v_1,...,v_r, or is a constant from Q. V
containedin Q^n is initially conjunctive if and only if each V|<=p is
conjunctive.

PROPOSITION 1.2. Every order invariant relation on Q^k has a fixed
point selector containing some initially conjunctive upper shift.

THEOREM 1.3. 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. Proposition 1.2 is provably
equivalent to Con(HUGE) over WKL_0. There is a tiny k such that
Proposition 1.2 is provably equivalent to Con(HUGE) over WKL_0.

SRP = ZFC + {there exists a strongly k-Mahlo cardinal}_k.

The SRP hierarchy is intertwined with the subtle and the ineffable
cardinal hierarchies.

HUGE = ZFC + {there exists a nontrivial elementary embedding
j:V(lambda) into V(mu) such that j^(k)(kappa) exists}_k.

2. FINITARY FIXED POINT SELECTORS

DEFINITION 2.1. A finitary system is an (f,k,n;p_1,...,p_m), where
i. f:D^k into Q^k, where D containedin Q is finite.
ii. p_1 < ... < p_m are rationals.
iii. D includes all values of expressions involving at most n
occurrences of the k coordinate functions of f and constants
p_1,...,p_m in Q.

It is sometimes convenient to identify (f,k,n;p_1,...,p_m) with f.

DEFINITION 2.2. Let R be a relation on Q^k. A finitary fixed point
selector for R is a finitary system (f,k,n;p_1,...,p_m), where each
f(x) is a fixed point related to x with strictly smaller first
coordinate, provided this exists.

DEFINITION 2.3. Let (f,k,n;p_1,...,p_m) be a finitary system. Its 0
upper shift is the result of adding 1 to all nonnegative coordinates
of the x in graph(f)|<=p_m.

PROPOSITION 2.1. Every order invariant relation on Q^k has a finitary
fixed point selector (f,k,n;0,...,m) containing its 0 upper shift.

DEFINITION 2.4. E containedin Q^r is conjunctive <= p if and only if
E|<=p is the set of solutions to some set of statements (x_1,...,x_2k)
in graph(f), where each x_i is among the variables v_1,...,v_r or a
constant among p_1,...,p_m.

PROPOSITION 2.2. Every order invariant relation on Q^k has a finitary
fixed point selector (f,k,n;0,...,m,m+.5) containing its 0 upper
shift, which is conjunctive <= m.

Obviously Propositions 2.1 and 2.2 are explicitly Pi02. However, we
can easily upper bound the cardinality of the selector, obtaining an
explicitly Pi01 form using the well known decision procedure for
(Q,<), or by directly bounding the numerators and denominators
involved.

THEOREM 2.3. Proposition 2.1 is provably equivalent to Con(SRP) over
EFA. Proposition 2.1 for some fixed k,m is provably equivalent to
Con(SRP) over EFA. Proposition 2.2 is provably equivalent to Con(HUGE)
over EFA. Proposition 2.2 for some fixed k 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 644th 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

Harvey Friedman