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

*To*: fom@math.psu.edu*Subject*: Re: FOM: Hilbert's program and RCF*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Wed, 22 Dec 1999 12:04:58 -0500*In-Reply-To*: <14431.60147.519320.277887@rayleigh.math.psu.edu>*References*: <v04003a2cb4839152d1de@[24.31.183.29]><v04003a2cb4839152d1de@[24.31.183.29]>*Sender*: owner-fom@math.psu.edu

This is a response to Simpson 4:02PM 12/21/99. The response is in several parts. 1. What does Simpson think Hilbert's program is (was)? 2. Main points of my posting #73 not addressed in Simpson's response. 3. RCF versus WKL_0. Extending and combining. 1. WHAT DOES SIMPSON THINK HILBERT'S PROGRAM IS (WAS)? I am not an historian and like to rethink f.o.m. issues from scratch. Nevertheless, I do acknowledge that sometimes looking at the past helps in dealing with the present and future. Simpson wrote >However, Hilbert's program has another aspect: consistency and >conservative extension results *relative to* PRA. There is reason to >believe that the real intention of Hilbert's program was to show that >**every mathematically provable Pi^0_1 sentence is provable in PRA. ** In >other words, to show that our formal system S for mathematics as a >whole is *conservative* over PRA for Pi^0_1 sentences, and provably >consistent *relative to* PRA. This is not the same as the consistency >of S being provable *within* PRA. The **'s are mine. Under this interpretation of Hilbert's program for Pi-0-2 sentences - not Pi-0-1 sentences - we already know many striking counterexamples which simply cannot be eliminated or analyzed away. E.g., see posting #19 and another dozen or so. You can also go back to Paris/Harrington. As for Pi-0-1 sentences of a mathematical character (not consistency statements), the only examples are the ones that have come up in my posting #72 and related earlier postings. One thing I mean to do is to give hopefully simpler versions of these Pi-0-1 independence results that are at least independent of weaker systems than ZFC + large cardinals - i.e., take advantage of the fact that I could make them independent of much weaker systems in order to make them even simpler. This should work and be perhaps rather elegant. The emphasis you place on the distinction between PRA proving the consistency of S and S being a conservative extension of PRA for Pi-0-1 sentences seems to be to be very misleading. First of all, in every case that has naturally come up, if PRA proves the consistency of S then every Pi-0-1 sentence provable in S is provable in PRA. And also if every Pi-0-1 sentence provable in S is provable in PRA then the consistency of S can be proved in rather trivial extensions of PRA such as PRA + Con(PRA). I don't know exactly what you are driving at, partly because the point you are making has nothing to do with the main thrust of my posting #73. Now let us take this conception of Hilbert's program literally. **every mathematically provable Pi^0_1 sentence is provable in PRA. ** Does this mean ***every mathematically proved Pi-0-1 sentence is provable in PRA***? Let's say we are referring to the actual published literature, rather than "provable" or my latest incursions. Then under this interpretation, Hilbert's program is wide open, and very exciting to investigate. In particular, we need to answer *Is FLT provable in PRA?* I actually care about the distinction between EFA and PRA. Perhaps historians will argue whether or not and to what extent or in what sense Hilbert cared about the distinction between EFA and PRA. So I will ask *Is FLT provable in EFA?* I conjecture that both are true, and the latter is considerably harder to prove than the former. And of course FLT is no isolated case. There are more things that need to be investigated along these lines. Now suppose that Simpson does not mean *** but rather something more strictly looking like **. Then I would take the program to, in an operational sense, mean #construct more and more comprehensive models of mathematical practice which can be shown to be conservative extensions of PRA for Pi-0-1 sentences. Furthermore, strive for the proof of such conservativity to be actually given in PRA, in the sense that it is not merely a proof somewhere that in fact such a proof exists.# There is a reason for the second sentence above. See posting #61 and the posting of Avigad Tue Nov 02 12:29:51 1999 as well as the review of Simpson's book by Burgess which can be found at http://www.math.psu.edu/simpson/sosoa/burgess/ I can inject here once again the spirit of my posting #73. Perhaps we can even find a formal system, which supports mathematical reasoning of enormous scope in an unfettered natural way, including proofs of theorems that are known to have great logical strength in the presence of the usual base theories we use, such as RCA_0, but where we have a demonstrable conservative extension of PRA for Pi-0-1 sentences? Somehow we manage to avoid incorporating the standard base theories such as RCA_0 by a more subtle analysis of mathematical practice. I am now actively trying to refute this possibility. Perhaps it can be refuted to a large extent, but still carried out to a surprisingly large extent? I just don't know how this will come out. There could be very clever surprises on both sides of this fence. 2. MAIN POINTS OF MY POSTING #73 NOT REFLECTED IN SIMPSON'S RESPONSE. I wrote: > > there is a system PRA (primitive recursive arithmetic) that some > > authors like to identify with Hilbertian finitism. In all of the > > proposed formalizations of extensive mathematics - including, say, > > what goes on in such things as FLT - there is more than enough to > > easily interpret PRA. So by Godel, Hilbert's program cannot be > > carried out in such a setup. Simpson wrote: > >However, Hilbert's program has another aspect: consistency and >conservative extension results *relative to* PRA. There is reason to >believe that the real intention of Hilbert's program was to show that >every mathematically provable Pi^0_1 sentence is provable in PRA. In >other words, to show that our formal system S for mathematics as a >whole is *conservative* over PRA for Pi^0_1 sentences, and provably >consistent *relative to* PRA. This is not the same as the consistency >of S being provable *within* PRA. By a proposed formalization of *extensive* mathematics, in the context of my posting #73, I meant really extensive mathematics including the entire graduate curriculum as normally presented. So this would include such things as Cantor Bendixson, perfect subsets of Borel sets, various forms of abstract measure theory, least upper bound principles, noneseparable Banach spaces and duals, etcetera. There are no proposed formalizations that go that far that are not essentially set theory with many iterations of the power set operation. In any case, no formalization of things like Cantor Bendixson or a variety of things that in the usual setup of reverse mathematics, are at least ACA_0 and beyond, and so well beyond being conservative extensions of PRA, or provably consistent relative to PRA. In fact, it is common wisdom that you cannot include such kinds of abstract mathematics in a conservative extension of PRA, and the partial evidence normally given is that such abstract mathematics reverses to systems that in fact prove the consistency of PRA, such as ACA_0 and higher. The point of my posting is to question that line of reasoning since it relies on a base theory that is subject to various kinds of attack. Simpson wrote >Of course G"odel's second incompleteness theorem shows that this more >restricted version of Hilbert's program also cannot be carried out >wholesale, e.g., for S = ZFC or, for that matter, S = PA. The point is that I am criticizing this kind of citing of Godel's theorem. E.g., there could be a very powerful practical set theory that covers a vast amount of abstract mathematics in an unfettered way, and yet is provably consistent within, say PRA! Or maybe at least provably consistent within something unexpectedly weak. E.g., you don't actually use full comprehension in actual abstract unfettered mathematics, but rather only blue comprehension, and that makes it metamathematically much much weaker, while preserving all of the theorems in an unfettered, natural, direct way. I want to see how far one can go in either direction with this. I.e., refute that this can be done. And also maybe actually do something like this. Simpson wrote >However, it >*can* be carried out for, e.g., S = WKL_0, and WKL_0 suffices for a >remarkably large portion of mathematics, including many of the >best-known non-constructive theorems in analysis, algebra, and other >parts of core mathematics. Of course, reverse mathematics is filled with all kinds of examples where this fails, because over the base theory RCA_0, things reverse into ACA_0 and higher - see Simpson's book. I'm not going to criticize this business of WKL_0 being conservative over PRA for Pi-0-1 and Pi-0-2. After all, the result is credited to me. But it has nothing to do with the main points of my posting #73. >To me this looks like the most significant >progress to date in the direction of realizing Hilbert's program. >This is the point of my paper ``Partial Realizations of Hilbert's >Program'', JSL, 53, 1988, pp. 349-363, on-line at ><http://www.math.psu.edu/simpson/papers/hilbert/>. I was making the point that it is still possible to realize Hilbert's program in a way that is approximately 10^100 times as powerful. Only I suspect that it can't be done and I am trying to refute that. By the way, you seem to take PRA as something special for Hilbert's program. See the discussion of this in the paragraph below marked ##. 3. RCF VERSUS WKL_0. EXTENDING AND COMBINING. >Friedman continues: > > > There has been considerable progress on one front. Namely, to show > > that a lot of interesting mathematics can be proved consistent > > within PRA. Perhaps most notably, the consistency of Elementary > > Algebra and Geometry - formalized by, say, real closed fields - is > > proved consistent in PRA, and even in the much much weaker system > > EFA (exponential function arithmetic, or ISigma(exp) discussed in, > > say, Hajek/Pudlak). See posting #56. In fact, RCF (real closed > > fields) is interpretable in Robinson's Q (interpretable in the > > sense of Tarski). Hence RCF is consistent relative to Q in an > > appropriate sense. Simpson wrote > >But, how much interesting mathematics is formalizable in RCF? Much >less than in WKL_0, for sure. So it is not clear to me how much these >results concerning RCF contribute to Hilbert's program. I think that the point you are making is that WKL_0, or even RCA_0, proves the intermediate value theorem for continuous functions, and hence for polynomials. Hence every theorem of RCF translates into a theorem in RCA_0 via the coding of real algebra in RCA_0. Incidentally, this argument can be used to prove the consistency of RCF relative to the consistency of RCA_0, and hence PRA. And I think it can be nudged a bit to show the consistency of RCF within PRA. This would be much easier than previous arguments that I know of. Of course, the result in posting #56 that RCF can be proved consistent within EFA is much more complicated. ##However, what you are saying here doesn't make sense unless you have decided that Hilbert's program is absolutely tied to PRA. If you interpret Hilbert's program to mean that one wants to prove consistency or conservation extension results using methods that are somehow "unimpeachable," then why take PRA as a dividing line? It makes more sense to recognize that there are gradations, and that the weaker the theory that is doing the proving, the more "unimpeachable" it is, and hence the stronger the result for Hilbert's - or somebody's - program. ## And if Hilbert can be seen to clearly take PRA as the dividing line, then perhaps people just concentrate on this dividing simply because of its historical connection with David Hilbert. In the long run, this is not an appropriate reason to take PRA as a dividing line, whereby weaker systems don't "contribute to Hilbert's program." In other words, PRA is not the dividing line between relevance and non relevance just because of what Hilbert may or may not have said. As far as what mathematics RCF proves, take RCF as formalized by the least upper bound axioms. All sorts of deep mathematical facts can be formalized in RCF. E.g., 1. The fundamental theorem of algebra, that a complex polynomial of degree >= 1 has a root. 2. The whole of Euclidean geometry as developed formally by Hilbert. 3. If a multivariate complex polynomial is one-one from some C^n into C^n then it is onto. 4. I remember being told about RCF and a famous 1,2,4,8 dimensional theorem about certain types of algebras. Perhaps somebody can refresh my memory of this. Now there is a very interesting objection to what I am saying. Namely, that in each case one can only formulate the theorems in a fixed dimension since the language of RCF does not have variables over natural numbers. So this leads to the project of giving an axiomatization of real algebra that allows one to state and prove facts about, say, all polynomials, and all semi-algebraic sets. One would have an induction principle on the parameters such as the degree and the number of variables, and in the case of a semi-algebra set, on the number of parameters. Perhaps an elegant system like this would formalize the actual reasoning done by semi-algebraic geometers. One would then attempt to prove the consistency of the resulting system within a weak fragment of PRA (and conservativity also over a weak fragment of PRA). Along these lines, it makes sense to go for a combined system with variables over integers and variables over real numbers. The idea here is not to rely on coding of real numbers, but rather take them as primitive. This kind of formalization, with its associated conservative extension results, is precisely the kind of tool that would be useful to have - especially for mathematicians - when analyzing a proof like FLT with an eye towards showing that FLT is provable in PRA or even EFA. There are continuous constructions that come in.

**References**:**Harvey Friedman**- FOM: 73:Hilbert's program wide open?**Stephen G Simpson**- FOM: Hilbert's program and RCF

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

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