FOM: 72:New finite forms/large cardinals
Harvey Friedman
friedman at math.ohio-state.edu
Sun Dec 12 06:11:04 EST 1999
We present a uniform way of giving finite forms of certain infinite
discrete statements. This is in the context of independence results from
ZFC.
The idea is based on the following strengthened notion of inclusion among
subsets of N = the set of all nonnegative integers. Let k >= 0 and A,B
containedin N. We say that
A containedin_k B
if and only if for all x in A,
|B intersect [0,x]| <= |A intersect [0,x]|^k.
Here | | denotes cardinality.
The point is that if we take a statement that asserts the existence of a
finite length tower of infinite subsets of N under inclusion, then we can
consider the same statement with arbitrarily large finite subsets of N
under inclusion_q, where q is properly chosen. Under the right
circumstances, this statement will also be true, and will in fact imply
that the original statement holds in certain crucial situations.
Unfortunately, this method does not quite work (nicely) for the statements
in posting #63. However, it does work for some closely related new infinite
discrete independent statements which we present here.
1. GENERAL METHOD.
We start with a sentence of the following form:
(forall k,r >= 1)(forall R containedin N^k)(there exist infinite A_1
containedin ... containedin A_r containedin N)(phi(k,r,R,A_1,...,A_r)),
where phi is a universal formula in the language of arithmetic with
primitive recursive function symbols, and in the matrix bounded quantifiers
are allowed, connectives, and membership of (tuples of) terms in
R,A_1,...,A_r.
The prospective finite form is:
(forall k,r,p >= 1)(therexists t)(for all finite R containedin N^k)(there
exist finite A_1 containedin_f(k,r) ... containedin_f(k,r) A_n containedin
[0,t] with at least p elements)(phi(k,r,p,R,A_1,...,A_r)),
where f(k,r) is a judiciously chosen function of k,r.
This finite form follows by compactness from the strengthened infinite
statement
(forall k,r >= 1)(forall R containedin N^k)(there exist infinite A_1
containedin_f(k,r) ... containedin_f(k,r) A_r containedin
N)(phi(k,r,R,A_1,...,A_r)),
which hopefully can be proved by the same methods that proved the original
infinite statement. The function f(k,r) is chosen for that purpose.
It will generally not be true that this finite form implies the infinite
statement. However, using compactness, one can get some sort of weakening
of the original infinite statement from this finite form. This can be
enough to prove the independence of the finite form.
2. INFINITE DISCRETE INDEPENDENCE RESULTS.
We now present some infinite statements to which we apply the method. For
motivation and background, see posting #63.
We use N for the set of all nonnegative integers.
Let A,B,C containedin N. We say that A,B is a disjoint cover of C if and
only if
i) A,B are disjoint;
ii) C containedin A union B.
For x in N^k, we write max(x) for the maximum of the coordinates of x.
Let F:N^k into N. We say that F is strictly dominating if and only if for
all x in N^k, F(x) > max(x).
For A containedin N, we write F[A] for the forward image of A^k under F.
We start with the following infinite disjoint cover theorem.
THEOREM 2.1. Let F:N^k into N be strictly dominating. There exists A
containedin N such that A,F[A] is a disjoint cover of N. A is unique and
infinite.
We now move directly to an independent statement.
PROPOSITION 2.2. Let k,r >= 1, F:N^k into N be strictly dominating. There
exist infinite A_1 containedin
... containedin A_r containedin N such that for all 1 <= i <= r-1,
A_i+1\A_1,F[A_i+1]\A_1 is a disjoint cover of A_i + A_i.
Note that if we drop both of the \A_1 then this trivially follows from
Theorem 2.1. It can also be seen that if we drop either one of the \A_1
then in one case this trivially follows from Theorem 2.1 and in the other
case it is simply trivial.
We now apply the method. The proof of Proposition 2.2 from large cardinals
also proves the following.
PROPOSITION 2.3. Let k,r >= 1, F:N^k into N be strictly dominating. There
exist infinite A_1 containedin_8(kr)^2
... containedin_8(kr)^2 A_r containedin N including 1 such that for all 1
<= i <= r-1, A_i+1\A_1,F[A_i+1]\A_1 is a disjoint cover of A_i + A_i.
We use 8(kr)^2 just to be on the safe side. When we go into complete
detail, we will almost certainly find a simple expression in k, not
involving r, that will work.
We then give the finite form.
PROPOSITION 2.4. Let t >> k,r,p >= 1 and F be a strictly dominating
function from a finite subset of N^k into N. There exist finite A_1
containedin_8(kr)^2
... containedin_8(kr)^2 A_r containedin [0,t] with at least p elements
including 1 such that for all 1 <= i <= r-1, A_i+1\A_1,F[A_i+1]\A_1 is a
disjoint cover of A_i + A_i.
Actually this follows from Proposition 2.3 stated for strictly dominating
partial functions F:N^k into N, which also is proved by the same large
cardinal argument. Incidentally, Proposition 2.4 is a trivial consequence
of Theorem 2.1 without the "including 1."
We now get more concrete and avoid the use of >> by using integral
semilinear functions. These are the functions whose graph is a Boolean
combination of halfplanes with integral coefficients.
PROPOSITION 2.5. Let k,r >= 1, F:N^k into N be a strictly dominating
integral semilinear function. There exist infinite A_1 containedin
... containedin A_r containedin N such that for all 1 <= i <= r-1,
A_i+1\A_1,F[A_i+1]\A_1 is a disjoint cover of A_i + A_i.
PROPOSITION 2.6. Let k,r,p >= 1 and F:N^k into N be a strictly dominating
integral semilinear function. There exist finite A_1 containedin_8(kr)^2
... containedin_8(kr)^2 A_r containedin N with at least p elements
including 1 such that for all 1 <= i <= r-1, A_i+1\A_1,F[A_i+1]\A_1 is a
disjoint cover of A_i + A_i.
Furthermore, a bound in k,r,p (roughly double exponential) can be placed on
the elements of A_r in this statement, thereby making it an explicitly
pi-0-1 sentence.
Let MAH = ZFC + {there exists an n-Mahlo cardinal}_n.
THEOREM 2.7. Propositions 2.2, 2.3, 2.4 are provably equivalent to the
1-consistency of MAH over RCA_0. For Proposition 2.4, PRA suffices.
Propositions 2.5, 2.6 are provably equivalent to the consistency of MAH
over RCA_0. For Proposition 2.6, EFA (exponential function arithmetic)
suffices. The growth rate associated with Proposition 2.4 is greater than
that of all provably recursive functions of MAH, but is a provably
recursive function of MAH+.
**********
This is the 72nd 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
More information about the FOM
mailing list