FOM: Interpretability in Q

[Harvey Friedman]

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.