FOM: 129:Finite BRT/Improvements

[Harvey Friedman]

This posting is the result of my efforts to find finite statements in BRT
that are more "beautiful" than the finite statements in posting 128. Here
is my current approach.

*GENERAL STRATEGY*

1. The finite statements should be as close as possible in form and content
to the infinitary statements. This is because of the very sharp recent
improvements in the infinitary statements. As an indication of a major
change, the new infinitary statements are now being judged by several
significant authorities outisde the logic communicty as "beautiful" -
earlier versions were never judged as "beautiful" by these same
authorities. These authorities went from "nice", "interesting", and the
like, to "beautiful" on the basis of the same new infinitary statements.
This is not a coincidence, and is not a function of the personal
interaction.

2. In particular, I cannot expect to find finite statements (at least in
the near future) that are "beautiful" unless they are very closely allied
to the "beautiful" infinitary statements.

3. I prefer to use highly concrete functions only (forming a countable
class of functions) so that I do not need to clutter the statement with
variables representing finite initial segments of N or Z, and associated
quantifiers. However, one could still use friendly slang like "for all
functions defined on sufficiently large initial segments of N (with certain
conditions) satisfying the following estimate ...". Nevertheless, there
would inevitably have to be some care taken with the conditions/estimates,
whereas such considerations do not surface in the "beautiful" infinitary
statements.

4. Such highly concrete functions should generally be on the integers, not
just on N. This is because they involve the group or ring stucture of Z.
However, in the case of arbitrary functions (satisfying growth conditions),
it is preferable to use N instead of Z. This is because many people will
only be concerned with the infinitary statements, and use of N is
conceptually simpler than use of Z.

An exception is d and e below, where N plays a special role as the
coefficient space. So here it is particularly natural for the functions to
live on N.

5. The conclusion will assert the existence of finite sets A,B,C obeying
the same two disjoint union inclusions that I use for the state of the art
infinitary statements.

6. An additional condition is placed simultaneously on each of A,B,C, thus
maintaining symmetry. The condition should be uncluttered, clear,
symmetric, and thematic. Here is where I use common slang to keep things
"beautiful". The additional condition asserts that the three sets each
contain any finite set given in advance of prescribed kind.

6. The statement would be of a more purely combinatorial nature if I didn't
follow 3 above. Using arbitrary functions (with finite domains subject to
growth conditions) definitely should appear in a full manuscript. However,
I think that it is important to feature the approach with concrete
functions when discussing finite BRT.

*THE TEMPLATE AND SOME CLASSES OF CONCRETE FUNCTIONS*

The form of the finite statement is as follows.

PROPOSITION. For all f,g in V there exist finite A,B,C containedin Z (or N)
such that

A U. fA containedin C U. gB
A U. fB containedin C U. gC

where A,B,C each contain any given finite exponential progression whose
base is sufficiently large relative to f,g.

We use the following classes of concrete functions.

a. Expansive integral piecewise polynomial functions. These are the
functions of the form F:Z^k into Z such that

i) there exists c > 1 such that for all x in dom(F), |F(x)| >= c|x|;
ii) F is defined by a partition of its domain into finitely many pieces,
each of which are defined by a finite set of polynomial inequalities with
integer coefficients, where on each piece the function is defined by a
polynomial with integer coefficients.

b. Expansive integral polynomials from halfspace to fullspace. These are
the functions of the form F:Z^k-1 x N into Z^k such that

i) there exists c > 1 such that for all x in Z^k-1 x N, |F(x)| >= c|x|;
ii) F is defined by a partition of its domain into finitely many pieces,
each of which are defined by a finite set of linear inequalities with
integer coefficients, where on each piece the function is defined by a
polynomial  with integer coefficients.

c. Expansive integral piecewise linear functions. These are the functions
of the form F:Z^k into Z such that

i) there exists c > 1 such that for all x in Z^k, |F(x)| >= c|x|;
ii) F is defined by a partition of its domain into finitely many pieces,
each of which are defined by a finite set of linear inequalities with
integer coefficients, where on each piece the function is defined by an
affine transformation with integer coefficients.

d. Strictly dominating N piecewise linear functions. These are the
functions of the form F:N^k into N such that

i) for all x in N^k, F(x) > |x|;
ii) F is defined by a partition of its domain into finitely many pieces,
each of which are defined by a finite set of linear inequalities with
integer coefficients, where on each piece the function is defined by an
affine transformation with nonnegative integer coefficients.

e. Strictly dominating N affine transformations from a finite intersection
of halfspaces into N. These are functions of the form F:A into N, A
containedin N^k, such that

i) for all x in A, f(x) > |x|;
ii) A is a finite intersection of halfspaces in N^k;
iii) F is the restriction of an affine transformation from Z^k into Z with
nonnegative integer coefficients.

For b, the notion of FA is the set of all coordinates of values of f at
arguments from A.

An exponential progression with base k is a finite or infinite subset of N
where each term after the first term is k raised to the previous term.

*RESULTS*

THEOREM 1. Suppose V is any of
i) the set of all expansive integral piecewise polynomial functions;
ii) the set of all expansive integral polynomials from upper halfspace to
fullspace.
Then the Proposition is provably equivalent to the 1-consistency of MAH
over EFA (exponential function arithmetic).

THEOREM 2. Suppose V is any of
i) the set of all strictly dominating N piecewise linear functions;
ii) the set of all strictly dominating N affine transformations from a
finite intersection of halfspaces into N.
Then the Proposition is provably equivalent to the consistency of MAH over
EFA (exponential function arithmetic).

The above results do not address the set of all expansive integral
piecewise linear functions. I have been hedging my claims for some time
because there are particularly delicate constructions needed for a
reversal, surrounding special difficulties in getting a pairing function.
The full checking of the details of this must wait. This is why I started
using strictly dominating N piecewise linear functions. Here the pairing
problems can be resolved comparatively easily. I can't use strictly
dominating integral piecewise linear functions, because then the
Proposition, even with infinite A,B,C, would be refutable.

So with this preamble, for the case of V = the set of all expansive
integral piecewise linear functions, the result should be the same as
Theorem 2.

In the case of Theorem 2, one can provide triple exponential upper bounds
on "sufficiently large" and on the maximum of A union B union C in terms of
the presentations of the functions f,g. This results in explicitly Pi-0-1
sentences.

Finite exponential progressions are convenient, but much lower rates of
growth will suffice.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 129th 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