FOM: 130:Finite BRT/More

[Harvey Friedman]

We have continued to improve the finite BRT statements. This time we
introduce a couple of integer variables in the hypotheses, something we
avoided doing in the previous posting 129. However, there appears to be
enough to be gained by doing this.

For integers n,m we write [n,m] for the set of all integers i such that n
<= i <= m.

For A containedin N we write A!! = {p!!: p in A} and A!!! = {p!!!: p in A}.

See posting 129 for definitions of the categories of concrete functions
used below.

PROPOSITION 1. For all expansive integral piecewise polynomial functions
f,g and sufficiently large n,r, there exist [n,r]!!! containedin A,B,C
containedin [-(r+1)!!!,(r+1)!!!] such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 2. For all expansive integral polynomials f,g from halfspace
into fullspace and sufficiently large n,r, there exist [n,r]!!! containedin
A,B,C containedin [-(r+1)!!!,(r+1)!!!] such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 3. For all strictly dominating N piecewise linear functions f,g
and sufficiently large n,r, there exist [n,r]!! containedin A,B,C
containedin [1,r+1]!! such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 4. Let f,g be strictly dominating restrictions of affine
transformations to finite intersections of halfspaces, with coefficients
from N, and n,r be sufficiently large. There exist [n,r]!! containedin
A,B,C containedin [1,r+1]!! such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 5. For all expansive integral piecewise linear functions and
sufficiently large n,r, there exist [n,r]!! containedin A,B,C containedin
[-(r+1)!!,(r+1)!!] such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

THEOREM 6. Propositions 1,2 are both provably equivalent to the
1-consistency of MAH
over EFA (exponential function arithmetic). Propositions 3,4 are both
provably equivalent to the consistency of MAH over EFA (exponential
function arithmetic).

THEOREM 7. (Hedged claim as discussed in posting 129). Proposition 5 is
provably equivalent to the conssistency of MAH over EFA (exponential
function arithmetic).

In this setting, we can conveniently give explicitly Pi-0-1 forms of
Propositions 3-5 as follows.

PROPOSITION 8. For all r >= n >= k >= 8 and strictly dominating piecewise
linear functions f,g:N^k into N with coefficients from [0,n], there exist
[n,r]!!! containedin A,B,C containedin [1,r+1]!!! such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 9. Let r >= n >= k >= 8 and f,g:E into N be strictly dominating
restrictions of affine transformations, where E containedin N^k is a finite
intersections of halfspaces, all with coefficients from [0,n]. There exist
[n,r]!!! containedin A,B,C containedin [1,r+1]!!! such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

PROPOSITION 10. For all r >= n >= k >= 8 and expansive piecewise linear
functions f,g:Z^k into Z with coefficients from [-n,n], there exist
[n,r]!!! containedin A,B,C containedin [-(r+1)!!!,(r+1)!!!] such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC.

THEOREM 11. Propositions 9,10 are both provably equivalent to the
1-consistency of MAH
over EFA (exponential function arithmetic). Propositions 3,4 are both
provably equivalent to the consistency of MAH over EFA (exponential
function arithmetic).

THEOREM 12. (Hedged claim as discussed in posting 129). Proposition 10 is
provably equivalent to the conssistency of MAH over EFA (exponential
function arithmetic).

Note that we have reverted to triple factorials for Propositions 8-10 from
the double factorials of Propositions 3-5. This is cautious. More precise
information is not a priority at this point, and will wait until the
writing of manuscripts.

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

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

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