FOM: 145:BRT/A U. B U. TB/simplification/new chapter

[Harvey Friedman]

This simplified version gets rid of a whole clause, and is clearly much
better when using U. (disjoint union) rather than Delta (symmetric
difference). It is a relief to finally see that one is better than the
other, so that I do not have to continue mentioning both formulations!

I also now see that one can very naturally adjust the NUMERICAL hypothesis
and get a huge variety of logical strenghts, from Z_2,Z_3,..., to around Z,
ZFC, Mahlo, 2-Mahlo, 3-Mahlo, etcetera. See "NEW CHAPTER" below.

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

I am still trying to run out of ideas.

This posting is self contained.

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

*PRELIMINARIES*

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 write f' for the upper restriction of f, which is f restricted to {x:
f(x) > max(x)}.

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

As background, we mention the following versions of the Complementation
theorem, provable in RCA0.

COMPLEMENTATION. Let k >= 1 and f:N^k into N. There exists B containedin N
such that B U. f'B = N.

In fact there is a unique solution A to the set equation, and that unique
solution A is infinite.

Let E containedin N. We write E* for the set of all finite sequences from
E, including the empty sequence.

Let f:N^k into N and x in N^p, where 0 <= p <= k-1. Then we write f_x:N^k-p
into N for the cross section of f at x, where f_x(y) = f(x,y). It is
natural to extend this definition to all x in N* by taking f_x(y) =
f(x1,...,xk) in case the length of y is at least k. In this case, we think
of f_x as a 0-ary function; i.e., a constant.

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.

*FINITARY PROPOSITION*

PROPOSITION 1. Let T be a piecewise linear transformation over N and A be a
finite set of sufficiently large double factorials. There exists finite B
containedin N such that for all x in A*, min T_x B in A U. B U. T'B.

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

If we replace A U. B U. T'B by B U. T'B then the Proposition is easily
proved in EFA (exponential function arithmetic).

In Propositions 1,2, we can find a triple exponential expression alpha(|T|)
so that we can replace "sufficiently large" by r > alpha(|T|), and N by
[0,alpha(|T|)], where |T|
is the maximum of the arity and the coefficients used in the presentation
of T. This results in statements with the same metamathematical status as
Propositions 1,2. This results in explicitly Pi-0-1 statements with the
same metamathematical status as Propositions 1,2.

The double powers of 2 can be used instead of the double factorials.

NOTE 1: MAH is ZFC + {there exists a k-Mahlo cardinal}_k. RCA0 is the
current base theory for reverse mathematics (recursive comprehension axiom
naught). EFA is exponential function arithmetic. For RCA0, see Stephen G.
Simpson's book on Reverse Mathematics (SOSOA). EFA is essentially the same
as ISigma0(exp): see Hajek and Pudlak, Metamathematics of First Order
Arithmetic. For MAH, see Aki Kanamori, The Higher Infinite.

*NEW CHAPTER*

It appears that we can place restrictions on the "finite set of
sufficiently large double factorials" so that the Proposition has various
levels of strength below that of Mahlo cardinals of all finite orders.

For instance, it appears that if we use only sets of the form [n,n!]!! =
{n!!,(n+1)!!,...,n!!!|, then we get something right around the level of the
consistency of Z_2 (second order arithmetic). I.e.,

PROPOSITION 2. Let T be a piecewise linear transformation over N and r be a
sufficiently large integer. There exists finite B containedin N such that
for all x in [r,r!]!!*, min T_x B in [r,r!]!! U. B U. T'B.

If we use [r,r!!]!! then this is around the level of the consistency of
Z_3.  Each additional factorial goes up one in Russell's type theory.

If we use [r,!^r(r)]!! then we get something around the level of the
consistency of Zermelo set theory. Here !^r(r) is r with r factorials.

If we use [r,A(r)]!!, where A(r) is the Ackermann function at r, then we
get something between the consistency of ZFC and the consistency of ZFC +
there exists an inaccessible cardinal.

If we use [r,f_j(r)]!!, where f_1,f_2,... is the natural cofinal sequence
through the provably recursive functions of PA (Peano arithmetic), then we
climb cofinally through the consistency of MAH.

*COMPARISON WITH DISJOINT UNION INCLUSION WORK*

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 interesting or
intriguing or otherwise notable information.

Obviously neither #126 nor #144 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 145th 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