[FOM] 641: Progress in Pi01 Incompleteness 4
Harvey Friedman
hmflogic at gmail.com
Sat Oct 31 20:12:06 EDT 2015
#640 http://www.cs.nyu.edu/pipermail/fom/2015-October/019325.html
focused on Constrained Function Theory, which is second on the list of
3 (see below for 1-3).
Here we focus on the third - Fixed Point Minimization. In addition to
penetrating HUGE, it also lends itself naturally to a general method
for obtaining explicitly Pi01 sentences from implicitly Pi01
sentences.
This - at least for the moment - concludes the Concrete Incompleteness
that lives in (Q,<) and (Q,<,+1). I.e., the series Progress in Pi01
Incompleteness 1-4, with the previous
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
We now plan to correspondingly upgrade the existing
Mathematically Natural Concrete Incompleteness, June 21, 2015, 60 pages
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87
with the developments in these four postings, and put it on that site.
The resulting paper will be fairly complete for the positive
directions of the results claimed in this Progress series.
Then we will mostly be focused on writing complete proofs of the
reversals, to appear as a book. Then we will have two books on
Concrete Incompleteness - Boolean Relation Theory and this new one.
As proofs are written, we expect most of the claims to be sharpened in
natural worthwhile ways. Thus in these Progress series, I did not
write down the strongest claims that I expect to be able to prove.
I am in some preliminary discussions with an expert in mathematical
physics concerning some Concrete Incompleteness in (N,<,+). We are at
the point where the statements are being absorbed, and there is some
back and forth about ways of modifying them to resonate more from the
point of view of mathematical physics. At this point, it is not at all
clear how far this will go.
#############################
To orient the reader, I again give a highly abridged version of
http://www.cs.nyu.edu/pipermail/fom/2015-October/019279.html
1. Order invariant relations and maximal roots. This yields implicitly
Pi01 for SRP. Uses order invariant relations.See
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#87
2. Constrained Function Theory.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019253.html Here we
use PUD (purely universally definable) sets of partial functions, and
get implicitly Pi01 for SRP. The idea here is that any PUD set of
partial functions with an extension property (it's an r.e. condition)
has a very good element (satisfying certain equation).
3. Fixed Point Minimization.
http://www.cs.nyu.edu/pipermail/fom/2015-October/019264.html Here we
obtain implicitly Pi01 for SRP and for HUGE. We also get explicitly
Pi01 for SRP and HUGE. Uses order invariant relations only, and not
PUD. Here the key idea is the natural notion of a fixed point
minimizer for a relation.
#################################
FIXED POINT MINIMIZATION
by
Harvey M. Friedman
October 31, 2015
1. Fixed point minimizers
2. Guarded fixed point minimizers
3. Lexicographic ordering
4. Embeddings
5. Explicitly Pi01
1. FIXED POINT MINIMIZERS
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 E
containedin Q^k, E|<p, E|<=p, E|>p, E|>=p is the set of all x in E
such that max(x) is <p, <=p, >p, >=p, respectively. x in Q^k is
nondecreasing if and only if x_1 <= ... <= x_k. The upper shift ush(x)
of x in Q^k results from adding 1 to all nonnegative coordinates of x.
DEFINITION 1.2. 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. R is reflexive if and
only if for all x in Q^k, x R x. 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 minimizer
for R is a function f:D^k into D^k, 0 in D containedin Q, where each
f(x) is a minimal fixed point related to x. I.e.,
i. f(x) is a fixed point of f related to x.
ii. There is no fixed point y of f related to x with max(y) < max(x).
THEOREM 1.1. If R is a reflexive relation on Q^k and 0 in D
containedin Q is well ordered, then R has a fixed point minimizer
f:D^k into D^k.
PROPOSITION 1.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).
THEOREM 1.3. Proposition 1.2 is provably equivalent to Con(SRP) over
WKL_0. For some tiny fixed k, Proposition 1.2 is provably equivalent
to Con(SRP) over WKL_0.
SRP = ZFC + {there exists a cardinal with the k-SRP}_k. SRP+ = ZFC +
(for all k there exists a cardinal with the k-SRP).
The SRP hierarchy of large cardinals is intertwined with the subtle
and ineffable cardinal hierarchies.
2. GUARDED FIXED POINT MINIMIZERS
In guarded fixed point minimizers, instead of requiring that the
condition apply to all x, we only require that it applies to
nondecreasing x.
DEFINITION 2.1. Let R be a relation on Q^k. A guarded fixed point
minimizer for R is a function f:D^k into D^k, 0 in D containedin Q,
where each f(x) , x nondecreasing, is a minimal fixed point related to
x.
PROPOSITION 2.1. Every reflexive order invariant relation on Q^k has a
guarded fixed point minimizer with f(ush(x)) = ush(f(x)), x in dom(f).
PROPOSITION 2.2. Every reflexive order invariant relation on Q^k has a
guarded fixed point minimizer f:D^k into D^k with
i. f(ush(x)) = ush(f(x)), x in D^k.
ii. f(k+.5,p,...,p) = (p+1,...,p+1), p in D|<=k-1.
THEOREM 2.3. Proposition 2.1 is provably equivalent to Con(SRP) over
WKL_0. For some tiny fixed k, Proposition 2.1 is provably equivalent
to Con(SRP) over WKL_0.
THEOREM 2.4. Proposition 2.2 is provably equivalent to Con(HUGE) over
WKL_0. For fixed k, Proposition 2.2 is provable in HUGE.
HUGE = ZFC + {there exists a nontrivial elementary embedding
j:V(lambda) into V(mu) such that j^(k)(kappa) exists}_k.
3. LEXICOGRAPHIC ORDERING
There is a variant of the development in sections 1,2, which uses the
lexicographic ordering on Q^k. This brings in some determinism.
DEFINITION 3.1. Let R be a relation on Q^k. 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 lex least fixed point related to x. A guarded
lex fixed point minimizer for R is a function f:D^k into D^k, 0 in D
containedin Q, where each f(x), x nondecreasing, is the lex least
fixed point related to x.
THEOREM 3.1. If R is a reflexive relation on Q^k and 0 in D
containedin Q is well ordered, then R has a unique lex fixed point
minimizer f:D^k into D^k.
PROPOSITION 3.2. Every reflexive order invariant relation on Q^k has a
lex fixed point minimizer with f(ush(x)) = ush(f(x)), x in dom(f).
PROPOSITION 3.3. Every reflexive order invariant relation on Q^k has a
guarded lex fixed point minimizer with f(ush(x)) = ush(f(x)), x in
dom(f).
PROPOSITION 3.4. Every reflexive order invariant relation on Q^k has a
guarded lex fixed point minimizer f:D^k into D^k with
i. f(ush(x)) = ush(f(x)), x in D^k..
ii. f(k+.5,p,...,p) = (p+1,...,p+1), p in D|<=k-1.
THEOREM 3.5. Propositions 3.2 and 3.3 are provably equivalent to Con(SRP) over
WKL_0. For some tiny fixed k, Propositions 3.2 and 3.3 are provably equivalent
to Con(SRP) over WKL_0.
THEOREM 3.6. Proposition 3.4 is provably equivalent to Con(HUGE) over
WKL_0. For fixed k, Proposition 3.4 is provable in HUGE.
4. EMBEDDINGS
DEFINITION 4.1. Let E containedin Q^k. E is order theoretic if and
only if E can be defined by a propositional combination of
inequalities between variables x_1,...,x_k and constants from Q. h is
an embedding of E if and only if h:Q into Q is partial, and for all x,hx in Q^k,
x in E iff hx in E. Here h acts coordinatewise. All functions are
treated as sets of ordered pairs.
TEMPLATE 4.1. Let partial h:Q into Q be order theoretic (piecewise
linear with rational coefficients, finitely many pieces). Every
reflexive order invariant relation on Q^k has an h embedded (lex)
fixed point minimizer.
TEMPLATE 4.2. Let partial h:Q into Q be order theoretic (piecewise
linear with rational coefficients, finitely many pieces). Every
reflexive order invariant relation on Q^k has an h embedded guarded
(lex) fixed point minimizer.
There are some more ambitious multiple forms of these Templates.
TEMPLATE 4.3. Let partial h_1,...,h_r:Q into Q be order theoretic
(piecewise linear with rational coefficients, finitely many pieces).
Every reflexive order invariant relation on Q^k has an h_1,...,h_r
embedded (lex) fixed point minimizer.
TEMPLATE 4.4. Let partial h:Q into Q be order theoretic (piecewise
linear with rational coefficients, finitely many pieces). Every
reflexive order invariant relation on Q^k has an h_1,...,h_r embedded
guarded (lex) fixed point minimizer.
CONJECTURE 4.5. Every instance of Templates 4.1 - 4.4 with order
theoretic is provable in SRP or refutable in RCA_0. Every instance of
Templates 4.1 and 4.3 with piecewise linear is provable in SRP+ or
refutable in RCA_0. Every instance of Templates 4.2 and 4.4 with
piecewise linear is provable in ZFC + j:V(lambda+1) into V(lambda+1)
or refutable in RCA_0.
We have only done some preliminary research on this Conjecture. Here's
what we know now.
1. Templates 4.1 - 4.4 with order theoretic reach Con(SRP) over WKL_0, at least.
2. Templates 4.2 and 4.4 with piecewise linear climb through the HUGE
hierarchy, at least.
3. For Template 4.1 with order theoretic, Conjecture 4.5 holds. I.e.,
every instance is provable in SRP or refutable in RCA_0.
5. EXPLICITLY Pi01
The conclusion of all of the statements in sections 1-4 asserts that
there is an f:D^k into D^k with a purely universal property in
(Q,<,0), (Q,<,0,+1), or (Q,<,0,k+.5,+1). If we simply require that
f:D^k into D^k be finite, then of course we obtain explicitly Pi02
forms - and explicitly Pi01 forms if we bound the cardinality of D.
But the statements become refutable in EFA.
Instead, we ask for a partial f:Q^k into Q^k that is a finite
approximation to some actual f:D^k into D^k. This is defined as
follows.
DEFINITION 5.1. Let E containedin Q. An (E;t) generated function is a
partial f:Q^k into Q^k whose domain is the set of values of the
expressions that use at most t occurrences of +1 and the coordinate
functions of f, and constants from E.
Note that if E is finite then all (E;t) generated functions are
finite, with an obvious upper bound on the cardinality of the domain.
We assume that we have written the conclusions of the Propositions in
sections 1-4 in purely universal form in (Q,<,0), (Q,<,0,+1), or
(Q,<,0,k+.5,+1). See PUD in
http://www.cs.nyu.edu/pipermail/fom/2015-October/019325.html
THEOREM 5.1. If we modify the Propositions in sections 1-4
corresponding to SRP by requiring (0;t) generated f, with the
equations holding when both sides are defined, then the same results
hold. If we modify of the Propositions in sections 1-4 corresponding
to HUGE by requiring (0,k+.5;t) generated f, with the equations
holding when both sides are defined, then the same results hold.
Thus we are using a very general method for obtaining explicitly Pi01
sentences from implicitly Pi01 sentences. That this method yields
explicitly Pi01 sentences can be seen in two ways.
i. By the well known decision procedure for (Q,<,+1).
ii. By directly bounding the numerators and denominators involved in
the finite f.
Alternatively, we can go from Q to Z and adjust the upper shift in an
obvious way. Also k+.5 needs to be raised. Then i,ii are not needed,
as the statement so constructed will be explicitly Pi01 as written.
A much more thorough treatment of this section 5 will appear on
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
**********************************************************
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 641st 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
Harvey Friedman
More information about the FOM
mailing list