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

*To*: fom@math.psu.edu*Subject*: FOM: Interpretability in Q*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Thu, 23 Dec 1999 08:24:32 -0500*In-Reply-To*: <v04210107b485702b6861@[194.117.5.135]>*Sender*: owner-fom@math.psu.edu

This is a reply to Ferreira 12:21PM 12/22/99. >Five years ago (JSL vol. 59), I introduced a Base Theory for Feasible >Analysis (BTFA) in which some basic analysis can be stated and proved >(this latter part is stated but not worked in the paper; at the time >there was evidence for this, since I had studied some analysis over >the Cantor space in my Penn State'88 dissertation). In a >working-in-progress paper of mine and my student Marques Fernandes, >we retake this line of work and, among other things, prove the >intermediate value theorem in BTFA (Yamazaki has also work in this >direction). From this it follows that the theory of real closed >fields (RCF) is interpretable in BTFA. Now, BTFA is interpretable in >Q. Thus, RCA is interpretable in Q, as Friedman points. In the last line you wrote RCA instead of RCF (real closed fields), which you obviously meant. I was under the impression that certain approaches like what you describe have problems with closure under the field operations - because of reciprocal, one seems to have to start asking whether certain algorithmically defined real numbers are zero or not, which introduces a disastrous quantifier. But I guess that you are proving me wrong about this. When I first read this, I was very surprised because I get an interpretation of RCF in Q as a byproduct of other results which use a lot of detailed algebra, and it looks as though you avoid detailed algebra in favor of analysis. See my posting #56. I now realize that just from the interpretability of RCF in Q, one cannot derive the main results of posting #56 which say, in effect, that the entire theory of real closed fields can be developed in EFA = ISigma_0(exp). E.g., that RCF is provably consistent and complete in EFA, that various axiomatizations of RCF are provably equivalent in EFA, that RCF is conservative over ordered fields for quantifier free formulas provably in EFA, applications to Hilbert's 17th problem, etcetera. At least I don't see how to derive these results from the interpretability result. The interpretability of a theory in Q does establish the consistency of that theory within the stronger system ISigma_0(superexp), where the theory is given a recursively enumerable presentation as is RCF. Nevertheless, I am quite interested in your "working-in-progress paper" and look forward to hearing more about it privately or publicly. It sounds rather intriguing. I get this interpretability as a byproduct of the consistency proof in EFA of RCF together with a general result about interpretability which I discuss below. The interpretability of RCF in Q gives another following weaker result: that EFA proves the cut free consistency of RCF. Here the cut free consistency of a theory asserts that there is no cut free inconsistency from the (universal closures of the) axioms of the theory. This is weaker than proving the consistency. I use much more detailed algebra to prove the consistency of RCF in EFA than to prove the cut free consistency of RCF. My intuition was that even the weaker result needs detailed algebra. >Wilkie's 86 result on the non-interpretability of ISigma0(exp) in Q >is the fundamental result on non-interpretability in Q. It surely >draws a line, and surely there is the question on whether this line >is optimal. However, I believe that *reasonable* bounded theories >which do not prove the totality of exponentiation are interpretable >in Q. For instance, theories whose provably total functions are the >PSPACE computable functions. In such theories more analysis can be >done (Riemman integration, for a start). Thus, more analysis can be >interpreted in Q. I was going to write a systematic posting covering various issues on interpretability, going back to my equivalence of interpretability and relative consistency from the early 80's, and with new results - but your interesting posting got me going. THEOREM 1. A finitely axiomatized theory is interpretable in Q if and only if there is a proof in ISigma_0(exp) = EFA that it is cut free consistent. We say that a finitely axiomatized theory is n-interpretable in Q if and only if there is an interpretation given by formulas in the language of Q each of which has at most n quantifiers. THEOREM 2. Let T be a recursively enumerable theory. T is interpretable in Q if and only if there exists n such that every finite subset of T is n-interpretable in Q. THEOREM 3. Let T be presented as a recursively enumerable theory. Suppose ISigma_0(exp) = EFA proves that T is cut free consistent. Then T is interpretable in Q. In posting #56, I prove the consistency of RCF in EFA, and so by Theorem 3, RCF is interpretable in Q. >I do not know if theories with WKL are still interpretable in Q. But >I see no reason why not. Again, with WKL more analysis can be done. >Hence (hopefully) more analysis can be interpreted in Q. Is WKL_0 interpretable in RCA_0? Yes, because of the earlier results of mine about relative consistency = interpretability from at least the early 80's, and the forcing work. Is VB + AxC + not CH interpretable into VB (von Neumann Bernays class theory)? Yes, for the same reasons. One should be able to use the above criteria together with, perhaps, nonstandards methods from my posting #61, to handle much weaker systems. I think that many people on the FOM (and elsewhere) would like to hear about just where analysis can and can't be done in a way that is interpretable in Q.

**References**:**Fernando Ferreira**- FOM: Some remarks on Friedman's 73 posting

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

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