[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: <fom@math.psu.edu>*Subject*: FOM: 151:Finite forms by bounding*From*: friedman@math.ohio-state.edu*Date*: Wed, 5 Jun 2002 08:36:41 -0000*Sender*: owner-fom@math.psu.edu

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

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]