[FOM] 423: Well Behaved Reduction Functions 2
Harvey Friedman
friedman at math.ohio-state.edu
Thu May 27 11:21:36 EDT 2010
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION.
**********************************************************************
There has been a major breakthrough in finding a very simple notion of
WELL BEHAVEDNESS that creates independent Pi01 sentences.
Of course, there is still, lying in the background, the plan to
systematically develop the theory of Well Behavedness, and use that
also in independent Pi01 statements.
This new idea of having things be constant on subsequences from a
sequence gives a rather striking new way of stating the ordinary
Ramsey theorems (see section 3 below).
PROPOSITION. Every R contained in N^k x N^k has a reduction function
whose regressive k-composites are constant on the length k
subsequences of some common nonconstant infinite sequence.
PROPOSITION. Every R contained in N^k x N^k has a finite reduction
function whose regressive k-composites are constant on the length k
subsequences of some common nonconstant sequence of length k+1.
PROPOSITION. Every order invariant R contained in N^k x N^k has a
finite reduction function whose regressive p-composites are constant
on the length k subsequences of some common nonconstant sequence of
length r.
PROPOSITION. Every order invariant R contained in N^k x N^k has a
reduction function <= (8k)!! whose regressive k-composites are
constant on the length k subsequences of {(7k)!!,(7k)!!^2,...,(7k)!!^k}.
Here !! is safe overkill.
We place bounds on the second and third Propositions, thereby
obtaining explicitly Pi01 sentences. The fourth Proposition is already
explicitly Pi01.
THIS ABSTRACT IS SELF CONTAINED.
WELL BEHAVED REDUCTION FUNCTIONS 2
by
Harvey M. Friedman
May 27, 2010
1. REDUCTION FUNCTIONS.
2. COMPOSITES AND REGRESSIVITY.
3. INFINITE REDUCTION FUNCTION THEOREM.
4. FINITE REDUCTION FUNCTION THEOREMS.
5. ORDER INVARIANT REDUCTION FUNCTION THEOREMS.
6. EXPONENTIAL PRESBURGER.
7. WELL BEHAVEDNESS.
1. REDUCTION FUNCTIONS.
Let N be the set of all nonnegative integers.
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.
THEOREM 1.1. Let R,A be given. There is a reduction function from A
into A. Any reduction function from A into A is idempotent. Any two
reduction functions from A into A have the same fixed points. The
reduction functions f:A into A are exactly the functions f:A into A
such that for all x in A, f(x) is a strict R reduction of x that is a
fixed point of f, if this exists; x otherwise.
I am anxious to explore a lot of ways to motivate reduction functions.
They have a direct motivation in terms of kernels of induced
subdigraphs of R* = {(x,y) in R: max(x) > max(y)}. Reduction functions
then merely witness the kernel in an obvious sense.
Obviously, various known and yet to be known motivations for kernels
in digraphs are highly relevant, as a reduction function is a kind of
straightforward witness to being a kernel.
Some possible motivations are geometric - roughly finding a set of
observers that don't see each other, but see everybody else. Or in
communication networks, placing stations, etc. All of these that I am
thinking of have associated variants that are perhaps even more
natural, and this leads to altered notions of reduction functions that
may be more natural yet - and where it is not yet clear whether we get
independent Pi01 sentences when we plug in these changes into the
statements in sections 3,4,5.
One rather mild change would be to change the relation
max(x) > max(y)
that is used in our "reductions" to the more geometric
|x| > |y|
where | | is the ordinary Euclidean norm of x,y in N^k. Or generally,
that we can use any standard kind of norm function, and everything is
fine. We haven't yet checked this, but it seems highly likely.
When we were doing one dimensional forms some time ago on the FOM, we
were writing integers as signed sums of other integers. The additive
rewrite idea should be revisited also in the present context.
FLASH: I see that even if we are doing one dimensional stuff, the k-
composites should involve addition, and take the k-composites to be
multivariate (say, use at most k variables), and then we can talk
about the regressive ones being constant on the subsequences yet
again. So it seems like there may be a real point in now having a
series on
WELL BEHAVED REWRITING FUNCTIONS
and this in turn suggests that perhaps I should look at *term
rewriting* - a fairly active area area of computer science!
2. COMPOSITES AND REGRESSIVITY.
Let f:A into A, A contained in N^k.
We consider the expressions involving the component functions
f_1,...,f_k:A into N of f and variables x_1,...,x_k. E.g., for k = 3,
h(g(x,z,z),x,f(y,h(z,z,y),y))
where for readability, we have used f,g,h for f_1,f_2,f_3, and x,y,z
for x_1,x_2,x_3.
In logic, these are called the terms in k-ary function symbols
f_1,...,f_k and variables x_1,...,x_k.
Each of these define a partial function from A into N. We adhere to
the important convention that if an expression is defined then all of
its subexpressions are defined.
We define the k-composites of f to be the partial functions from A
into N that are given by such expressions involving at most k
functions. Thus the displayed expression defines a 4-composite of f.
Note that in general, the domain of a k-composite will be a proper
subset of A.
3. INFINITE REDUCTION FUNCTION THEOREMS.
We can restate the ordinary Ramsey theorems from 1930 in terms of
subsequences from nonconstant sequences, as follows.
INFINITE RAMSEY THEOREM. Every f:N^k into [m] is constant on the
length k subsequences of some nonconstant infinite sequence.
FINITE RAMSEY THEOREM. If n >> k,m,r, then every f:[n]^k into [m] is
constant on the length k subsequences of some nonconstant sequence of
length r.
Now for the exotic.
PROPOSITION 3.1. Every R contained in N^k x N^k has a reduction
function whose regressive k-composites (p-composites) are constant on
the length k subsequences of some common nonconstant infinite sequence.
THEOREM 3.2. Propositions 3.1 is provable in SRP+ but not from
any consequence of SRP that is consistent with RCA_0. Proposition
3.1 is provably equivalent, over ACA', to Con(SRP).
Proposition 3.1 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".
4. FINITE REDUCTION FUNCTION THEOREMS.
PROPOSITION 4.1. Every R contained in N^k x N^k has a finite reduction
function whose regressive k-composites (p-composites) are constant on
the length k subsequences of some common nonconstant sequence of
length k+1 (length r).
A k-ary reduction function is said to be <= n if and only if its
domain is contained in [0,...,n)^k.
We write 2^[t] for the exponential stack of t 2's.
PROPOSITION 4.2. Every R contained in N^k x N^k has a reduction
function <= 2^[8k] whose regressive k-composites are constant on the
length k subsequences of some common nonconstant sequence of length k+1.
PROPOSITION 4.3. Every R contained in N^k x N^k has a reduction
function <= 2^[8kpr] whose regressive p-composites are constant on the
length k subsequences of some common nonconstant sequence of length r.
Obviously, only the part of R bounded by 2^[8k] or 2^[8kpr] can
possibly be relevant.
We now have the explicitly Pi01 sentences
PROPOSITION 4.4. Every R contained in [2^[8k]]^k x [2^[8k]]^k has a
reduction function <= 2^[8k] whose regressive k-composites are
constant on the length k subsequences of some common nonconstant
sequence of length k+1.
PROPOSITION 4.5. Every R contained in [2^[8k)]]^k x [2^[8k]]^k has a
reduction function <= 2^[8kpr] whose regressive p-composites are
constant on the length k subsequences of some common nonconstant
sequence of length r.
THEOREM 4.6. Propositions 4.1 - 4.5 are provable in SRP+ but not from
any consequence of SRP that is consistent with RCA_0. Proposition 4.1
is provably equivalent, over RCA_0, to Con(SRP). Propositions 4.2 -
4.5 are provably equivalent, over SEFA, to Con(SRP).
Here SEFA = super exponential function arithmetic.
5. ORDER INVARIANT REDUCTION FUNCTION THEOREMS.
PROPOSITION 5.1. Every order invariant R contained in N^k x N^k has a
reduction function whose regressive k-composites (p-composites) are
constant on the length k subsequences of some common nonconstant
infinite sequence.
PROPOSITION 5.2. Every order invariant R contained in N^k x N^k has a
finite reduction function whose regressive k-composites (p-composites)
are constant on the length k subsequences of some common nonconstant
sequence of length k+1 (length r).
PROPOSITION 5.3. Every order invariant R contained in N^k x N^k has a
reduction function <= (8k)! whose regressive k-composites are constant
on the length k subsequences of some common nonconstant sequence of
length k+1.
We can even be explicit about the common set.
PROPOSITION 5.4. Every order invariant R contained in N^k x N^k has a
reduction function <= (8k)!! whose regressive k-composites are
constant on the length k subsequences of some common nonconstant
geometric progression of length k+1.
PROPOSITION 5.5. Every order invariant R contained in N^k x N^k has a
reduction function <= (8k)!! whose regressive k-composites are
constant on the length k subsequences of {(7k)!!,(7k)!!^2,...,(7k)!!^k}.
Note that Proposition 5.2 is explicitly Pi02, and Propositions 5.3 -
5.5 are explicitly Pi01.
THEOREM 5.6. Propositions 5.1 - 5.5 are provable in SRP+ but not from
any consequence of SRP that is consistent with ACA'. Propositions 5.1
- 5.5 are provably equivalent, over RCA_0, to Con(SRP). Propositions
5.2 - 5.5 are provably equivalent, over EFA, to Con(SRP).
Here EFA = exponential function arithmetic.
6. 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 6.1. Every R contained in N^k x N^k has a reduction
function whose regressive k-composites are constant on the length k
subsequences of some common nontrivial infinite sequence.
THEOREM 6.2. For all k >= 1, every order invariant R contained in N^k
x N^k has an exponential Presburger reduction function whose
regressive k-composites are constant on the length k subsequences of
some common 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.
7. WELL BEHAVEDNESS.
There is a strongest reasonable notion of what we mean by a partial
function f:N^k into N being well behaved over E contained in N. The
notion is presented in terms of a set of functions of the form
f:E^k into N
where E is an infinite subset of N, up to isomorphism. It can also be
given a set of actual functions
f:E^k into N
where E is the set of powers of 2 that are greater than 2^(8k)!!.
These isomorphism types can be used for our Propositions. Any other
isomorphism type will make our Propositions refutable in RCA_0.
This strong dichotomy also holds when we consider finite E, and even E
of cardinality k.
There are also strong connections with the behavior of affine
transformations T:N^k into N with nonnegative coefficients.
Exact formulations of these results will have to wait until I get some
more time to work them out.
**********************
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
422: Well Behaved Reduction Functions 1 5/23/10 4:12PM
Harvey Friedman
More information about the FOM
mailing list