FOM: June 1 - June 30, 2002

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

FOM: 151:Finite forms by bounding

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 

"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 

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 

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 

When both upper boundings are in place, we have a Pi-0-1 sentence. The 
boundings are quite reasonable, involving at most triple exponential 

In any case, it is already clear from a proper reading of Proposition 4 that 
Proposition 4 is in FINITE FORM. 


   I use 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]