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

*To*: fom@math.psu.edu*Subject*: FOM: 61:Finitist proofs of conservation*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Wed, 29 Sep 1999 11:52:47 -0400*Sender*: owner-fom@math.psu.edu

This is the 61st 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/18/99 1:32PM John Burgess has specifically asked about whether one give a finitistic model theoretic proof of certain conservative extension results discussed in [Si99]. Burgess asks this in connection with Hilbert's program. Specifically, I. WKL_0 is a conservative extension of PRA for Pi-0-2 sentences. II. ACA_0 is a conservative extension of PA for arithmetic sentences. III. ATR_0 is a conservative extension of IR for arithmetic sentences. IV. Pi-1-1-CA_0 is a conservative extension of ID(<omega) for arithmetic sentences. Here IR is Feferman's IR, which can be taken to be the theory extending PA with new function symbols encoding the Kleene H-sets on each specific initial segment of the ordinal notation system Gamma_0. All of these conservative extension results are given model theoretic proofs in [Si99] except for III. The reader is referred to the exposition of my proof in Friedman, MacAloon, Simpson, "A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis", 1982, 197-230 in: G. Metakides (ed.), Patras Logic Symposion, Studies in Logic and the Foundations of mathematics, North-Holland, 1982. These model theoretic proofs are naturally and straightforwardly directly formalized in ACA and in fact, in a little weaker system lying properly between ACA_0 and ACA called ACA0+ in [Si99]. In particular, they are not obviously formalized in ACA_0. So some work is needed to prove them in a weak arithmetic system. Here we prove them in the weak system of arithmetic called EFA* (see below), and show that EFA* is best possible. More specifically, we write PFA (polynomial function arithmetic) for the system in the language of 0,1,+,x,<, with the usual successor axioms and defining equations, together with induction for all bounded formulas. This is the same as what is called ISigma_0 in the book {HP93] and elsewhere. In [HP93], it is proved that PFA is fully capable of developing finite sequence coding and formalizing syntax. In fact, they devote all of Chapter V, section 3, to this topic, which is entitled "Exponentiation, Coding Sequences and Formalization of Syntax in ISigma_0." In the Bibliographic Notes on page 406, they write "A formalization of syntax in ISigma_0 is considered here for the first time, though the ideas on which it is based have been around for some time." This makes PFA a good vehicle for taking a reverse mathematics point of view towards weak fragments of arithmetic. >From this point of view, it is natural to take EFA = exponential function arithmetic to be in the language of PFA, whose axioms are PFA plus the single axiom (forall n)(2^n exists). (From some points of view it is more natural to take exponentiation as primitive). And we take EFA* to be PFA plus the axiom that asserts that for all n, there is a sequence of integers of length n, starting with 0, where each term is the base 2 exponentiation of the preceding term. Here is what we will do in this note. 1. We isolate a crucial general fact about theories, which we call the Key Lemma. The Key Lemma has an easy model theoretic proof. But the Key Lemma also has a proof using the Criag interpolation theorem for predicate calculus with equality. The interpolation theorem has model theoretic proofs, but it also has a proof theoretic proof using Gentzen's cut elimination theorem for predicate calculus with equality. The usual proof of the cut elimination theorem with iterated exponential estimates (given by Gentzen) is readily formalized in EFA*. This yields a proof of the interpolation theorem and of the Key Lemma that is readily formalized in EFA*. 2. Using the Key Lemma, we give a purely model theoretic proof the conservation results in question. In fact, we adapt the usual model theoretic proofs of these conservation results to provide formal interpretations of the appropriate kind which establish the conservation results. The Key Lemma is crucial. 3. We round out the situation by claiming that EFA* is best possible in the following sense. That each of the conservation results are provably equivalent to EFA* over PFA. By the way, the cut elimination theorem for predicate calculus is also equivalent to EFA* over PFA. ********** 1. THE KEY LEMMA THEOREM 1.1. Let T be a theory in predicate calculus whose language includes <,=,c, and which contains the axioms of linear order. Suppose that for each n >= 0, T is consistent with "there are at least n elements << c." Let I be a new monadic predicate symbol. Then T + "I is a cut below c" is consistent. Proof: The model theoretic proof is straightforward. Consider T' = T together with the axioms c > c_1 > c_2 > ..., where the c_i are new constant symbols. Then T' is consistent. Let M be a model of T'. There is obviously a cut below c in M. Set I to be a cut below c in M. Then (M,I) satisfies T + "I is a cut below c." QED Let W be the following theory in the language {<,=,0,S}: a) axioms of linear order; b) 0 is the least element; c) Sx is the successor of x; d) every nonzero element is the successor of some element. There is a well known elimination of quantifiers for W. From this elimination of quantifiers, one can also show that every formula phi(x) in one free variable is provably equivalent over W to a Boolean combination of inequalities of the form x < S...S0. KEY LEMMA. Let T be a finitely axiomatized theory in predicate calculus whose language includes <,=,0,c, and which contains the axioms of W. Suppose that for each n >= 0, T is consistent with "there are at least n elements < c." Let I be a new monadic predicate symbol. Then T + "I is a cut below c" is consistent. Proof: This is an immediate consequence of Theorem 1.1. But now we wish to give an alternative proof using the Craig interpolation theorem for predicate calculus with equality, and quantifier elimination for W. Fix T,I to be as in the hypothesis of the Key Lemma, and assume that T proves "I is not a cut below c." By the Craig interpolation theorem, let phi be a sentence in the common language of T and "I is not a cut below c" such that T proves phi and phi proves "I is not a cut below c." Hence phi is in the language {<,=,c} and has the following properties: i) for all n >= 0, phi is consistent with W + "there are at least n elements < c." ii) phi proves "I is not a cut below c." By cut elimination for W, there exists n >= 0 such that phi if and only if c >= S^n(0) is provable in W. Let (K,<) be the linear ordering omega + Z, I = omega, and c lies in Z. Then (K,<,I,c) satisfies W and therefore satisfies phi. But (K,<,I,c) also satisfies "I is a cut below c." This contradicts that phi implies "I is not a cut below c." QED THEOREM 1.2. The Key Lemma is provable in EFA*. Proof: We indicate the essential points. First of all, we have used the interpolation theorem. One of the well known proofs goes as follows. Let phi arrows psi be provable. Then phi arrows psi has a cut free proof. And then an interpolant is constructed by recursion on the cut free proof. There are no blowups in size after one obtains the cut free proof. The original proof by Gentzen of his cut elimination theorem coontained iterated exponential estimates, and so is readily formalized in EFA*. The cut elimination theorem for W is readily formalizable in EFA, which is better than we need. In the final steps, we considered the structure (K,<,I,c), where c lies in Z. We used that satisfaction implies consistency, which in general requires induction with respect to a truth predicate, and so could be a problem in a system like EFA* with its limited induction. However, because of the simplicity of the cut elimination procedure, the truth predicate for this structure can be built up by simple recursions. In fact, this can be carried out in EFA. Then the induction needed for the final step is easily available in EFA. QED More delicate arguments will also establish more general versions of the Key Lemma in EFA*. In particular, with considerable effort, it can be proved in EFA* with W replaced by the axioms for linear ordering (and with 0 removed), as in Theroem 1.1. But the Key Lemma is precisely what we need here. 2. WKL_0 OVER PRA We use the following version of the usual Ackerman hierarchy of functions from Z+ into Z+. A_1(n) = 2n. A_i+1 is the indefinite iteration of A_i. I.e., A_i+1(n) is the result of applying A_i n times starting at 1. We need to consider a formalization of this hierarchy within PRA, or even within EFA. We have to take into account the limited language of PRA, and that no matter how this is formalized in PRA, we cannot prove that the A's are total. Let f(n) be the obvious algorithm for computing the n-th function in the usual Ackerman hierarchy of functions using stacks. Specifically, suppose the algorithm f(n) has been defined. The algorithm f(n+1) computes at m by starting with 1, and applying the algorithm f(n) m times. Clearly f is a low level computable function. In PRA we cannot prove that every f(n) is total; i.e., halts at all arguments. However, we can obviously prove in PRA that i) if f(n+1) is total and m < n then f(n) is total; ii) if f(n+1) is total then f(n+1) is the indefinite iteration of f(n) as in the usual Ackerman hierarchy of functions. Here we have identified f(n) with the partial function that it computes, which is a harmless abuse of terminology. Thus we will write f(n)(m) for the output of the algorithm f(n) at the input m, which may not be defined. We now let phi be a Sigma-0-2 sentence that is consistent with PRA. We want to show that phi is consistent with WKL0. Let phi = (therexists p)(forall q)(R(p,q)). Fix p such that (forall q)(R(p,q)). We let PRA' be PRA + phi + "f(c) is total." Since PRA proves f(n) is total for each particular n, we see that the Key Lemma applies to PRA'. Hence the system PRA'' = PRA + phi + "f(c) is total" + "I is a cut below c" is consistent. We now build a sequence of closed intervals [xi,yi], 0 <= i <= c/4. For each such i, yi = f_c-2i(xi). We start with [x_0,y_0] = [p,f_c(p)]. Suppose [x_i,y_i] has been defined, yi = f_c-4i(x_i). Look at all Turing machines with index <= fc-4i-2(x_i) which produce an output at 0 that lies in [x_i,y_i]. Let E be the set of these at most f_c-4i-2(x_i) values. By elementary combinatorial considerations, E must be disjoint from some subinterval [x_i+1,y_i+1], where y_i+1 = f_c-2i-4(x_i+1), and x_i+1 > 2^(x_i). Take this to be [x_i+1,y_i+1]. The idea is that this choice of the next interval is to handle all appropriate instances of Sigma-0-1 bounding whose front universal quantifier ranges over [0,x_i], and whose parameters are subsets of [0,y_i+1]. Note that the left endpoints are strictly increasing and lie at or above p. We now let J be the cut determined by looking at the left endpoints whose index i lies in the cut I. We now define an interpretation of WKL0 in PRA''. The integers are taken to be the elements of J. And 0,<,+,x are are usual. From the perspective of PRA'', take the sets to be the intersections of finite sets with the cut J. Since J cannot be a finite set, we have the usual overspill situation which allows us to prove the interpretation of weak Konig's lemma and Delta-0-1 comprehension in PRA''. Also, the interpretation of phi is obviously provable in PRA''. Every instance of Sigma-0-1 induction becomes provable in PRA'' under this interpretation; this has to be checked with set parameters. Hence WKL_0 + phi is consistent since PRA'' is consistent. THEROEM 2.1. EFA* proves that WKL_0 is conservative over PRA for Pi-0-2 sentences. 3. ACA_0 OVER PA Let phi be an arithmetic sentence that is consistent with PA. Let R be a binary relation symbol. Let T' be the following theory in the language of PA together with c,R: 1) PA + phi; 2) for all i <= c, R(i,n) codes the i-th Turing jump. 3) induction for all formulas in the language. Obviously, for all n, T' + c > n is consistent. We can therefore apply the Key Lemma. Let T'' = T' + "I is a cut below c." Then T'' is consistent. We now define a translation of ACA_0 into T''. We take the arithmetic part to be standard from the perspective of T''. We take the sets of integers to be the sets of integers coded by the unary predicates R(i,n) for i lying in I. We use 3) to verify that the interpretation of the induction axiom of ACA_0 is provable in T''. And since T'' proves that I is a cut below c, we see that the interpretation of each instance of arithmetic comprehension is provable in T''. THEOREM 3.1. EFA* proves that ACA_0 is conservative over PA for arithmetic sentences. 4. ATR_0 OVER IR IR amounts to the system ACA_0 + "for all x, the H-set starting with x on each ordinal notation < Gamma_0 exists", where the statement in quotes is taken as a scheme. We prove conservativity of ATR_0 over IR with respect to Pi-1-1 sentences within EFA* as follows. Let alpha_0 < alpha_1 < ... be the usual fundamental sequence approaching Gamma_0. Let phi = (therexists x containedin omega)(psi(x)) be a Sigma-1-1 sentence consistent with IR, where psi is arithmetical. Let P be a predicate symbol. Let T be the following first order system (no set variables): i) Peano arithmetic; ii) for each i, we introduce a predicate symbol Q_i together with the axioms asserting that Q_i is an H-set starting with P on alpha_i; iii) transfinite induction on each alpha_i with respect to all formulas in the language; iv) psi(P). Then T is consistent. Now let T' be in the language of arithmetic plus P plus a new monadic predicate symbols Q,I plus the constant c. The axioms of T' are T + "I is a cut below c" + "Q is an H-set starting with P on alpha_c." By the Key Lemma, T' is consistent. Then follow my model theoretic proof to get the consistency of ATR_0 + psi(P), and hence of IR + phi. 5. Pi-1-1-CA_0 OVER ID(<omega) We actually show in EFA* that every sentence of the form "p in O" that is provable in Pi-1-1-CA_0 is provable in ID(<omega). Let "p not in O" be consistent with ID(<omega). We can transfer over to subsystems of second order arithmetic. Thus let T = ACA_0 + "the n-th hyperjump exists" + "p not in O". Here the second axiom is a scheme over n, and the third axiom is a specific sentence using a specific p. Then T is consistent. Let T' = ACA_0 + "the c-th hyperjump exists" + "p not in O." By the Key Lemma, T'' = ACA_0 + "the c-th hyperjump exists" + "p not in O" + "I is a cut below c" is consistent. Then define the obvious structure using the sets coded up in the hyperjump hierarchies on the integers lying in the cut I. 6. LENGTHS OF PROOFS In each case we get a proof of the conservation result within EFA* that is of normal length for a mathematical proof. This is because there is no metamthametical argument used to prove the existence of a proof in EFA*. Rather the proofs in EFA* are given explicitly. One does have to consider relatizations of the four bigger theories (WKL_0, ACA_0, ATR_0, Pi-1-1-CA_0) that come out of the translations that are defined in each case. However, these theories are finitely axiomatized by formulas of reasonable size. One can consider lengths of proofs inherent in the conservation statements themselves. The only nonlinear blowups involved occur in the conversion of proofs with cut to proofs without cut in the predicate calculus. This is well known to be a linear stack of 2's. It is also well known that there is a linear stack of 2's blowup in this cut elimination procedure. One of the proofs of this blowup can be converted into a proof that this same blowup occurs in each of these four conservation results. These observations can also be converted to a proof within PFA that each of these four conservation results are provably equivalent to EFA*. REFERENCES [Si99] Steve Simpson, Subsystems of Second Order Arithmetic, Persepctives in Mathematical Logic, Springer, 1999. [HP93] Petr Hajek and Pavel Pudlak, Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic, Springer, 1993.

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

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