[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: 72:New finite forms/large cardinals*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Sun, 12 Dec 1999 06:11:04 -0500*Sender*: owner-fom@math.psu.edu

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

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]