FOM: 147:Another Way

Harvey Friedman friedman at
Mon Apr 22 07:21:23 EDT 2002

We have discovered another way to obtain explicitly Pi-0-1 independence
results at the level of Mahlo cardinals of finite order that is closely
connected with the work in posting 126, which continues to be the state of
the art work on discrete independence results at the level of Mahlo
cardinals of finite order.

The present method has its advantages. One of the strongest aspects of the
work in posting 126 is the complete classification of all 81^2 pairs of
statements. This classification aspect is preserved in the present


We let N be the set of all nonnegative integers.

Let f:N^k into N be partially defined. For B containedin N we write fB for
the set of all values of f at arguments from B.

We use U. for disjoint union. I.e., when we write A U. B we mean A U B
together with the assertion that A,B are mutually disjoint.

We say that f is strictly dominating if and only if for all x in N^k, f(x)
> max(x).

A k-ary piecewise linear transformation over N is a function of the form
T:N^k into N such that there is a partition of N^k into finitely many
pieces, where each piece is given by a finite set of linear inequalities
with coefficients from N, and where f agrees with an affine function with
coefficients from N on each piece.

The nonnegativity of the coefficients has a major effect on the affine
functions, but no effect on the linear inequalities. This is because
shifting terms from one side to the other in linear inequalities has the
effect of taking negatives of coefficients.

Recall the following from posting 126.

PROPOSITION 1. For all multarivate 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. gB containedin C U. gC.

We also have

PROPOSITION 2. For all strictly dominating piecewise linear transformations
S,T over N, there exists infinite A,B,C containedin N such that
A U. SA containedin C U. TB
A U. SB containedin C U. TC.

We can make a finite statement out of Proposition 2 by requiring that A,B,C
be "tame" infinite subsets of N. I.e., A,B,C are sets that fall within the
purview of extensions of Presburger arithmetic that have a known quantifier
elimination. I.e., add base 2 exponentiation to Presburger arithmetic. Here
we use finite A,B,C.

PROPOSITION 3. For all strictly dominating piecewise linear transformations
S,T over N, there exists finite A,B,C containedin N containing any given
finite set of sufficiently large double factorials, such that
A U. SA containedin C U. TB
A U. SB containedin C U. TC.

>From posting 126, Proposition 1 is provably equivalent to 1-Con(MAH) over ACA.

NOTE: This Proposition 3 is obviously closely related to a number of
earlier versions of finite forms posted on the FOM soon after posting 126,
but is cleaner and more readily digestible. Also, we can replace double
factorials by any sufficiently spread apart set. We can also rephrase
Proposition 2 involving sufficient spread apart sets, but this seems to add
complexity to the statement.

THEOREM. Propositions 2,3 are provably equivalent to Con(MAH) over ACA.

Furthermore, we can place explicit double exponential bounds in Proposition
3 to get an explicitly Pi-0-1 sentence as follows. Firstly, by using the
Presburger decision procedure, or more direct methods, one sees that T is
strictly dominating if and only if T is strictly dominating on all
arguments bounded by a number depending only on the largest coefficient
used in the presentation of T. Also, an upper bound can be placed on
"sufficiently large" depending only on the largest coefficient used in the
presentation of T. Also there is an obvious upper bound for A,B,C. These
bounds are double exponential in the data (undoubtedly they can be made
much better, as we shall see when doing the writing).

In addition, we can perform the analogous classification study that we
reported on in posting 126. We also have that, up to symmetry of A,B,C,
there is exactly one case out of 81^2 that is not decided within RCA0:
namely, the one displayed, which corresponds to Mahlo cardinals in the
manner indicated.

Moreover, we can weaken "any given finite set of sufficiently large double
factorials" in the manner discussed in posting 145 in order to gain control
of the strength of the statement, hitting various important levels on or
nearly on the button such as Zermelo and ZFC.



I use for manuscripts with
proofs. Type Harvey Friedman in the window.

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

More information about the FOM mailing list