FOM: 136:BRT/A Delta fA/A U. fA/nicer

[Harvey Friedman]

Believe it or not, I really want to run out of ideas. Not yet, but
hopefully soon.

###########################################

This posting supercedes posting #135, 5:45PM  3/27/02. We need to correct
the way that strictly dominating was used there. We also do some badly
needed beautification.

Let E containedin Z. A piecewise linear function over E is a piecewise
linear function with coefficients lying in E U {0}.

PROPOSITION 1. Let k,n >= 1 and S1,...,Sn,T be k-ary piecewise linear
functions over the factorials, where T is strictly dominating and has only
unit coefficients. There exists finite A containedin N including (k+8)!!
such that min(S1A),...,min(SnA) in A Delta TA.

PROPOSITION 2. Let k,n >= 1 and S1,...,Sn,T be k-ary piecewise linear
functions over the factorials, where T is strictly dominating and has only
unit coefficients. There exists finite A containedin N including (k+8)!!
such that min(S1A),...,min(SnA) in A U. TA.

Note that if we remove "including (k+8)!!" then these Propositions are
easily provable in EFA.

We don't yet have a good feel for the (k+8)!! that appears at the end.
Certainly (k+8)!! needs to be made more beautiful. We have picked a safe
expression, but intend to reduce it considerably. In any case, this will be
gone into in detail at the appropriate time, which is not now.

By the Presburger decision procedure, or by more direct methods, we see
that strict domination of T is a finitary attribute. In addition, we can
replace N by [0,alpha]. where alpha is the next factorial after the
coefficients in the S's and (k+8)!!. Thus we see that Propositions 1,2 are
explicitly Pi-0-1.

THEOREM. Propositions 1,2 are each provably equivalent to the consistency
of MAH over ACA.

Speaking of Presburger, the results hold even if we replace "piecewise
linear" with "Presburger".

How do these results fit in to the development of Boolean relation theory?

The results here are quite different than the earlier clear milestone
reached in Posting # 126, Sat, 9 Mar 2002 02:10:12. The results in #126
were the subject of the "beautiful" reactions I reported, with the
classification of the 81^2 pairs of clauses. There one has a "beautiful"
category of statements, no one of which is especially natural, but where
only one, up to symmetry, is independent of ZFC.

The results in this posting is an attempt to do two things at once:

a) to give explicitly finite independence results;
b) to give a single statement that conveys specific interseting or
intriguing or otherwise notable information.

Obviously neither #126 nor #136 is yet obsolete.

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

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

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