FOM: 95:Boolean Relation Theory III
Harvey Friedman
friedman at math.ohio-state.edu
Tue Dec 19 19:29:44 EST 2000
This is a self contained update on Boolean Relation Theory taken from the
beginning. It supercedes postings #80 and #88.
I am now writing Boolean Relation Theory, opus 1. for publication. This
will have
i) a presentation of Boolean Relation Theory and its variants, including
disjoint cover theory and formal partition theory;
ii) discussion of the Thin Set Theorem and the Complementation Theorem,
including proofs, some variants, and counterexamples to variants;
iii) proof of the disjoint cover tower theorem for expansive linear growth
using Mahlo cardinals of finite order;
iv) proof of the disjoint cover tower theorem for expansive piecewise
polynomials using Mahlo cardinals of finite order;
v) reversal of the disjoint cover tower theorem for piecewise polynomials
of expansive linear growth to Mahlo cardinals of finite order;
vi) discussion of conjectures, and results to appear elsewhere.
BOOLEAN RELATION THEORY
by
Harvey M. Friedman
friedman at math.ohio-state.edu
www.math.ohio-state.edu/~friedman/
Extended Abstract
December 19, 2000
Boolean relation theory concerns the relationship between sets and their
images under multivariate functions. We give detailed formulations of
Boolean relation theory and its specializations.
1. EQUATIONAL, INEQUATIONAL, PROPOSITIONAL, BOOLEAN RELATION THEORY.
To avoid ambiguities in the general theory, we want every muiltivariate
function to have an unambiguous arity. Thus we say that f is a multivariate
function if and only if
i) f is a function; or
ii) f is a pair (g,k), where k >= 2 (the arity of f) and g is a function
whose domain is a nonempty set of ordered k-tuples.
In case ii), we write dom(f) for dom(g), and define f(x_1,...,x_k) =
g(<x_1,...,x_k>).
BRT is based on the following notion of forward image of a multivariate
function on a set. Let f be a multivariate function and A be a set. We
define fA = {f(x_1,...,x_k): k is the arity of f and x_1,...,x_k in A}.
We say that f is a multivariate function from nonempty A into B if and only if
dom(f) = A^k and rng(f) containedin B, where f is k-ary. The empty function
is a multivariate function of arity 1.
The set variables consist of A_1,A_2,... . The function variables consist
of f_1,f_2,... .
The Boolean expressions are inductively defined as follows:
i) emptyset, U, and each set variable are Boolean expressions;
ii) if s,t are Boolean expression then (s union t), (s intersection t), and
s' are Boolean expressions.
Here s' denotes the complement of s, and U denotes the universal set.
A Boolean equation is an equation s = t, where s,t are Boolean expressions.
A Boolean inequation is an inequation s not= t, where s,t are Boolean
expressions.
The propositional combinations of Boolean equations are obtained from the
Boolean equations through use of the usual propositional connectives.
Let V be a set of multivariate functions and K be a set of sets. Let n,m >= 1.
Equational (inequational, propositional) BRT on (V,K) of type (n,m) is the
study of all statements of the form
for all f_1,Š,f_n in V there exists A_1,Š,A_m in K such that a given
Boolean equation (Boolean inequation, propositional combination of Boolean
equations) holds in the m(n+1) sets
A_1,Š,A_m
f_1A_1,Š,f_1A_m
Š
f_nA_1,Š,f_nA_m.
Here we interpret the universal set U to be the union of K, and
complementation is taken relative to U.
The case n = m = 1 is the most elemental type, where we have a single
function and a single set. Here even equational BRT on (V,K) of type (1,1)
can be highly nontrivial.
The goal of equational (inequational, propositional) BRT on (V,K) of type
(n,m) is to determine the truth or falsity of all of its members. For a
given n,m >= 1, there are 2^2^m(n+1) elements of equational (inequational)
BRT on (V,K) of type (n,m), up to Boolean equivalence. There are
2^2^2^2^m(n+1) elements of propositional BRT on (V,K) of type (n,m) up to
Boolean/logical equivalence.
Note that equational BRT is fairly robust. I.e., any finite conjunction of
Boolean equations is equivalent to a single Boolean equation (formally, in
Boolean algebra), and inclusions between Boolean terms are equivalent to
single Boolean equations (again formally, in Boolean algebra).
2. EXTENDED EQUATIONAL, INEQUATIONAL, PROPOSITIONAL, BOOLEAN RELATION THEORY.
The extended Boolean expressions are defined inductively as follows:
i) emptyset, U, and each set variable are extended Boolean expressions;
ii) if s,t are extended Boolean expressions then so are (s union t), (s
intersect t), and s';
iii) if s is an extended Boolean expression and f is a function variable
then f(s) is an extended
Boolean expression.
An extended Boolean equation is an equation s = t, where s,t are extended
Boolean expressions.
An extended Boolean inequation is an inequation s not= t, where s,t are
extended Boolean expressions.
The propositional combinations of extended Boolean equations are obtained
from the extended Boolean equations through use of the usual propositional
connectives.
Let V be a set of multivariate functions and K be a set of sets. Let n,m >= 1.
Extended equational (inequational, propositional) BRT on (V,K) of type
(n,m) is the study of all statements of the form
for all f_1,Š,f_n in V there exists A_1,Š,A_m in K such that a given
extended Boolean equation (Boolean inequation, propositional combination of
Boolean equations) holds in the functions f_1,Š,f_n and the sets A_1,Š,A_m.
Extended equational (inequational, propositional) BRT on (V,K) is the union
over n,m >= 1 of extended equational (inequational, propositional) BRT of
type (n,m).
Note that there are infinitely many statements even in extended equational
BRT on (V,K) of type (1,1). However, we can introduce a new parameter for
the number of occurrences of functions (or function variables) in an
extended Boolean expression. We then have finitely many statements in the
extended theory of type (n,m).
3. THE THIN SET THEOREM.
We use Z for the set of all integers. An integral multivariate function is
a multivariate function from Z into Z.
Boolean relation theory begins with the thin set theorem. It is the most
basic interesting theorem in inequational Boolean relation theory. In fact,
it is a statement in inequational Boolean relation theory on (V_1,K_1) of
type (1,1).
THIN SET THEOREM. Let f be an integral multivariate function. There exists
infinite A containedin Z such that fA not= Z.
THIN SET THEOREM restated. Every integral multivariate function omits a
value over some infinite set.
The thin set theorem can be easily proved from the classical infinite
Ramsey theorem, and can be proved in ACA but not in ACA_0. In fact, it is
provably equivalent over RCA_0 to the classical infinite Ramsey theorem. It
is discussed in a joint paper with Steve Simpson in the Proceedings of the
Boulder Conference (an AMS Summer Research Conference).
4. THE COMPLEMENTATION THEOREM.
For x in Z^k, we write |x| for the sup norm of x, which is the maximum of
the absolute values of the coordinates of x. We say that an integral
multivariate f is strictly dominating if and only if for all x in dom(f),
|f(x)| > |x|.
The complementation theorem is the most basic interesting theorem in
equational Boolean relation theory. It is provable in RCA_0, but is, in a
sense, complete for bounded recursion.
COMPLEMENTATION THEOREM. Let f be a strictly dominating integral
multivariate function. There exists infinite A containedin Z such that fA =
A'. There exists a unique A containedin Z such that fA = A'.
The structure of this unique fixpoint A is rather complex even for strictly
dominating affine transformations from Z into Z (even one-dimensional!).
5. BABY BOOLEAN RELATION THEORY.
By baby BRT I generally mean equational and inequational BRT on (V,K) of
type (1,1) for some basic V,K. We refer to this as unary equational and
inequational BRT on (V,K). In each case, there are only 16 statements
involved.
It is easy to completely classify unary equational and inequational BRT on
the following pairs:
1) V = the set of all integral multivariate multivariate functions, K = the
set of all infinite subsets of Z;
2) V = the set of all integral multivariate multivariate functions, K = the
set of all bi-infinite subsets of Z;
3) V = the set of all strictly dominating integral multivariate functions,
K = the set of all infinite subsets of Z;
4) V = the set of all strictly dominating integral multivariate functions,
K = the set of all bi-infinite subsets of Z.
Here a subset of Z is said to be bi-infinite if and only if it has
infinitely many positive and infinitely many negative elements. We make
this definition also for subsets of R.
The only interesting statements that appear are
a) the thin set theorem together with a straightforward refinement;
b) the complementation theorem.
The refinement is the stronger conclusion that fA union A not= Z.
6. EXTENSIONS OF THE COMPLEMENTATION THEOREM.
We say that A is covered by B,C if and only if A containedin B union C. We
say that A is disjointly covered by B,C if and only if A is covered by B,C,
and B,C are disjoint.
We can restate the complementation theorem as follows.
THEOREM 6.1. Let f be a strictly dominating integral multivariate function.
There exists infinite A containedin Z such that Z is disjointly covered by
A,fA. There is a unique A containedin Z such that Z is disjointly covered
by A,fA.
We now strive for a bi-infinite disjoint cover theorem.
PROPOSITION 6.2. Let f be a strictly dominating integral multivariate
function. There exists bi-infinite A containedin Z such that Z is
disjointly covered by A,fA.
Unfortunately this is false. Here is a fix.
PROPOSITION 6.3. Let f,g be a strictly dominating integral multivariate
function. There exists bi-infinite A containedin Z such that fA is
disjointly covered by A,gA.
Note that here we have replaced f by g and we do not insist that Z be
disjointly covered by A,gA, but only that fA be disjointly covered by A,gA.
Unfortunately this, also, is false.
To fix this, we consider towers A containedin B containedin Z of length 2.
THEOREM 6.4. Let f,g be strictly dominating integral multivariate function.
There exist bi-infinite A containedin B containedin Z such that fA is
disjointly covered by B,gB.
Let f,g be integral multivariate functions. We say that A_1,...,A_r is a
disjoint cover tower for f,g if and only if
i) A_1 containedin ... containedin A_r containedin Z;
ii) for all 1 <= i <= r-1, fA_i is disjointly covered by A_i+1,gA_i+1.
We say that a disjoint cover tower is bi-infinite (infinite, finite) if and
only if the sets are bi-infinite (infinite, finite).
THEOREM 6.4 restated. Every pair of strictly dominating integral
multivariate functions has a bi-infinite disjoint cover tower of length 2.
There is an obvious extension to towers A containedin B containedin C of
length 3:
PROPOSITION 6.5. Every pair of strictly dominating integral multivariate
functions has a bi-infinite disjoint cover tower of length 3.
Unfortunately this is false. But this can be fixed by changing the class of
functions. Let f be an integral multivariate function. We say that f is of
expansive linear growth if and only if there exist constants p,q > 1 such
that p|x| < f(x) < q|x| holds for all sufficiently large |x|.
PROPOSITION 6.6. Every pair of integral multivariate function of expansive
linear growth has a bi-infinite disjoint cover tower of length 3.
Here is an obvious generalization.
PROPOSITION 6.7. Every pair of integral multivariate functions of expansive
linear growth has bi-infinite disjoint cover towers of every finite length.
The status of Propositions 6.6 and 6.7 is discussed in section 7.
7. EQUATIONAL BOOLEAN RELATION THEORY OF TYPE (2,3).
Let ELG(Z) be the set of all integral multivariate functions of expansive
linear growth. Let BINF(Z) be the set of all bi-infinite subsets of Z. Let
INF(Z) be the set of all infinite subsets of Z.
Note that Proposition 6.6 is a statement in equational BRT on
(ELG(Z),BINF(Z)) of type (2,3). For each r >= 1, Proposition 6.7 is a
statement in equational BRT on (ELG(Z),BINF(Z)) of type (2,r).
Let MAH = ZFC + {there exists an n-Mahlo cardinal}_n. Let MAH+ = ZFC + "for
all n >= 1 there exists an n-Mahlo cardinal."
THEOREM 7.1. Propositions 6.6 and 6.7 are provable in MAH+. If MAH is
consistent then neither are provable in MAH.
THEOREM 7.2. The following are provably equivalent in ACA.
i) Proposition 6.6;
ii) Proposition 6.7;
iii) MAH is 1-consistent.
We conjecture that we can "classify" equational BRT on (ELG(Z),BINF(Z)) of
type (2,3). I.e.,
CONJECTURE 7.3. Every instance of equational BRT on (ELG(Z),BINF(Z)) of
type (2,3) is provable or refutable in MAH+.
By the above we see that this conjecture is false with MAH+ replaced by
MAH, assuming MAH is consistent. We encapsulate this conjecture by saying
that it is necessary and sufficient to use Mahlo cardinals of finite order
in order to classify equational BRT on (ELG(Z),BINF(Z)) of type (2,3).
We now consider INF(Z). It is easy to see that Proposition 6.7 is provable
in RCA_0 with BINF(Z) replaced by INF(Z).
PROPOSITION 7.4. Every pair of integral multivariate functions of expansive
linear growth has infinite disjoint cover towers of every finite length
whose first component is disjoint from the image of the last component
under the first function.
THEOREM 7.5. Proposition 7.4, even for length 3, is provably equivalent to
1-Con(MAH) over ACA.
CONJECTURE 7.6. Every instance of equational BRT on (ELG(Z),INF(Z)) of type
(2,3) is provable or refutable in MAH+.
By the above we see that this conjecture is false with MAH+ replaced by
MAH, assuming MAH is consistent. We encapsulate this conjecture by saying
that it is necessary and sufficient to use Mahlo cardinals of finite order
in order to classify equational BRT on (ELG(Z),BINF(Z)) of type (2,3).
We also make a conjecture about type (2,2).
CONJECTURE 7.7. Every statement of equational BRT on (ELG(Z),BINF(Z)) of
type (2,2) is provable or refutable in RCA_0. Same for (ELG(Z),INF(Z)).
8. DISJOINT COVER THEORY.
Boolean relation theory is very difficult (for us) to handle, even of type
(2,2), and even more so of type (2,3).
Note that Proposition 6.6 involves a tower of sets obeying two disjoint
cover conditions. Thus we define disjoint cover theory, a simplification of
Boolean relation theory, as follows.
Disjoint cover theory (DCT) on (V,K) of type (n,m) is the study of all
statements of the form
for all f_1,Š,f_n in V there exists A_1 containedin ... containedin A_m in
K such that a given
set of disjoint cover conditions holds among the m(n+1) sets
A_1,Š,A_m
f_1A_1,Š,f_1A_m
Š
f_nA_1,Š,f_nA_m.
Here a disjoint cover condition among sets B_1,...,B_r is an assertion of
the form
B_i is disjointly covered by B_j,B_p
where 1 <= i,j,p <= r.
Note that we build the tower condition A_1 containedin ... containedin A_m
into disjoint cover theory. Towers are not built into the more general
Boolean relation theory.
We have been able to classify DCT on (ELG(Z),BINF(Z)) of type (2,2).
THEOREM 8.1. Every statement of DCT on (ELG(Z),BINF(Z)) of type (2,2) is
either provable or refutable in RCA_0.
We have not been able to classify DCT on (ELG(Z),BINF(Z)) of type (2,3). We
do have the following partial result.
THEOREM 8.2. Every statement of DCT on (ELG(Z),BINF(Z)) of type (2,3) with
at most two disjoint cover conditions is either provable or refutable in
RCA_0 or provably equivalent, over ACA, to the 1-consistency of MAH.
9. FINITENESS.
There is a striking fact that we have observed in all of our
classifications to date. Recall that these are
a. Equational and inequational BRT on (V,K) of type (1,1), where V is
either the set of all integral multivariate functions, or the set of all
strictly dominating integral multivariate functions, and K is either the
set of all infinite subsets of Z, or the set of all bi-infinite subsets of
Z.
b. Disjoint cover theory on (ELG(Z),BINF(Z)) of type (2,2).
c. Disjoint cover theory on (ELG(Z),BINF(Z)) of type (2,3) with at most two
disjoint cover conditions.
Let NFIN(Z) be the set of all nonempty finite subsets of Z.
THEOREM 9.1. Let V,K be as in a. Every true statement of equational
(inequational) BRT on (V,NFIN(Z)) of type (1,1) is true on (V,K).
THEOREM 9.2. Every true statement of DCT on (ELG(Z),NFIN(Z)) of type (2,2)
is true on (ELG(Z),BINF(Z)).
THEOREM 9.3. Every true statement of DCT on (ELG(Z),NFIN(Z)) of type (2,3)
with at most two disjoint cover conditions is true on (ELG(Z),INF(Z)).
PROPOSITION 9.4. Every true statement of DCT on (ELG(Z),NFIN(Z)) of type
(2,3) with at most two disjoint cover conditions is true on
(ELG(Z),BINF(Z)).
THEOREM 9.5. Proposition 9.4 is provable in MAH+ but not in MAH, assuming
MAH is consistent. Proposition 9.4 is provably equivalent to 1-Con(MAH)
over ACA.
CONJECTURE 9.6 (finiteness). Every true statement of equational BRT on
(ELG(Z),NFIN(Z)) of type (2,2) is true on (ELG(Z),BINF(Z)).
CONJECTURE 9.7 (finiteness). Every true statement of DCT on
(ELG(Z),NFIN(Z)) of type (2,3) is true on (ELG(Z),BINF(Z)). Every true
statement of equational BRT on (ELG(Z),NFIN(Z)) of type (2,3) is true on
(ELG(Z),BINF(Z)).
MAH is insufficient to prove Conjecture 9.7, assuming MAH is consistent.
10. INTEGRAL PIECEWISE POLYNOMIALS.
An integral polynomial is a multivariate polynomial from Z into Z.
An integral piecewise polynomial is an integral multivariate function which
is defined by possibly different integral polynomials in each of finitely
many cases, where each case is given by a finite set of integral polynomial
inequalities.
An integral multivariate function f is expansive if and only if for some
constant p > 1, |f(x)| > p|x| holds for all sufficiently large |x|.
We write EPP(Z) for the set of all expansive integral piecewise polynomials.
THEOREM 10.1. The status of Propositions 6.6 and 6.7 remains the same when
stated for EPP(Z). The same holds if we also require that the functions in
EPP(Z) are of expansive linear growth.
In fact, when Propositions 6.6 and 6.7 are stated for EPP(Z), we can
require that the components A,B,C are of the following form. The image of
an integral piecewise polynomial on the set of double factorials. This will
not affect the status. Note that this results in an explicitly arithmetical
sentence.
11. FINITE FORMS.
Note that at the end of section 10, we have already presented arithmetical
forms. Here we wish to be more finitary. This results in naturally Pi-0-3
statements.
We say that A containedin Z is exponentially sparse if and only if for all
|n| < |m| from A, 2^|n| <= |m|.
PROPOSITION 11.1. Every pair from EPP(Z) has finite disjoint cover towers
of every finite length whose first component is any given exponentially
sparse finite set of integers that are sufficiently large relative to the
pair and length.
THEOREM 11.2. Proposition 11.1, even for length 3, is provably equivalent
to 1-Con(MAH) over ACA.
Proposition 11.1 is in Pi-0-3 form (Pi-0-4 if you are careless).
We can also be more explicit about the sets. An exponential progression is
a sequence where each term is the base 2 exponential of the preceding term.
The first term is arbitrary.
PROPOSITION 11.3. Every pair from EPP(Z) has finite disjoint cover towers
of of every finite length whose first component is any given finite
exponential progression starting with an integer that is sufficient large
relative to the pair and length.
THEOREM 11.4. Proposition 11.3, even for length 3, is provably equivalent
to 1-Con(MAH) over ACA.
THEOREM 11.5. Let f,g in EPP(Z) and n,r,t be a sufficiently large integers.
Then f,g have a finite disjoint cover tower of length r whose first
component is an n element set containing t.
THEOREM 11.6. Theorem 11.5, even for r = 3, is provably equivalent to
1-Con(type theory) over ACA.
12. REAL PIECEWISE POLYNOMIALS.
A real polynomial is a multivariate polynomial from R into R.
A real piecewise polynomial is a real multivariate function which is
defined by possibly different real polynomials in each of finitely many
cases, where each case is given by a finite set of real polynomial
inequalities.
We write EPP(R) for the set of all expansive real piecewise polynomials. We
write EPP(R,Z) for the set of all expansive real piecewise polynomials with
integer coefficients, where the polynomial inequalities also involve only
integer coefficients.
In the case of multivariate functions from R into R, we define a disjoint
cover tower to be as before, except that the sets are subsets of R (not
necessarily subsets of Z). A discrete disjoint cover tower is a disjoint
cover tower where the distance between any two elements of the last
component is at least 1.
PROPOSITION 12.1. Every pair of functions from EPP(R,Z) has bi-infinite
discrete disjoint cover towers of every finite length.
THEOREM 12.2. Proposition 12.1 follows from 1-Con(MAH) and implies Con(MAH)
over ACA, even for length 3.
NOTE: I may not need the "discrete" condition here. I won't be able to tell
for sure until I do some more writing.
13. FINITE FORMS AGAIN.
Recall that in section 11 we obtained naturally Pi-0-3 statements
corresponding to large cardinals. Here we obtain naturally Pi-0-1
statements corresponding to large cardinals, using section 12, by using the
real numbers. The proofs involve use of the technology from Tarski's work
on real algebra.
PROPOSITION 13.1 Every pair from EPP(R,Z) has finite discrete disjoint
cover towers of arbitrary finite length whose first component is any given
exponentially sparse finite set of sufficiently large integers
(sufficiently large relative to the pair and the desired length).
Furthermore, sufficiently large can be replaced by a triple exponential in
the data.
THEOREM 13.2. Proposition 13.1, even for length 3, is provably equivalent
to Con(MAH) over ACA.
PROPOSITION 13.3. Every pair from EPP(R,Z) has finite discrete disjoint
cover towers of of every finite length whose first component is any given
finite exponential progression starting with a sufficiently large integer
(sufficiently large relative to the pair and the length). Furthermore,
sufficiently large can be replaced by a triple exponential in the data.
THEOREM 13.4. Propositions 13.4, even for length 3, is provably equivalent
to Con(MAH) over ACA.
NOTE: The difference between these Propositions and those in section 11 is
that real numbers are allowed in the towers. The theory of the real field
kicks in, and one obtains the triple exponential bound because of
definability in the real field.
Several modifications can be made to these Propositions with the same
results. For instance, we can replace "sufficiently large integer" by
"sufficiently large real." Also, exponentially sparse/progressions can be
replaced by power sparse/progressions, where the power (constant exponent)
is given by a polynomial in the data. When this is done, one can also use
sufficiently large integers or sufficiently large reals. With extra care,
one can gain considerable control over the bounds.
Note that Propositions 13.1 and 13.2 would be easily in immediate Pi-0-1
form if real numbers were not allowed in the tower. However, all of the
integer data can be universally quantified out, resulting in a matrix which
is a statement in real closed fields. This results in a Pi-0-1 sentence. In
order to be more explicit, we can instead ask that the tower be made up of
real algebraic numbers, with a bound placed on their "complexity" or "real
algebraic names." Then one has an explicitly Pi-0-1 statement.
It seems reasonable that one can consider approximate discrete disjoint
covers, and then approximate everything by rationals. This would yield an
explicitly Pi-0-1 statement that avoids the use of names for real algebraic
numbers, in favor of bounds on the numerator/denominator of rationals. Of
course, one has to replace discrete disjoint covers by approximate discrete
disjoint covers.
This whole development depends on the obvious bounds on the number of
elements in the components of a (discrete) disjoint cover tower in terms of
the number of elements in the first component and the arity of the pair of
functions. This is obvious.
14. INTEGRAL POLYNOMIALS FROM N INTO Z.
For elegant concreteness, one may wish to replace piecewise polynomials
with actual polynomials. This is quite tricky to do. It appears that we can
do this, although the details are particularly complicated.
We need to use strongly bi-infinite subsets of Z. These are the subsets of
Z which contain an infinite subset which is symmetric about 0.
PROPOSITION 14.1 Any pair of expansive integral polynomials from N into Z
has strongly bi-infinite disjoint cover towers of every finite length.
THEOREM 14.2. Proposition 14.1, even for length 3, is provably equivalent
to 1-Con(MAH) over ACA.
We can also obtain finite forms analogous to those in section 11, which are
equivalent to 1-Con(MAH), and also analogous to those in section 13, which
are equivalent to Con(MAH). For these finite forms, strong bi-infinite sets
do not appear. We can still rely on exponential sparsity and exponential
progressions. To be safe, we can also require that the first components be
symmetric about 0.
15. BOUNDED ARITY.
All statements thus far considered use multivariate functions without
bounding the arity.
It now appears that in the case of Theorem 6.7, we can restrict attention
to functions of small arity, and get the same results for arbitrarily
length towers. If we not only fix the arity, but also the length of the
tower, then we stay within MAH, but grow indefinitely within MAH as the
length of the tower increases. In particular, there is a small arity and a
short length so that 6.7 is independent of ZFC. If the length is 3 and the
arity is quite small then 6.7 is independent of ZFC. The exact size of
these two parameters that is enough to get independence from ZFC is yet to
be determined, and could be quite tricky. We are confident that, say, arity
4 and length 4 should be enough. Arity 2 and length 3 is the obvious final
target.
Other Propositions should be subject to such analysis.
16. LINEARITY.
We conjecture that piecewise polynomials can be everywhere replaced by
piecewise linear functions. If so, then the finite forms analogous to
section 11 would already be in Pi-0-1 form using machinery related to
Presburger arithmetic instead of real algebra.
What would the analogous linear form of Proposition 14..1 look like?
Expansive integral affine functions from N into Z would be ideal, but may
be too much to ask for. Expansive restrictions of integral affine functions
to finite intersections of integral halfplanes is a good bet. Better would
be expansive restrictions of integral affine functions to integral
halfplanes.
17. FORMAL PARITION THEORY.
We say that A is partitioned by B,C if and only if A is covered by B,C and
A intersect B intersect C = emptyset. This is weaker than A is disjointly
covered by B,C. Nevertheless, we can replace "disjointly covered" by
"partitioned" everywhere and get the same results - except that we have not
redone the classification results. We expect that they will go through and
have the same properties.
If we use "partitioned" instead of "disjoint covered" then the general
theory is called "formal partition theory" instead of "disjoint cover
theory".
****************************
This is the 95th 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
84:BRT/First Major Classification 3/27/00 4:04AM
85:General Framework/BRT 3/29/00 12:58AM
86:Invariant Subspace Problem/fA not= U 3/29/00 9:37AM
87:Programs in Naturalism 5/15/00 2:57AM
88:Boolean Relation Theory 6/8/00 10:40AM
89:Model Theoretic Interpretations of Set Theory 6/14/00 10:28AM
90:Two Universes 6/23/00 1:34PM
91:Counting Theorems 6/24/00 8:22PM
92:Thin Set Theorem 6/25/00 5:42AM
93:Orderings on Formulas 9/18/00 3:46AM
94:Relative Completeness 9/19/00 4:20AM
More information about the FOM
mailing list