[FOM] 422: Well Behaved Reduction Functions 1
Harvey Friedman
friedman at math.ohio-state.edu
Sat May 22 22:01:40 EDT 2010
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION.
**********************************************************************
TEMPLATE. Every R contained in N^k x N^k has a reduction function
whose k-composites are "ultimately well behaved" over some common
infinite set.
TEMPLATE. Every R contained in N^k x N^k has a finite reduction
function whose k-composites are "ultimately well behaved" over some
common k element set.
TEMPLATE. Every order invariant R contained in N^k x N^k has a finite
reduction function whose k-composites are "ultimately well behaved"
over some common k element set.
Various levels of "well behavedness" short of "ultimately well
behaved" are expected to correspond to the consistency of systems
ranging from PA through SRP.
Note that the last Template is explicitly Pi02. The last two Templates
can be given estimates (iterated exponential for the second, and
double exponential for the third), so that they become explicitly Pi01.
Well Behaveedness Theory is a rather delicate and large subject, even
in the realm of N.
We only scratch the surface of it with one narrow aspect that we are
able to handle right at this moment.
I will come back to this seriously in about a month, and also go back
to measurables through rank into rank and a bit higher.
WELL BEHAVED REDUCTION FUNCTIONS
Harvey M. Friedman
May 22, 2010
1. REDUCTION FUNCTIONS.
2. COMPOSITES.
3. WELL BEHAVEDNESS.
4. INFINITE REDUCTION FUNCTION THEOREM.
5. FINITE REDUCTION FUNCTION THEOREMS.
6. ORDER INVARIANT REDUCTION FUNCTION THEOREMS.
7. EXPONENTIAL PRESBURGER.
8. BEST POSSIBLE.
9. RADICAL FUTURE.
1. REDUCTION FUNCTIONS.
Let N be the set of all nonnegative integers.
We consider R contained in N^k x N^k.
We say that y is a strict R reduction of x if and only if max(x) >
max(y) and x R y.
We say that y is an R reduction of x if and only if y is a strict R
reduction of x or y = x.
We say that f is a reduction function for R if and only if
i. f:A into A, A contained in N^k.
ii. For all x in A, f(x) is an R reduction of x.
iii. No value of f is a strict R reduction of any value of f.
We think of
y is a strict R reduction of x
as asserting that
y "strictly simplifies to x".
We think of
y is an R reduction of x
as asserting that
y "simplifies to x".
Let f:A into A be a reduction function for R. Then
each x in A is simplified by f to a "core", f(x), that is not going to
strictly simplify to any other "core".
NOTE: In this motivating language, simplification and strict
simplification are not transitive.
THEOREM 1.1. Let R,A be given. There is a reduction function from A
into A. Its range is the same as its fixed points. Any two reduction
functions from A into A have the same range (or fixed points). The
reduction functions f:A into A are exactly the functions f:A into A
that are defined by: f(x) is a strict R reduction of x that is a fixed
point of f, if this exists; x otherwise.
2. COMPOSITES.
Let f:A into A, A contained in N^k.
The 0-composites of f are the k component functions f_1,...,f_k:A into
N, together with the k projection functions pi_i:A into N given by
pi_i(x_1,...,x_k) = x_i.
The n+1-composites of f are the n-composites of f together with the
partial functions g:A into N given by
g(x_1,...,x_k) = h(F_1(x_1,...,x_k),...,F_k(x_1,...,x_k))
where h,F_1,...,F_k are n-composites of f.
Note that the domain of g above consists of the (x_1,...,x_k) for which
each F_i(x_1,...,x_k) is defined; and
h(F_1(x_1,...,x_k),...,F_k(x_1,...,x_k)) is defined.
Note that the domain of an n-composite of f is a (possibly very thin)
subset of A.
3. WELL BEHAVEDNESS.
Here we merely scratch the surface of Well Behavedness Theory by
focusing on a rich but particularly manageable aspect.
We now define the k-ary well behavedness conditions. We use the
function symbol F and numerical variables x_1,x_2,... .
A k-ary well behavedness condition is a statement of the form
s op t implies s' op t'
where
i. s,t,s',t' are each either some x_i, or of the form f(x_i1,...,x_ik).
ii. Each op is among <,<=,=.
We say that a k-ary well behavedness condition holds of f on E if and
only if
i. f:N^k into N is partial.
ii. E is a subset of N.
iii. If x_i appears in the condition, then there are at least i
elements of E.
iv. The condition forms a true statement if each x_i appearing is
interpreted as the i-th element of E.
Let W[k] be the set of all k-ary well behavedness conditions such that
the following holds. For every piecewise linear f:N^k into N, there
exists E contained in N such that the condition holds of f on E.
Let W*[k] be the set of all k-ary well behavedness conditions such
that the following holds. For every piecewise linear f:N^k into N with
nonnegative integer coefficients, there exists E contained in N such
that the condition holds of f on E.
Obviously each W[k], W*[k] are finite. Note that W[k] and W*[k] are
different. For example,
f(x_2) < x_2 implies f(x_2) = f(x_3)
lies in W*[k] but not in W[k], because of f(x) = x-1 if x > 0; 0
otherwise.
THEOREM 3.1. The W[k], W*[k] are totally intelligibly and
interestingly low level algorithmically decidable, uniformly in k.
We say that partial f:N^k into N is ultimately well behaved on E if
and only if every element of W*[k] that uses only variables whose
subscript is at most the cardinality of E, holds of f on E.
Note that if f:A into N is ultimately well behaved on E then dom(f)
includes E^k. This is clear by considering the elements of W*[k],
x_1 = x_1 implies f(x_i1,...,x_ik) = f(x_i1,...,x_ik).
Also, the Lower Shift Invariance used in http://www.cs.nyu.edu/pipermail/fom/2010-May/014744.html
is expressed here in the form
f(x_i,...,x_i+k-1) < x_i implies f(x_i,...,x_i+k-1) = f(x_i+1,...,x_i
+k).
Of course, this is in W*[k]\W[k].
We will systematically develop Well Behavedness Theory later,
including lots of robustness theorems. Well Behavedness Theory
naturally subsumes Paris/Harrington theory and more.
4. INFINITE REDUCTION FUNCTION THEOREMS.
PROPOSITION 4.1. Every R contained in N^k x N^k has a reduction
function whose k-composites are ultimately well behaved over some
common infinite set.
PROPOSITION 4.2. Every R contained in N^k x N^k has a reduction
function whose p-composites are ultimately well behaved over some
common infinite set.
THEOREM 4.3. Propositions 4.1, 4.2 are provable in SRP+ but not from
any consequence of SRP that is consistent with RCA_0. Propositions
4.1, 4.2 are provably equivalent, over RCA_0, to Con(SRP).
Proposition 4.2 allows us to fix k and let p vary, obtaining
independence statements climbing up the SRP hierarchy.
Here SRP+ = ZFC + "for all k there exists a limit ordinal with the k-
SRP. SRP = ZFC + {there exists a limit ordinal with the k-SRP}_k. The
k-SRP asserts that every partition of the unordered k-tuples from
lambda into two pieces has a homogeneous set that is a stationary
subset of lambda. ACA' is ACA_0 + "for all n in N and x contained in
N, the n-th Turing jump of x exists". Another way of formulating ACA'
is ACA_0 + "arithmetic recursion on omega".
5. FINITE REDUCTION FUNCTION THEOREMS.
PROPOSITION 5.1. Every R contained in N^k x N^k has a finite reduction
function whose k-composites are ultimately well behaved over some
common k element set.
PROPOSITION 5.2. Every R contained in N^k x N^k has a finite reduction
function whose p-composites are ultimately well behaved over some
common r element set.
A k-ary reduction function is said to be below n if and only if its
domain is contained in [n]^k = [0,...,n)^k.
We write 2^[t] for the exponential stack of t 2's.
PROPOSITION 5.3. Every R contained in N^k x N^k has a reduction
function below 2^[8k] whose k-composites are ultimately well behaved
over some common k element set.
PROPOSITION 5.4. Every R contained in N^k x N^k has a reduction
function below 2^[8kpr] whose p-composites are ultimately well behaved
over some common r element set.
Obviously, only the part of R bounded by 2^[8k] or 2^[8kpr] can
possibly be relevant. For R contained in [n]^2k, reduction functions
are required to have domain contained in {0,...,n}^k.
We now have the explicitly Pi01 sentences
PROPOSITION 5.5. Every R contained in [2^(8k)]^k x [2^[8k]]^k has a
reduction function whose k-composites are ultimately well behaved over
some common k element set.
PROPOSITION 5.6. Every R contained in [2^(8k)]^k x [2^[8k]]^k has a
reduction function below 2^[8kpr] whose p-composites are ultimately
well behaved over some common r element set.
THEOREM 5.7. Propositions 5.1 - 5.6 are provable in SRP+ but not from
any consequence of SRP that is consistent with ACA'. Propositions 5.1
- 5.6 are provably equivalent, over ACA', to Con(SRP). In the case of
Propositions 5.5, 5.6, we can use SEFA instead of ACA'.
Here SEFA = super exponential function arithmetic.
6. ORDER INVARIANT REDUCTION FUNCTION THEOREMS.
PROPOSITION 6.1. Every order invariant R contained in N^k x N^k has a
reduction function whose k-composites (p-composites) are lower shift
invariant over some common infinite set.
PROPOSITION 6.2. Every order invariant R contained in N^k x N^k has a
finite reduction function whose k-composites are ultimately well
behaved over some common k element (r element) set.
PROPOSITION 6.3. Every order invariant R contained in N^k x N^k has a
reduction function below (8k)!] whose k-composites are lower shift
invariant over some k element (r element) set.
We can even be explicit about the common set.
PROPOSITION 6.4. Every order invariant R contained in N^k x N^k has a
reduction function below [(8k)!]^k whose k-composites are ultimately
well behaved over some k element (r element) geometric progression.
PROPOSITION 6.5. Every order invariant R contained in N^k x N^k has a
reduction function below [2(8k)!]^k whose k-composites are ultimately
well behaved over 2^(8k)!,...,2^((8k)!+k)}.
Note that Proposition 6.2 is explicitly Pi02, and Propositions 6.3 -
6.5 are explicitly Pi01.
THEOREM 6.6. Propositions 6.1 - 6.5 are provable in SRP+ but not from
any consequence of SRP that is consistent with ACA'. Propositions 6.1
- 6.5 are provably equivalent, over RCA_0, to Con(SRP). Propositions
6.2 - 6.5 are provably equivalent, over EFA, to Con(SRP).
Here EFA = exponential function arithmetic.
7. EXPOENENTIAL PRESBURGER SETS.
Presburger arithmetic is the first order theory of the structure (N,
+). Exponential Presburger arithmetic is the first order theory of the
structure (N,+,2^). I.e., we add base 2 exponentiation to Presburger
arithmetic. THere remains a decision procedure. See, e.g.,
F. Point, On the Expansion (N;+;2^x) of Presburger Arithmetic,
Appendix B, Book Drafts, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html
Recall
PROPOSITION 7.1. Every R contained in N^k x N^k has a reduction
function whose k-composites are ultimately well behaved over some
common infinite set.
THEOREM 7.1. For all k >= 1, every order invariant R contained in N^k
x N^k has an exponential Presburger reduction function whose k-
composites are ultimately well behaved over some tail of the powers of
2.
This sentence is provably equivalent to Con(SRP) over SEFA.
From the decision procedure for exponential Presburger arithmetic
(see F. Point above), this yields a Pi02 sentence. By placing a
suitable bound on the complexity of the exponential Presburger
function, this yields a Pi01 sentence.
8. BEST POSSIBLE.
Is there a proper superset of W*[k] that can be used in place of
"ultimately well behaved" - which corresponds to W*[k] - in the above
Propositions? Obviously, the answer is yes, because we can certainly add
x_1 = x_1 implies f(x_i1,...,x_ik) <= x_j
where j = max(i1,...,ik).
We can redefine W*[k] using piecewise linear functions with
coefficients from N obeying f(x_1,...,x_k) <= max()x_1,...,x_k),
obtaining the larger sets W**[k].
Then "ultimately well behaved" based on W**[k] appears to be best
possible.
We have not had an opportunity to check the details of this claim, but
have some confidence.
9. RADICAL FUTURE.
One not too radical a direction is to work with, for example,
s op t and s' op t' implies s'' op t''
and more complicated forms propositional forms. Not only do we want to
get the best possible form of the Propositions for this stronger kind
of well behavedness, but also we would like to relate this kind of
well behavedness to standard functions in mathematics - like we did
with the piecewise linear functions from N^k into N with coefficients
from N.
ALso, there is the not too radical program of looking at various
notions of "well behaved" weaker than "ultimately well behaved", and
calculating the associated consistency statements, ranging from PA
through SRP.
More radical is the idea of templating the reduction functions
themselves. I.e., we would look at
TEMPLATE. Every R contained in N^k x N^k has a GADGET FUNCTION whose k-
composites are ULTIMATELY WELL BEHAVED over an infinite (k element) set.
And yet more radical,
TEMPLATE. Every object from a mathematically interesting class V has a
GADGET FUNCTION whose k-composites are ULTIMATELY WELL BEHAVED over a
NICE SET.
**********************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 422nd 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-349 can be found at http://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.
350: one dimensional set series 7/23/09 12:11AM
351: Mapping Theorems/Mahlo/Subtle 8/6/09 10:59PM
352: Mapping Theorems/simpler 8/7/09 10:06PM
353: Function Generation 1 8/9/09 12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1 8/9/09 6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2 8/10/09 6:18PM
356: Simplified HIGH SCHOOL and Mapping Theorem 8/14/09 9:31AM
357: HIGH SCHOOL Games/Update 8/20/09 10:42AM
358: clearer statements of HIGH SCHOOL Games 8/23/09 2:42AM
359: finite two person HIGH SCHOOL games 8/24/09 1:28PM
360: Finite Linear/Limited Memory Games 8/31/09 5:43PM
361: Finite Promise Games 9/2/09 7:04AM
362: Simplest Order Invariant Game 9/7/09 11:08AM
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
11:18AM
365: Free Reductions and Large Cardinals 1 9/24/09 1:06PM
366: Free Reductions and Large Cardinals/polished 9/28/09 2:19PM
367: Upper Shift Fixed Points and Large Cardinals 10/4/09 2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction 10/6/09
8:15PM
369. Fixed Points and Large Cardinals/restatement 10/29/09 2:23PM
370: Upper Shift Fixed Points, Sequences, Games, and Large Cardinals
11/19/09 12:14PM
371: Vector Reduction and Large Cardinals 11/21/09 1:34AM
372: Maximal Lower Chains, Vector Reduction, and Large Cardinals
11/26/09 5:05AM
373: Upper Shifts, Greedy Chains, Vector Reduction, and Large
Cardinals 12/7/09 9:17AM
374: Upper Shift Greedy Chain Games 12/12/09 5:56AM
375: Upper Shift Clique Games and Large Cardinals 1graham
376: The Upper Shift Greedy Clique Theorem, and Large Cardinals
12/24/09 2:23PM
377: The Polynomial Shift Theorem 12/25/09 2:39PM
378: Upper Shift Clique Sequences and Large Cardinals 12/25/09 2:41PM
379: Greedy Sets and Huge Cardinals 1
380: More Polynomial Shift Theorems 12/28/09 7:06AM
381: Trigonometric Shift Theorem 12/29/09 11:25AM
382: Upper Shift Greedy Cliques and Large Cardinals 12/30/09 2:51AM
383: Upper Shift Greedy Clique Sequences and Large Cardinals 1
12/30/09 3:25PM
384: THe Polynomial Shift Translation Theorem/CORRECTION 12/31/09
7:51PM
385: Shifts and Extreme Greedy Clique Sequences 1/1/10 7:35PM
386: Terrifically and Extremely Long Finite Sequences 1/1/10 7:35PM
387: Better Polynomial Shift Translation/typos 1/6/10 10:41PM
388: Goedel's Second Again/definitive? 1/7/10 11:06AM
389: Finite Games, Vector Reduction, and Large Cardinals 1 2/9/10
3:32PM
390: Finite Games, Vector Reduction, and Large Cardinals 2 2/14/09
10:27PM
391: Finite Games, Vector Reduction, and Large Cardinals 3 2/21/10
5:54AM
392: Finite Games, Vector Reduction, and Large Cardinals 4 2/22/10
9:15AM
393: Finite Games, Vector Reduction, and Large Cardinals 5 2/22/10
3:50AM
394: Free Reduction Theory 1 3/2/10 7:30PM
395: Free Reduction Theory 2 3/7/10 5:41PM
396: Free Reduction Theory 3 3/7/10 11:30PM
397: Free Reduction Theory 4 3/8/10 9:05AM
398: New Free Reduction Theory 1 3/10/10 5:26AM
399: New Free Reduction Theory 2 3/12/10 9:36AM
400: New Free Reduction Theory 3 3/14/10 11:55AM
401: New Free Reduction Theory 4 3/15/10 4:12PM
402: New Free Reduction Theory 5 3/19/10 12:59PM
403: Set Equation Tower Theory 1 3/22/10 2:45PM
404: Set Equation Tower Theory 2 3/24/10 11:18PM
405: Some Countable Model Theory 1 3/24/10 11:20PM
406: Set Equation Tower Theory 3 3/25/10 6:24PM
407: Kernel Tower Theory 1 3/31/10 12:02PM
408: Kernel tower Theory 2 4/1/10 6:46PM
409: Kernel Tower Theory 3 4/5/10 4:04PM
410: Kernel Function Theory 1 4/8/10 7:39PM
411: Free Generation Theory 1 4/13/10 2:55PM
412: Local Basis Construction Theory 1 4/17/10 11:23PM
413: Local Basis Construction Theory 2 4/20/10 1:51PM
414: Integer Decomposition Theory 4/23/10 12:45PM
415: Integer Decomposition Theory 2 4/24/10 3:49PM
416: Integer Decomposition Theory 3 4/26/10 7:04PM
417: Integer Decomposition Theory 4 4/28/10 6:25PM
418: Integer Decomposition Theory 5 4/29/10 4:08PM
419: Integer Decomposition Theory 6 5/4/10 10:39PM
420: Reduction Function Theory 1 5/17/10 2:53AM
421: Reduction Function Theory 2 5/19/10 12:00PM
Harvey Friedman
More information about the FOM
mailing list