FOM: 45:Result #1/Program A
Harvey Friedman
friedman at math.ohio-state.edu
Wed Jul 14 06:07:22 EDT 1999
This is the 45th 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
A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of self contained postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html
This concerns the first substantial result in the program discussed in
posting #39: Large Cardinals/synthesis. Now that I have a good clean
initial result, this program - which I henceforth call Program A - is off
to a real start.
This posting is entirely self contained, and will not require familiarity
with #39. I believe that this real launching of Program A is in and of
itself enough to sustain the wider program of establishing new and
interesting areas of discrete mathematics that can only be developed using
large cardinals for the forseeable future. There are additional related
programs that I don't have good initial results about yet which I expect to
add to the mix.
In a nutshell, Program A begins with one of my discrete independence
statements that asserts the existence of arbitrarily long finite towers of
infinite sets of integers satisfying some specific elementary conditions
relative to a function. Program A is to look at all such elementary
conditions and determine when the corresponding statement holds. The
desired results say that one can make this determination, but only with the
use of large cardinals. Also, that there is a finiteness theorem: that
there are infinite sets satisfying the conditions if and only if there are
arbitrarily large finite sets satisfying the conditions - but this fact is
itself provable only with the use of large cardinals. More detailed
information also arises: that every instance is either decidable in RCA_0
or equivalent to the 1-consistency of Mahlo cardinals of finite order. As
Program A develops, there may be a modification in the nature of these
results - e.g., other large cardinals, smaller and or larger, may enter the
picture. Now for the details.
**************************
Let N be the set of all nonnegative integers. Let F:N^k into N and A
containedin N. We write F[A] for {F(x): x in A^k}. We write A delta B for
the symmetric difference of A and B. We say that F is strictly dominating
if and only if for all x_1,...,x_k, F(x_1,...,x_k) > x_1,...,x_k.
We begin with the following (easy) fundamental result, which encapsulates
recursion.
THEOREM 1. Let k >= 1 and F:N^k into N be strictly dominating. There exists
A containedin N such that A delta F[A] = N. Furthermore, A is unique and
infinite.
Note that we can write A delta F[A] = N as A = N\F[A].
We continue with several versions of a discrete independence result. We had
to look at several formulations in order to obtain our first substantial
result in Program A. The first formulation is my favorite among the "tower"
independence results:
PROPOSITION 2. Let k,r >= 1 and F:N^k into N be strictly dominating. There
exists r infinite sets A_1 containedin A_2 containedin ... containedin A_r
containedin N such that for all 1 <= i <= r-1, A_i + A_i containedin (A_i+1
delta F[A_i+1])\A_1.
Proposition 3 still needs to be massaged.
We say that A is F-free if and only if for all x_1,...,x_k in A, if
F(x_1,...,x_k) in A then F(x_1,...,x_k) is among x_1,...,x_k. By way of
background, we have the following classical theorem:
THEOREM 3. Let k >= 1 and F:N^k into N. There exists an infinite F-free
subset of N.
With the help of F-free sets, we can reformulate the above as follows:
THEOREM 4. Let k >= 1 and F:N^k into N be strictly dominating. There exists
an F-free A containedin N such that A union F[A] = N. Furthermore, A is
unique and infinite.
PROPOSITION 5. Let k,r >= 1 and F:N^k into N be strictly dominating. There
exists r infinite F-free sets A_1 containedin A_2 containedin ...
containedin A_r containedin N such that for all 1 <= i <= r-1, A_i + A_i
containedin (A_i+1 union F[A_i+1])\A_1.
We're almost there. We need to massage Proposition 5 just a little bit more:
PROPOSITION 6. Let k,r >= 1 and F:N^k into N be strictly dominating. There
exists r infinite F-free sets A_1 properlycontainedin A_2
properlycontainedin ... properlycontainedin A_r containedin N such that for
all 1 <= i <= r-1, A_i + A_i containedin (A_i+1 union F[A_i+1])\A_1.
We write MAH for ZFC + {there exists an n-Mahlo cardinal}_n. We write MAH+
for ZFC + "for all n, there exists an n-Mahlo cardinal."
THEOREM 7. Propositions 2,5,6 are all provably equivalent to the
1-consistency of MAH over ACA_0.
We now initiate Program A.
We begin with the observation that Propsoition 6 is an instance of the
following general form:
FORM 8. Let k,r >= 1 and F:N^k into N be strictly dominating. There exists
r infinite F-free sets A_1 properlycontainedin A_2 properlycontainedin ...
properlycontainedin A_r containedin N such that for all 1 <= i <= r-1, a
certain Boolean relation holds between A_1, A_i + A_i, A_i+1, and F[A_i+1].
What is a Boolean relation between p subsets E_1,...,E_p of N? It is an
assertion that some Boolean combination of E_1,...,E_p is N, where
complementation is taken to be relative to N. Note that there are 2^2^p
such Boolean relations.
Let BR be a 4-ary Boolean relation. This determines the instance X_1(BR):
"Let k,r >= 1 and F:N^k into N be strictly dominating. There exists r
infinite F-free sets A_1 properlycontainedin A_2 properlycontainedin ...
properlycontainedin A_r containedin N such that for all 1 <= i <= r-1,
BR(A_1, A_i + A_i, A_i+1, F[A_i+1])."
THEOREM 9. ZFC does not decide all statements X_1(BR), assuming ZFC is
consistent. MAH+ does decide all elements of X_1(BR). In fact, every such
statement is either decided in RCA_0 or is provably equivalent over ACA_0
to the 1-consistency of MAH.
Every X_1(BR) has a natural weakening to finite sets. Thus we define
X_1'(BR) as:
"Let k,r,p >= 1 and F:N^k into N be strictly dominating. There exists r
finite F-free sets A_1 properlycontainedin A_2 properlycontainedin ...
properlycontainedin A_r containedin N such that for all 1 <= i <= r-1,
BR(A_1, A_i + A_i, A_i+1, F[A_i+1])."
THEOREM 10. MAH+ proves that for all 4-ary BR, X_1'(BR) implies X_1(BR).
This assertion is provably equivalent to the 1-consistency of MAH over
ACA_0.
Note that the assertion in Theorem 10 is a kind of finiteness theorem that
tells us that if we cannot find the required infinite sets, then there must
be a finite obstruction.
Three possible improvements stand out. One is to use the more comprehensive
BR(A_1, A_i, A_i+1, A_1 + A_1, A_i + A_i, A_i+1 + A_i+1, F[A_1], F[A_i],
F[A_i+1]). Another is to drop F-freeness. Still another is to drop
"properlycontainedin." The first will surely turn out to be easier to pull
off than the others.
There are more possible improvements, in various directions. Rather than
give a comprehensive list of possible improvements, let us see what
develops.
***************************
We close with a rather Grand Conjecture along these lines. It's somewhat
different than the above in some respects - since the number of instances
is infinite. We can make even much stronger conjectures, but we will
exercise some restraint at this early stage.
Let BR = BR(A_1,...,A_r, A_1 + A_1,...,A_r + A_r, F[A_1],...,F[A_r]) be a
Boolean relation. Let X(BR) be:
"Let k >= 1 and F:N^k into N be strictly domninating. There exists infinite
sets A_1,...,A_r containedin N such that BR(A_1,...,A_r, A_1 + A_1,...,A_r
+ A_r, F[A_1],...,F[A_r])."
We know that there is no algorithm which, provably in MAH, decides the
truth of each X(BR). We conjecture that there is an algorithm which,
provably in MAH+, decides the truth of each X(BR). Furthermore, we
conjecture that the appropriate finiteness theorem holds, and is provably
equvialent to the 1-consistency of Mahlo cardinals. I.e., that if we can
find arbitrarily large finite A_1,...,A_r, then we can find infinite
A_1,...,A_r. We know that this finiteness statement implies the
1-consistency of MAH over ACA_0.
More information about the FOM
mailing list