FOM: 151:Finite forms by bounding
friedman@math.ohio-state.edu
friedman at math.ohio-state.edu
Wed Jun 5 04:36:41 EDT 2002
We first clarify some wording in the posting 150:Finite obstruction/statistics
(some people may have seen this with the number 149):
In the three paragraphs preceding Proposition A, there was some unclear
wording. The unclear wording stemmed from an unfortunate wording at the
beginning of the first of these three paragraphs. I wrote:
"In the three classifications with "infinite", "nonempty finite", and
"arbitrarily large finite", of the 6561 statements, ... "
This should be:
In the classification with "infinite", of the 6561 statements, ...
Also in the third of these three paragraphs (right before Proposition A), I
wrote:
"In each of these three sample spaces above..."
This should be:
In each of these two sample spaces above ...
##########################################
As usual, we start with this:
PROPOSITION 1. For all multivariate functions f,g from N into N of expansive
linear growth, there exists infinite A,B,C containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.
{Recall that U. is disjoint union, which is ordinary union together with the
assertion of disjointness. Recall that hX is the set of all values of h at
arguments drawn from X. The above is a particularly elegant focused corner of
Boolean Relation Theory}.
In the preceding posting 150:Finite obstruction/statistics, (some people may
have seen this with the number 149), we discussed the classification of all
variants of Proposition 1 obtained by using any letters from {A,B,C} in the
eight positions that already have letters from {A,B,C}, thereby generating
exactly 6561 statements. (Of course, there is much symmetry).
In this posting, I want to return to what may appear to be a lifelong obsession
of mine. GIVE A CLEAN FINITE FORM. In other words, give a finite form which is
as close in conception as possible to Proposition 1.
The main approach to this for quite some time has been to first consider the
following closely related statement whose hypothesis is of a finite character:
PROPOSITION 2. For all strictly dominating piecewise linear functions f,g, over
N, there exists infinite A,B,C containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.
{These functions are of the form f:N^k into N and are defined by finitely many
cases, each case given by a finite set of linear inequalities with coefficients
from N, where on each case the function is given by an affine function with
coefficients from N. Strict dominance means F(x) > |x|, where |x| is the sup
norm}.
We have already shown that Proposition 2 is provable using Mahlo cardinals of
finite order but not in ZFC. In fact, Proposition 2 is provably equivalent to
the consistency (not the 1-consistency) of ZFC + {there exists an n-Mahlo
cardinal}_n over ACA.
Given the finitary explicit nature of piecewise linear functions over N (or
even over Z), the issue of finiteness surrounds the use of arbitrary infinite
A,B,C containedin N.
The latest approach to this was in the posting 148:Finite forms by
relativization, where we replaced "infinite" in Proposition 2 by "piecewise
linear exponential ranges". Actually, this can be simplified somewhat, but in
any case this involves the use of compound exponential terms, which is
acceptable.
HOWEVER, in this posting, we handle this problem in a much more straightforward
way, a way that we have overlooked for an embarassingly long time.
The idea is to first consider
PROPOSITION 3. For all strictly dominating piecewise linear functions f,g, over
N, there exists arbitrarily large finite A,B,C containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.
Of course, this is the ultimate solution if it worked! However, it is provable
in RCA_0, as expected. We must say more about these finite sets.
We say that A containedin N is bounded by F:N into N if and only if for all i >
= 1, the i-th element of A, if it exists, does not exceed F(i). Note that this
definition makes perfectly good sense regardless of the cardinality of A.
For our purposes, a triple exponential is a function of the form 2^2^2^cn,
where c is a positive integer.
PROPOSITION 4. For all strictly dominating piecewise linear functions f,g, over
N, there exists arbitrarily large finite A,B,C containedin N, all bounded by
some common triple exponential, such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.
Note that Proposition 4 is a Pi-0-4 sentence, since it has the form "for all
suitable functions, there exists a triple exponential such that for all n,
there exists finite A,B,C with at least n elements bounded by the triple
exponential, with those two inclusions."
It is easy to show that we can give a suitable a priori upper bound on the size
of the desired A,B,C (in terms of n and the presentations of f,g) so that the
statement is put into Pi-0-3 form.
Moreover, from analyzing the proof of Proposition 4 from Mahlo cardinals of
finite order, we see that we can also provide a suitable a priori upper bound
on the exponent c in the triple exponential (in terms of the presentations of
f,g).
When both upper boundings are in place, we have a Pi-0-1 sentence. The
boundings are quite reasonable, involving at most triple exponential
expressions.
In any case, it is already clear from a proper reading of Proposition 4 that
Proposition 4 is in FINITE FORM.
*********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 151st in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:
100:Boolean Relation Theory IV corrected 3/21/01 11:29AM
101:Turing Degrees/1 4/2/01 3:32AM
102: Turing Degrees/2 4/8/01 5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01 11:10AM
104:Turing Degrees/3 4/12/01 3:19PM
105:Turing Degrees/4 4/26/01 7:44PM
106.Degenerative Cloning 5/4/01 10:57AM
107:Automated Proof Checking 5/25/01 4:32AM
108:Finite Boolean Relation Theory 9/18/01 12:20PM
109:Natural Nonrecursive Sets 9/26/01 4:41PM
110:Communicating Minds I 12/19/01 1:27PM
111:Communicating Minds II 12/22/01 8:28AM
112:Communicating MInds III 12/23/01 8:11PM
113:Coloring Integers 12/31/01 12:42PM
114:Borel Functions on HC 1/1/02 1:38PM
115:Aspects of Coloring Integers 1/3/02 10:02PM
116:Communicating Minds IV 1/4/02 2:02AM
117:Discrepancy Theory 1/6/02 12:53AM
118:Discrepancy Theory/2 1/20/02 1:31PM
119:Discrepancy Theory/3 1/22.02 5:27PM
120:Discrepancy Theory/4 1/26/02 1:33PM
121:Discrepancy Theory/4-revised 1/31/02 11:34AM
122:Communicating Minds IV-revised 1/31/02 2:48PM
123:Divisibility 2/2/02 10:57PM
124:Disjoint Unions 2/18/02 7:51AM
125:Disjoint Unions/First Classifications 3/1/02 6:19AM
126:Correction 3/9/02 2:10AM
127:Combinatorial conditions/BRT 3/11/02 3:34AM
128:Finite BRT/Collapsing Triples 3/11/02 3:34AM
129:Finite BRT/Improvements 3/20/02 12:48AM
130:Finite BRT/More 3/21/02 4:32AM
131:Finite BRT/More/Correction 3/21/02 5:39PM
132: Finite BRT/cleaner 3/25/02 12:08AM
133:BRT/polynomials/affine maps 3/25/02 12:08AM
134:BRT/summation/polynomials 3/26/02 7:26PM
135:BRT/A Delta fA/A U. fA 3/27/02 5:45PM
136:BRT/A Delta fA/A U. fA/nicer 3/28/02 1:47AM
137:BRT/A Delta fA/A U. fA/beautification 3/28/02 4:30PM
138:BRT/A Delta fA/A U. fA/more beautification 3/28/02 5:35PM
139:BRT/A Delta fA/A U. fA/better 3/28/02 10:07PM
140:BRT/A Delta fA/A U. fA/yet better 3/29/02 10:12PM
141:BRT/A Delta fA/A U. fA/grammatical improvement 3/29/02 10:43PM
142:BRT/A Delta fA/A U. fA/progress 3/30/02 8:47PM
143:BRT/A Delta fA/A U. fA/major overhaul 5/2/02 2:22PM
144: BRT/A Delta fA/A U. fA/finesse 4/3/02 4:29AM
145:BRT/A U. B U. TB/simplification/new chapter 4/4/02 4:01AM
146:Large large cardinals 4/18/02 4:30AM
147:Another Way 7:21AM 4/22/02
148:Finite forms by relativization 2:55AM 5/15/02
149:Bad Typo 1:59PM 5/15/02
150:Finite obstruction/statisics 8:55AM 6/1/02
More information about the FOM
mailing list