FOM: Do We Need New Axioms? Results/Conjectures
Harvey Friedman
friedman at math.ohio-state.edu
Fri Feb 11 12:17:39 EST 2000
I am taking the liberty of presenting some results - which have not been
properly checked - together with some conjectures. This premature
announcement is prompted by their apparent relevance to the issue "Do We
Need New Axioms?" which is the topic of an upcoming panel discussion at the
ASL Annaul Meeting, June 3-7, 2000, in Urbana, with panelists Sol Feferman,
Harvey Friedman, Penelope Maddy, and John Steel. See my previous posting
"Do We Need New Axioms? Upcoming Panel Discussion".
**********
Let N be the set of all nonnegative integers. A multivariate function on N
is a function f such that
i) there exists k >= 1 such that the domain of f is N^k;
ii) the range of f is a subset of N.
For A containedin N, we write fA = {f(x): every coordinate of x lies in A}.
We say that f has precisely quadratic growth if and only if there exist
positive rational constants c,d such that the inequality
c|x|^2 <= f(x) <= d|x|^2
holds for all but finitely many x in dom(f).
Here |x| is the sup norm of x. If we use any l_p norm, 0 < p <= infinity,
this definition would remain unchanged.
The main conjectures concern the following family of 2^2^9 statements (up
to formal Boolean equivalence):
*For all multivariate functions f,g on N of precisely quadratic growth,
there exist infinite sets A,B,C containedin N such that a given Boolean
equation in A,B,C,fA,fB,fC,gA,gB,gC holds.*
Here Boolean equations involve union, intersection, and complement
(relative to N). There are 2^2^9 formally inequivalent = semantically
inequivalent Boolean equations, but this number can readily be cut down
somewhat because of relations like A containedin B implies fA containedin
fB.
THEOREM 1 (66%). There is an instance of * that is provably equivalent to
the 1-consistency of Mahlo cardinals of finite order, over ACA.
CONJECTURE 1. Informally speaking, it is necessary and sufficient to use
Mahlo cardinals of all finite orders in order to determine the truth values
of all instances of *. In particular, every instance of * is either
refutable in RCA_0, provable in ACA, or provably equivalent to the
1-consistency of Mahlo cardinals of finite order over ACA, with all three
possibilities present. Furthermore, in the first of the three cases, the
refutation proof can be given with fewer than 100,000 symbols in RCA_0 with
abbreviations.
Consider the following more general family of statements, indexed by n,m >=
1 and Boolean equations in (n+1)m set variables:
**For all multivariate functions f_1,...,f_n on N of precisely quadratic
growth, there exist infinite sets A_1,...,A_m containedin N such that a
given Boolean equation in
A_1,...,A_m,f_1A_1,...,f_nA_m,f_2A_1,...,f_2A_m,...,f_nA_1,...,f_nAm
holds.**
EXTENDED CONJECTURE 2. Same as conjecture 1, but for **.
In addition, we have finite obstruction conjectures.
FINITE OBSTRUCTION CONJECTURE 3. Any particular instance of * that holds
with "infinite" replaced by "arbitrarily large finite" must hold in its
original form.
EXTENDED FINITE OBSTRUCTION CONJECTURE 4. Any particular instance of **
that holds with "infinite" replaced by "arbitrarily large finite" must hold
in its original form.
At this time, even conjectures 1 and 3 are out of reach. In order to begin
to tame these conjectures, we restate them slightly where we insist that
the A's form a tower in general position:
We say that A_1 containedin ... containedin A_m containedin N are in
general position if and only if A_1, A_2\A_1, ..., A_m\A_m-1, N\A_m are
infinite.
And we restate * and ** with general position:
***For all multivariate functions f,g on N of precisely quadratic growth,
there exist infinite sets A containedin B containedin C containedin N in
general position such that a given Boolean equation in
A,B,C,fA,fB,fC,gA,gB,gC holds.*
****For all multivariate functions f_1,...,f_n on N of precisely quadratic
growth, there exist infinite sets A_1 containedin ... containedin A_m in
general position such that a given Boolean equation in
A_1,...,A_m,f_1A_1,...,f_nA_m,f_2A_1,...,f_2A_m,...,f_nA_1,...,f_nA_m
holds.**
And we have
THEOREM 2 (66%). There is an instance of *** that is provably equivalent to
the 1-consistency of Mahlo cardinals of finite order, over ACA.
And we restate the four conjectures using *** and ****.
However, even these restricted conjectures are out of reach. So further
taming is necessary for substantial progress.
Let B_1,...,B_p be subsets of N. A disjointness condition is an equation
B_i intersect B_j = emptyset
where i < j. Note that there are exactly C(p,2) disjointness conditions,
none, some, or all of which may be true.
The particular Boolean equation that is behind Theorems 1 and 2 is quite
powerful in the following sense. It formally implies 12 disjointness
conditions on the 9 sets A,B,C,fA,fB,fC,gA,gB,gC, in the sense of formal
Boolean algebra. Actually, formal implication and semantic implication are
demonstrably equivalent in this context.
Thus we define the $$$disjointness degree$$$ of a Boolean equation as the
number of disjointness conditions that it formally implies.
Thus it is natural to consider the family of statements *** for Boolean
equations of disjointness degree >= 12 only. Of course, Theorem 2 still
holds (66%).
The conjectures are then restated for *** with the restriction to Boolean
equations of disjointness degree >= 12 only. Here the conjectures appear to
be within reach, as I am making serious progress on them, and expect things
to go smoothly.
PLAN: To slowly reduce the number 12 down to 0. WIth 0 of course, we have
the original class ***. If I ever get this far, there is the matter of
relaxing or eliminating the general position requirement, and also, of
course, having more functions and/or more sets, towards **** and even **.
It also appears that if we restrict to Boolean equations of disjointness
degree >= 13 rather than of disjointness degree >= 12 (in ***), then things
get easier, and every statement will be refutable in RCA_0 or provable in
ACA. But this proof has not been completed.
More information about the FOM
mailing list