FOM: 132:Finite BRT/cleaner

[Harvey Friedman]

>From a technical point of view, the finite BRT statements below are almost
identical to those in 131. However, the use of iterated logarithmic images
seems to be appealing.

We have also changed Propositions 4 and 10, using integral semilinear sets.
These are Boolean combinations of halfplanes presented with integer
coefficients.

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

Let A containedin Z. We define log(0,A) = A, log(m+1,A) = {[log(x)]: x in
log(m,A)}. Here [ ] is rounding to the nearest integer (up in case of a
tie).

PROPOSITION 1. For all expansive integral piecewise polynomial functions
f,g and sufficiently large n,r, there exist A,B,C containedin Z such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

PROPOSITION 2. For all expansive integral polynomials f,g from halfspace
into fullspace and sufficiently large n,r, there exist A,B,C containedin Z
such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

PROPOSITION 3. For all strictly dominating N piecewise linear functions f,g
and sufficiently large n,r, there exist A,B,C containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

PROPOSITION 4. Let f,g be strictly dominating restrictions of affine
transformations to semilinear sets in N^k, with coefficients
from N, and n,r be sufficiently large. There exist A,B,C containedin N such
that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

PROPOSITION 5. For all expansive integral piecewise linear functions and
sufficiently large n,r, there exist A,B,C containedin Z such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

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 n,k,r >= 8 and strictly dominating piecewise
linear functions f,g:N^k into N with coefficients from {0,...,n}, there exist
A,B,C containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n,A) = log(n,B) = log(n,C) = {0,...,r}.

PROPOSITION 9. Let n,k,r >= 8 and f,g:E into N be strictly dominating
restrictions of affine transformations, where E containedin N^k is
semilinear, all with coefficients from {0,...,n}. There exist A,B,C
containedin N such that
A U. fA containedin C U. gB
A U. fB containedin C U. gC
log(n+k,A) = log(n+k,B) = log(n,C) = {0,...,r}.

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

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).

The use of iterated logarithms is of course overkill. The growth rates
needed will be investigated in due course.

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

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

This is the 132nd 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