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

*To*: fom@math.psu.edu*Subject*: FOM: Hilbert's program and RCF*From*: Stephen G Simpson <simpson@math.psu.edu>*Date*: Tue, 21 Dec 1999 16:02:43 -0500 (EST)*In-Reply-To*: <v04003a2cb4839152d1de@[24.31.183.29]>*Organization*: Department of Mathematics, Pennsylvania State University*References*: <v04003a2cb4839152d1de@[24.31.183.29]>*Reply-To*: simpson@math.psu.edu*Sender*: owner-fom@math.psu.edu

This posting is a followup to Harvey Friedman's discussion of what he calls ``conventional approaches'' to Hilbert's program, in his posting ``FOM: 73:Hilbert's program wide open?'', Tue Dec 21 11:04:48 1999. Friedman focuses on consistency proofs *within* PRA: > 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. 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. See for instance W. W. Tait, Finitism, Journal of Philosophy, 1981, pp. 524-546, and P. Kitcher, Hilbert's Epistemology, Philosophy of Science, 43, 1976, pp. 99-115. 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. 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. 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/>. 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. 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. Nevertheless, I feel that these new results of Friedman on RCF (EFA proves consistency of RCF, and Q interprets RCF) are remarkable and have obvious foundational significance in terms of a possible future base-theory free, coding-free incarnation of reverse mathematics, stated in terms of interpretability. I am looking forward to seeing the proofs of these exciting new results. -- Steve

**Follow-Ups**:**Harvey Friedman**- Re: FOM: Hilbert's program and RCF

**References**:**Harvey Friedman**- FOM: 73:Hilbert's program wide open?

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

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