FOM: 84:BRT/First Major Classification
Harvey Friedman
friedman at math.ohio-state.edu
Mon Mar 27 04:04:08 EST 2000
We present our first major classification result for Boolean Relation
Theory. We expect that it will be the first of many such classification
results.
PLAN: This announcement properly launches the subject of Boolean relation
theory, except for the missing discussion of the critical elegant
example(s) of Boolean relations that necessarily require large cardinals to
handle. That will be the topic of the next posting on BRT. As promised in
earlier postings, now that this much of the dust has settled, the key
claims about the critical elegant example will be carefully checked. In
particular, the sufficiency of large cardinals for handling the critical
elegant example has been written down and gone over in the local seminar.
The corresponding neccessity is now the critical matter to be written and
checked in the local seminar this spring quarter.
1. INITIAL BOOLEAN RELATION THEORY CONTEXT.
Let us recall the initial context for BRT that we have been focusing on. In
this minute corner of BRT, we seek to classify all statements of the
following form:
1) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite sets A_1,A_2,A_3 containedin N such that
A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a given Boolean equation.
Here fA is defined to be the set of all values of f at arguments from A.
Expansive linear growth means that there are rational constants c,d > 1
such that the inequality
c|x| <= f(x) <= d|x|
holds with at most finitely many exceptions, where |x| is the maximum
coordinate of x (sup norm of x).
A Boolean equation among sets is an equation between terms involving the
sets, union, intersection, and complement. Complementation throws us into
proper classes, but this is no cause for concern, and can be removed by
taking complements with respect to a universal set in the standard way
(which in our case is N).
As we emphasized in earlier postings on BRT, there is a particular elegant
instance of these problems for which it is necessary and sufficient to use
Mahlo cardinals of finite order to prove.
**In the next posting on BRT, I will present and discuss such elegant
instances. **
A complete classfication of these finitely many questions (with no pruning,
2^2^9), is going to take more time. So we have been feverishly working on a
suitably strong restricted classification result, which we now present.
2. RESTRICTED CLASSIFICATION PROBLEM.
As we said in earlier postings on BRT, every Boolean equation in sets
E_1,...,E_n can be equivalently written as a set of basic inclusions, where
the left side is a finite intersection of the E's and the right side is a
finite union of the E's. Here the convention is that if the right side is
the empty union then the right side is the empty set, and if the left side
is the empy intersection then the left side is the universal set (which, in
the case we are interested in, is N). This is a fundamental well known fact
from formal Boolean algebra.
Thus we can restate the fundamental classification problem 1) as:
2) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite sets A_1,A_2,A_3 containedin N such that
A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a given set of basic
inclusions.
A bit less ambitious but nearly as fundamental a classification problem is:
3) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite sets A_1 containedin A_2 containedin A_3
containedin N such that A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a
given set of basic inclusions.
Imposing the condition
A_1 containedin A_2 containedin A_3
is tantamount to requiring that
A_1 containedin A_2, A_2 containedin A_3
lie in the given set of basic inclusions.
Classification problem 3) is also going to take more time. We announce a
solution to the following restricted classification problem.
An exclusion among the nine terms A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3
is a condition
s intersect t = emptyset
where s,t are among the above nine terms.
A covering among the above nine terms is a condition
s containedin t_1 union .... union t_n
where 1 <= n <= 9 and s,t_1,...,t_n are among the above nine terms.
A forward covering among the above nine terms is a covering among the above
nine terms in which the subscript appearing on the left side is strictly
smaller than all subscripts appearing on the right side. Note that every
one of the nine terms uses exactly one subscript among the integers 1,2,3.
Here is the restricted classification problem that we have been able to solve:
4) For all multivariate functions f,g from N into N of expansive linear
growth, there exist infinite sets A_1 containedin A_2 containedin A_3
containedin N such that A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a
given set of exclusions and forward coverings.
Informally, the first essential point about this classification is that it
was accomplished using large cardinals - which go well beyond the usual
axioms of mathematics such as those formalized by ZFC - and cannot be
accomplished without using large cardinals. This is precisely formulated as
follows.
Let MAH be the formal system ZFC + {there exists an n-Mahlo cardinal}_n.
Let MAH+ be the formal system ZFC + (forall n)(there exists an n-Mahlo
cardinal).
THEOREM 1. Every instance of 4) is provable or refutable in MAH+. Not every
instance of 4) is provable or refutable in MAH (assuming MAH is
2-consistent).
We can give more precise information.
THEOREM 2. Every instance of 4) is either refutable in RCA_0 or provable in
ZFC + 1-Con(MAH). Let T be an extension of RCA_0 such that every instance
of 4) is provable or refutable in T. Then T proves or refutes 1-Con(MAH).
If T proves 1-Con(MAH) then every instance of 4) is provable or refutable
in T.
3. CRITICAL FEATURES OF THE RESTRICTED CLASSIFICATION.
We now present critical features of the restricted classification as
Propositions. Informally, we can prove all of these results using large
cardinals, and they cannot be proved without using large cardinals.
PROPOSITION 3. Any instance of 4) holds if and only if it holds with
"multivariate" replaced by "binary."
PROPOSITION 4. Any instance of 4) holds if and only if it holds with
"infinite" replaced by any of the following:
i) nonempty;
ii) nonempty finite;
iii) arbitrarily large finite.
We also have the hybrid statement:
PROPOSITION 5. Any instance of 4) holds if and only if it holds with
"multivariate" replaced by "binary" and "infinite" replaced by any of the
following:
i) nonempty;
ii) nonempty finite;
iii) arbitrarily large finite.
We remark that it is quite straightforward to prove that if a given
instance of 4) holds then it holds with "infinite"
replaced by "arbitrarily large finite."
Note that among Propositions 3-5 there are a total of seven equivalences.
THEOREM 6. Each of these seven equivalences can be proved in MAH+ but not
in MAH (assuming MAH is consistent).
4. REFORMULATION IN TERMS OF EQUIVALENT CLASSIFICATIONS.
There is another way of stating the results in section 3. There we have in
essence considered some related classification problems, and shown their
equivalence using large cardinals. To organize these related problems, we
define
MELG = the set of all multivariate functions from N into N of expansive
linear growth.
BELG = the set of all binary functions from N into N of expansive linear
growth.
INF = the family of all infinite subsets of N.
NON = the family of all nonempty subsets of N.
NONF = the family of all nonempty finite subsets of N.
We consider the classification problem
5) For all f,g in MELG,BELG, there exist A_1 containedin A_2 containedin
A_3 from INF,NON,NONF, such that A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3
obeys a given set of exclusions and forward coverings.
Note that there are six forms of 5).
Informally, it is necessary and sufficient to use large cardinals in order
to classify 5) using (MELG,INF). Large cardinals are not needed for the
remaining five forms of 5).
THEOREM 7. Every instance of 5) using
(MELG,NON),(MELG,NONF),(BELG,INF),(BELG,NON),(BELG,NONF) is provable or
refutable in RCA_0. It is provable in RCA_0 that 5) using
(MELG,NON),(MELG,NONF),(BELG,INF),(BELG,NON),(BELG,NONF) have exactly the
same corresponding true instances.
THEOREM 8. Every instance of 5) using (MELG,INF) is provable or refutable
in MAH+. It is provable in MAH+ that 5) using (MELG,INF) and 5) using
(BELG,NON) have the same corresponding true instances. However, in the
first claim, MAH+ cannot be replaced by MAH (assuming MAH is 2-consistent),
but can be replaced by ZFC + 1-Con(MAH). In the second claim, MAH+ cannot
be replaced by MAH (assuming MAH is consistent), but can be replaced by ZFC
+ 1-Con(MAH).
THEOREM 9. Let T be a theory extending RCA_0. If If we can replace MAH+ by
T in the first sentence of Theorem 8 then T proves or refutes 1-Con(MAH).
The statement "5) using (MELG,INF) and 5) using (BELG,NON) have the same
corresponding true instances" is provable equivalent to 1-Con(MAH) over
RCA_0.
5. HALF CONCRETE FORMULATIONS.
The most common concern expressed by some mathematicians is that an
arbitrary multivariate function from N into N is uncomfortably wild, and
they would prefer that one use concrete functions. This issue was addressed
in posting #83, Tame Boolean Relation Theory, where a number of classes of
tame functions and tame sets were considered. We present an improved
development.
Among mathematicians expressing this concern about the functions, most of
them are relatively comfortable with asking for infinite sets of natural
numbers. For such mathematicians, half concrete formulations are most
relevant, where the functions are concrete but the sets of natural numbers
are arbitrary.
We say that a multivariate function from N into N is piecewise linear if
and only if it it defined by finitely many cases in the following way. Each
case is given by a finite set of linear inequalities with integer
coefficients, and the function is defined in that case by an affine
expression with integer coefficients.
We emphaisize that integer coefficients are to be used throughout the
presentation of a multivariate piecewise linear function from N into N.
This is automatic for the affine expressions, but not automatic for the
division into cases.
We say that f is expansive if and only if there is a rational constant c >
1 such that the inequality
c|x| <= f(x)
holds with at most finitely many exceptions, where |x| is the maximum
coordinate of x (sup norm of x).
We define
MEPL = the set of all multivariate functions from N into N that are
expansive and piecewise linear.
BEPL = the set of all binary functions from N into N that are expansive and
piecewise linear.
We consider the half concrete classification problem
6) For all f,g in MEPL,BEPL there exist A_1 containedin A_2 containedin
A_3 from INF,NON,NONF such that A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3
obeys a given set of exclusions and forward coverings.
Note that there are six forms of 6).
Informally, it is necessary and sufficient to use large cardinals in order
to classify 6) using (MEPL,INF). Large cardinals are not needed for the
remaining five forms of 6).
THEOREM 10. Theorems 7-9 hold if 5) is replaced by 6), MELG is replaced by
MEPL, BELG is replaced by BEPL, and 1-Con(MAH) is replaced by Con(MAH).
THEOREM 11. It is provable in RCA_0 that 5) using (BELG,NON) and 6) using
(BEPL,NON) have the same corresponding true instances.
THEOREM 12. It is provable in MAH+ that 5) using (MELG,INF) and 6) using
(MEPL,INF) have the same corresponding true instances. This equivalence is
not provable in MAH (assuming MAH is 2-consistent). In fact, this
equivalence is provably equivalent to "if Con(MAH) then 1-Con(MAH)" over
RCA_0.
6. FULLY CONCRETE FORMULATIONS.
For some mathematicians, the use of arbitrary infinite sets of natural
numbers is objectionable. Fully concrete formulations are needed to meet
their objections. Finite formulations meet their objections even more
forcefully; see section 7.
We use the following family of concrete subsets of N:
AFEXP = the family of all images of infinite geometric progressions in N
under multivariate piecewise linear maps from N into N.
There is a straightforward decision procedure for testing membership in a
given element of AFEXP.
We now consider the classification problem
7) For all f,g in MEPL,BEPL there exist A_1 containedin A_2 containedin A_3
from AFEXP, such that A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a
given set of exclusions and forward coverings.
Then AFEXP in 7) behaves exactly like INF in 6). Informally, it is
necessary and sufficient to use large cardinals in order to classify 7)
using (EMPL,AFEXP). Large cardinals are not needed for 7) using
(BEPL,AFEXP).
In the instances of 7) using (MEPL,AFEXP) we can look for an upper bound on
the integers involved in the AFEXP presentation as a function of the
integers involved in the MEPL presentation. We can show that there is a
double exponential bound. Therefore, the classification of 7) using
(MEPL,AFEXP) involves necessary and sufficient uses of large cardinals even
though large growth rates are not involved.
7. FORMAL INEQUALITY THEORY.
Formal inequality theory will be combined with Boolean relation theory in
section 8. However, formal inequality theory is of obvious interest in its
own right.
Let f_1,...,f_k be multivariate functions from N into N and E_1,...,E_r be
subsets of N. We consider the formal inequalities that hold of the system
f_1,...,f_k,E_1,...,E_r in a certain precise sense.
We use variables x_1,x_2,... ranging over N. A formal inequality is an
assertion of the following form. Let x_1,...,x_p be elements of N
satisfying a finite set of conditions of the forms
i) x_i < x_j;
ii) x_i <= x_j;
iii) x_i in E_j.
Then an inequality of the forms
iv) f_i(x*) < f_j(x**);
v) f_i(x*) <= f_j(x**).
holds. Here x*,x** are sequences of variables among x_1,...,x_p of the
required lengths.
The first order of business of formal inequality theory is to solve the
following classification problem:
a) For all multivariate functions f_1,...,f_k from N into N there exists
infinite E_1,...,E_r containedin N such that f_1,...,f_k,E_1,...,E_r obeys
a given set of formal inequalities.
We can completely solve this problem with an intense use of the classical
infinite Ramsey theorem. Moreover, we can also solve the augmented problem
b) For all multivariate functions f_1,...,f_k from N into N there exists
infinite E_1,...,E_r containedin N such that f_1,...,f_k,E_1,...,E_r,N
obeys a given set of formal inequalities.
BACKGROUND: If we place a bound on a single function f and a single finite
set E, then we run right out of PA = Peano Arithmetic, with fast growing
functions, etcetera. For example, consider the following two theorems:
THEOREM A. Let n >> k and F:[0,n]^k into [0,n] obey the inequality
F(x_1,...,x_k) <= max(x_1,...,x_k). Then there exists x_1,...,x_k+2 <= n
such that F(x_1,...,x_k) <= F(x_2,...,x_k+1) <= F(x_3,...,x_k+2).
THEOREM B. Let n >> k and F,G:[0,n]^k into [0,n] obey the inequality
F(x_1,...,x_k),G(x_1,...,x_k) <= max(x_1,...,x_k). Then there exists
x_1,...,x_k+1 <= n such that F(x_1,...,x_k) <= F(x_2,...,x_k+1) and
G(x_1,...,x_k) <= G(x_2,...,x_k+1).
THEOREM C. Theorems A,B are independent of PA. They are equivalent to
1-Con(PA) over EFA. The growth rates are at the level epsilon_0 in the
usual hierarchies.
END OF BACKGROUND.
8. FINITE BOOLEAN RELATION THEORY.
We had made some remarks in earlier postings about finite Boolean relation
theory which are now obsolete. We start again.
The most obvious beginning of finite Boolean relation theory is to consider
the classification problem
8) For all f,g in MELG there exist arbitrarily large finite A_1 containedin
A_2 containedin A_3 containedin N such that
A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a given set of exclusions
and forward coverings.
However, we have solved this classification problem totally within the weak
theory RCA_0, and it comes out the same as all of the other classfications
in this abstract.
We run right into large cardinals when we combine finite Boolean relation
theory with formal inequality theory. In fact, consider the following
classification problem
9) For all f,g in MELG there exist arbitrarily large finite A_1 containedin
A_2 containedin A_3 containedin N such that
A_1,A_2,A_3,fA_1,fA_2,fA_3,gA_1,gA_2,gA_3 obeys a given set of exclusions
and forward coverings and four variable formal inequalities.
I expect to be able to handle this classification, too - formal inequality
theory is much easier than Boolean relation theory.
The crucial point is that there is a specific elegant instance of 9) which
is a necessary use of large cardinals. In fact, the large cardinals
necessary here are somewhat bigger - the subtle cardinals of finite order.
We finally come to the question of estimates in 9). An upper bound on the
elements of A_3 can be given in terms of the arity of f,g, the constants
used in the expansive linear growth inequalities, and the location of the
exceptions - and this upper bound is roughly akin to the iterated
exponential upper bounds in the classical infinite Ramsey theorem. Thus we
have explicitly Pi-0-1 statements.
Furthermore, we can use MEPL instead of MELG. We run right into these same
subtle cardinals of finite order. However, here the relevant upper bounds
can be taken to be double exponential.
**********
This is the 84th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:
1:Foundational Completeness 11/3/97, 10:13AM, 10:26AM.
2:Axioms 11/6/97.
3:Simplicity 11/14/97 10:10AM.
4:Simplicity 11/14/97 4:25PM
5:Constructions 11/15/97 5:24PM
6:Undefinability/Nonstandard Models 11/16/97 12:04AM
7.Undefinability/Nonstandard Models 11/17/97 12:31AM
8.Schemes 11/17/97 12:30AM
9:Nonstandard Arithmetic 11/18/97 11:53AM
10:Pathology 12/8/97 12:37AM
11:F.O.M. & Math Logic 12/14/97 5:47AM
12:Finite trees/large cardinals 3/11/98 11:36AM
13:Min recursion/Provably recursive functions 3/20/98 4:45AM
14:New characterizations of the provable ordinals 4/8/98 2:09AM
14':Errata 4/8/98 9:48AM
15:Structural Independence results and provable ordinals 4/16/98
10:53PM
16:Logical Equations, etc. 4/17/98 1:25PM
16':Errata 4/28/98 10:28AM
17:Very Strong Borel statements 4/26/98 8:06PM
18:Binary Functions and Large Cardinals 4/30/98 12:03PM
19:Long Sequences 7/31/98 9:42AM
20:Proof Theoretic Degrees 8/2/98 9:37PM
21:Long Sequences/Update 10/13/98 3:18AM
22:Finite Trees/Impredicativity 10/20/98 10:13AM
23:Q-Systems and Proof Theoretic Ordinals 11/6/98 3:01AM
24:Predicatively Unfeasible Integers 11/10/98 10:44PM
25:Long Walks 11/16/98 7:05AM
26:Optimized functions/Large Cardinals 1/13/99 12:53PM
27:Finite Trees/Impredicativity:Sketches 1/13/99 12:54PM
28:Optimized Functions/Large Cardinals:more 1/27/99 4:37AM
28':Restatement 1/28/99 5:49AM
29:Large Cardinals/where are we? I 2/22/99 6:11AM
30:Large Cardinals/where are we? II 2/23/99 6:15AM
31:First Free Sets/Large Cardinals 2/27/99 1:43AM
32:Greedy Constructions/Large Cardinals 3/2/99 11:21PM
33:A Variant 3/4/99 1:52PM
34:Walks in N^k 3/7/99 1:43PM
35:Special AE Sentences 3/18/99 4:56AM
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/17/99 1:32PM
61:Finitist proofs of conservation 9/29/99 11:52AM
62:Approximate fixed points revisited 10/11/99 1:35AM
63:Disjoint Covers/Large Cardinals 10/11/99 1:36AM
64:Finite Posets/Large Cardinals 10/11/99 1:37AM
65:Simplicity of Axioms/Conjectures 10/19/99 9:54AM
66:PA/an approach 10/21/99 8:02PM
67:Nested Min Recursion/Large Cardinals 10/25/99 8:00AM
68:Bad to Worse/Conjectures 10/28/99 10:00PM
69:Baby Real Analysis 11/1/99 6:59AM
70:Efficient Formulas and Schemes 11/1/99 1:46PM
71:Ackerman/Algebraic Geometry/1 12/10/99 1:52PM
72:New finite forms/large cardinals 12/12/99 6:11AM
73:Hilbert's program wide open? 12/20/99 8:28PM
74:Reverse arithmetic beginnings 12/22/99 8:33AM
75:Finite Reverse Mathematics 12/28/99 1:21PM
76: Finite set theories 12/28/99 1:28PM
77:Missing axiom/atonement 1/4/00 3:51PM
78:Qadratic Axioms/Literature Conjectures 1/7/00 11:51AM
79.Axioms for geometry 1/10/00 12:08PM
80.Boolean Relation Theory 3/10/00 9:41AM
81:Finite Distribution 3/13/00 1:44AM
82:Simplified Boolean Relation Theory 3/15/00 9:23AM
83: Tame Boolean Relation Theory 3/20/00 2:19AM
More information about the FOM
mailing list