[FOM] 194:PL Statement/clarification

Sun Nov 2 20:10:02 EST 2003

WE CORRECT SOME TYPOS AND UNCLEAR TERMINOLOGY IN POSTING #194.

########

BRT suggests a very large and varied field of investigation, with points of
contacts all over mathematics, where most problems can be solved very
constructively, but some problems can be solved only by using large
cardinals. Generally speaking, statements are not, in and of themselves,
more natural than other related statements. That is why it was so vital to
go in the direction of classifications - the 6561 classification being very
successful. 

One still would like to find particularly well motivated individual
statements (discrete/finite) that requires large cardinals - independently
of whether they are suggestive of a massive theory such as BRT. This would
complement the BRT developments.

I have been juggling a lot of leads for reaching new levels in this second
search - the search for particularly well motivated individual statements.

After a few weeks of hectic efforts, I now believe that the current state of
the art is through the following piecewise linear approach.

We start with the equation

A U. T[Ak] = N

which in our context has a unique solution A containedin N.

We then wish to say that

A U. T[Ak] is large.

Obviously this is a weaker condition. But we also want to say something
about A. Thus we say

A is somewhat large and A U. T[Ak] is large.

This can be solved, but only using large cardinals.

The somewhat largeness of A is straightforward: just that some factorials
lie in A. The largeness of A U. T[Ak] is rather subtle. It says that some
integers built out of A lie in A U. T[Ak].

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

Let N be the set of all nonnegative integers. T:Nk into N is said to be
strictly dominating if and only if for all x in Nk, T(x) > max(x).

We write A U. B for A U B if A,B are disjoint; undefined otherwise.

THEOREM 1. Let k >= 1 and T:Nk into N be strictly dominating. There exists a
unique A containedin N such that A U. T[Ak] = N.

We say that T:Nk into N is piecewise linear if and only if T is defined by
finitely many cases, each case given by a finite set of linear inequalities,
where in each case T is given by an affine expression. We will be concerned
with the coefficients used throughout this presentation of T.

PROPOSITION 2. Let T:Nk into N be strictly dominating. There exists A
containedin N such that A U. T[Ak] contains the minimum value over Ak of any
piecewise linear function with coefficients among 0,1 and the infinitely
many factorials in A.

PROPOSITION 3. Let k >= 1 and T:Nk into N be a strictly dominating piecewise
linear function with integer coefficients. There exists A containedin N such
that A U. T[Ak] contains the minimum value over Ak of any piecewise linear
function with coefficients from 0,1 and the infinitely many factorials in A.

PROPOSITION 4. Let k,p >= 1 and T:Nk into N be a strictly dominating
piecewise linear function with coefficients from {-k,...,k}. There exists
finite A containedin N such that A U. T[Ak] contains the minimum value over
Ak of any piecewise linear function with coefficients from 0,1 and the
subset {(8k)!!!,(8k+1)!!!,...,p!!!} of A.

We can obviously bound the largest element of A in terms of k and the
largest element of E. This results in an explicitly Pi01 statement.

Proposition 2 is provably equivalent, over ACA, to the 1-consistency of
Mahlo cardinals of finite order. Propositions 3 and 4 are provably
equivalent, over ACA, to the consistency of Mahlo cardinals of finite order.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 194th in a series of self contained numbered postings to
FOM covering a wide range of topics in f.o.m. The list of previous
numbered postings #1-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM

Harvey Friedman

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom