FOM: 83:Tame Boolean Relation Theory
Harvey Friedman
friedman at math.ohio-state.edu
Mon Mar 20 02:19:56 EST 2000
CAUTION: As I have emphasizing, things have not settled down enough for
serious checking. I am in the middle of the partial classification, and
after that is announced, the crucial reversal of the simple instance of BRT
will be gone over in the local Seminar. The proof using Mahlo cardinals of
the simple instance of BRT has been gone over in the local Seminar, and
there is a writeup of that.
***********************************
1. BRT SUMMARY. As discussed in postings #80 and 82, Boolean relation
theory concerns pairs (V,K), where V is a set of multivariate functions and
K is a family of sets. For each n,m >= 1, we seek to determine the truth or
falsity of the statements
#) For all f_1,...,f_n in V there exists A_1,...,A_m in K such that a given
Boolean relation holds of the (1+n)m sets
A_1,...,A_m,f_1A_1,...,f_1A_m,...,f_nA_1,...,f_nA_m.
In equational Boolean relation theory, the Boolean relations are just
equations between Boolean expressions. Technically speaking, the use of
complementation runs creates proper classes, but this is not important and
can be trivially removed if desired by choosing an appropriate universal
set.
In general Boolean relation theory, one allows propositional combinations
of Boolean equations, and even more generally, the Boolean equations can
involve arbitrary compound expressions (see gBes's in posting #80).
In this posting, we confine ourselves to equational Boolean relation theory.
We have been focusing on the following special case of BRT (Boolean
relation theory). V is the set of all multivariate functions from N into N
of expansive linear growth. K is the family of all infinite subsets of N.
Also n = 2, m = 3.
We are morally certain that it is necessary and sufficient to use Mahlo
cardinals of finite order in order to determine the truth or falsity of all
statements of the form
*) For all f,g in V there exists A,B,C in K such that a given Boolean
equation holds of A,B,C,fA,fB,fC,gA,gB,gC.
We guess that this result will be obtained within two years of work. We
already know the necessity.
We have already shown that it is necessary to use Mahlo cardinals of finite
order in order to determine even the truth or falsity of a particular
elegant instance of *). For future reference, we state this as a theorem.
THEOREM A. There is a particular instance of *) that can be proved in ZFC
with Mahlo cardinals of all finite orders but not with Mahlo cardinals of
any particular finite order. In fact, we get equivalence with the
1-consistency of ZFC + Mahlo cardinals of each finite order.
We are finishing up a good partial classification result, where we show
that it is necessary and sufficient to use Mahlo cardinals of finite order
to handle a significant fragment of *) which we expect to announce soon.
2. SOME DEFINABLE BOOLEAN RELATION THEORY.
Let M,M' be relational structures on N. We can consider
**) For all M-definable multivariate f,g of expansive linear growth there
exists infinite M'-definable A,B,C containedin N such that a given Boolean
equation holds of A,B,C,fA,fB,fC,gA,gB,gC.
THEOREM B. Let M = M' be the semiring (N,+,x). There is a particular
instance of **) that can be proved in ZFC with Mahlo cardinals of all
finite orders but not with Mahlo cardinals of any particular finite order.
In fact, we get equivalence with the 1-consistency of ZFC + Mahlo cardinals
of each finite order.
It is well known that definability in the semiring (N,+,x) and its
expansions is very very wild.
3. SOME TAME BOOLEAN RELATION THEORY.
The most familiar substantial tame relational structure on N is the
semigroup (N,+).
THEOREM C. Let M = (N,+) and M' = (N,+,x). There is a particular instance
of **) that can be proved in ZFC with Mahlo cardinals of all finite orders
but not with Mahlo cardinals of any particular finite order. In fact, we
get equivalence with the consistency of ZFC + Mahlo cardinals of each
finite order. Moreover, these results hold if we remove M'-definable from
**).
Note that C is only half tame. If we use M = M' = (N,+) then we are morally
certain that all instances of **) can be settled in RCA_0.
I have known for some time that in the case of my favorite instance of **)
with M = (N,+) and M' = (N,+,x), the sets A,B,C constructed with the
necessary help of Mahlo cardinals of finite order are very simple - far
simpler than merely being M'-definable . But not as simple as being
definable in M.
In fact, I have known for some time that they are definable in (N,+,2^n).
I.e., definable in the semigroup with base 2 exponentiation added. But I
subconsciously thought that definability in (N,+,2^n) is awkward,
uninteresting, and wild.
It suddently dawned on me that structures such as (N,+,2^n) might be really
interesting, because they might be tame.
I called Lou and found out, to my great delight, that (N,+,2^n) had in fact
been proved to be tame. Lou told me about a 47 page manuscipt dated 1988 in
German of Dorte Gotsch, with doubledots over the o's, containing a proof of
quantifier elimination for (N,+,2^n) using the following symbols.
1. <,+,0,1,2^n.
2. cutoff subtraction, -*.
3. for each n >= 2, divisibility by n.
4. the function log*(n) = the greatest integer m such that 2^m <= n for n
>= 1; log*(0) = 0.
I.e., in the structure (N,<,+,0,1,2^n,-*,log*,2|x,3|x,...), every formula
is equivalent to a quantifier free formula.
I'm not sure just who first proved this, since this 1988 paper refers to an
earlier 1986 paper of Cherlin and Point, On extensions of Presburger
arithmetic (which I can't find in my library) where the Zentralbatt review
indicates that this 1986 paper gives a detailed proof of a much more
general result of Sememov.
THEOREM D. Let M = M' = (N,+,2^n). There is a particular instance of **)
that can be proved in ZFC with Mahlo cardinals of all finite orders but not
with Mahlo cardinals of any particular finite order. In fact, we get
equivalence with the consistency of ZFC + Mahlo cardinals of each finite
order. The results also hold if we use M = (N,+) and M' = (N,+,2^n).
Note the following added bonus that we get from Theorem D. There are no
quantifiers over infinite sets involved.
In fact, we can go further. There is a reasonable measure of how
complicated a given set definable in a structure on N is. Namely we look
for the least size of a formula that defines it, where we measure the size
by the number of symbols and the maximum size of any parameters used. We
can then place at most triple exponential bounds on these complexity
measures whenever an instance of **) is true in Theorem D. E.g., we can
establish that if any instance of **) in D is true then it is triple
exponentially true. This makes the necessary uses of Mahlo cardinals of
finite order directed at explicitly Pi-0-1 sentences.
4. EVEN TAMER.
A very important class of tame functions is the piecewise linear
multivariate functions from N into N. These are the functions defined by
finitely many cases, where
i) each case is given by a finite set of linear inequalities with integer
coefficients;
ii) the function in each case is given by a linear expression with integer
coefficients and integer constant term.
Let V' be the set of all such piecewise linear multivariate functions from
N into N which are of expansive linear growth.
Piecewise linearity is a stronger condition than definability in (N,+).
THEOREM E. Theorem D holds if we use V' instead of (N,+,2^n)-definable
multivariate functions from N to N of expansive linear growth. We still use
the infinite M'-definable sets.
5. LOGIC FREE TAMENESS.
Model theorists normally use definability in connection with tameness.
Obviously, by the very nature of tameness - in the sense used by model
theorists - one can use quantifier free definability (perhaps with
additional symbols). But for our purposes we would like an entirely logic
free formulation where a family of functions and a family of sets are used
that are simple, natural, and concrete.
We use the exponential polynomials. These are the least class of
expressions containing variables, the constants 0,1, and closed under
+,x,exponentiation. It is clear that each expression denotes an element of
N when the variables are assigned elements of N, except that a convention
must be established for 0^0, which should either be 0 or 1, and which
should be determined by, say, a vote of the FOM e-mail list subscribers
(smile).
The piecewise exponential multivariate functions from N into N are defined
by finitely many cases, where
i) each case is given by a finite set of exponential inequalities (i.e., s
< t, where s,t are exponential polynomials);
ii) the function in each case is given by an exponential polynomial.
The semiexponential subsets of N are taken to be the ranges of peicewise
exponential multivariate functions from N into N.
Since minus and division are not present, these ranges are well controlled.
In particular, there is an obvious algorithm for testing membership.
We now consider
***) For all peicewise exponential multivariate f,g of expansive linear
growth there exists infinite semiexponential A,B,C containedin N such that
a given Boolean equation holds of A,B,C,fA,fB,fC,gA,gB,gC.
THEROEM F. There is a particular instance of ***) that can be proved in ZFC
with Mahlo cardinals of all finite orders but not with Mahlo cardinals of
any particular finite order. In fact, we get equivalence with the
consistency of ZFC + Mahlo cardinals of each finite order. Furthermore the
result holds if we don't allow multiplication in the definition of
expoential polynomials, piecewise exponential functions, and
semiexponential sets.
We can again give an obvious complexity measure and provide explicit
estimates, thereby aiming the necessary and sufficient use of large
cardinals at Pi-0-1 targets.
**********
This is the 83rd 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
More information about the FOM
mailing list