[FOM] Interpretability in Q

[Robert M. Solovay]

I reconstructed my example. Some details follow.

1) It is well-known that IDelta_0 + Omega_1 is relatively interpretable in
Q. {Here Omega_1 asserts that the function {x -> x^{log x}} is total.}

I use QQ for a "sufficiently large" finite fragment of IDelta_0 + Omega_1.
In particular, QQ proves the usual arithmetic facts about + and *
[commutativity and associativity of + and *, distributivity of * over +,
etc.] and the theorems that say the usual definition [in IDelta_0] of the
relation z = x^ y works and has the usual properties. {A good choice for
QQ is Buss's theory S^1_2, transcribed into the language of arithmetic.}

Our sentences A and B will each include:
     1) QQ;
     2) The statement that the map m -> 2^m is not total.

	To proceed further, I need to work in the theory 1) + 2). Define a
partial function J thus; J(0) = 0; J(n+1) [if defined] is 2^{J(n)}. Since
exp is not total, it is clear that there is a largest m such that J(m) is
defined.

	A will conisist of 1), 2) and:
3a): m is even.

	B will consist of 2), 2) and:
3b): m is odd.

	Of course, A and B cannot both hold. So our only remaining task is
to see that Q[A] and Q[B] are relatively interpretable in Q. It certainly
is sufficient to see that they are relatively interpretable in the more
comfortable theory QQ. I will focus on A; the treatment of B is entirely
similar. My discussion will be quite sketchy in spots.

	Our interpretation will first ask: Does ISigma_3 hold?

	If it does, there is no particulr difficulty in defining an
explicit interpretation of A using the arithmetical completeness theorem.

	Now suppose that ISigma_3 fails. Then we can explicitly define a
proper cut [containing 2, downward closed, and closed under + and *].
Call it J.

	By the method of "shortnening of cuts" we can define a subset J_1
of J which is a cut [containing 2, downward closed, closed under +, * and
the map {x -> x^ {log x} } ] such that if x is in J_1, then Beth_{10}(x)
is in J. {Here Beth_0(x) = x and Beth_{n+1}(x) = 2^{Beth_n(x)}.} I do not
claim that J_1 is a proper subset of J.

	It is now easy to use the methods of my "letter to Hajek" to get
an interpretation of QQ[A]. Roughly speaking the terms one will use for
the model we are creating will come from J_1; the integer x such that 2^x
does not exist [needed to prove the appropriate Herbrand consistency
statements] will be available since for y in J_1, Beth_10(y) lies in J.

	I am keenly aware that in the immediately proceeding paragraph the
handwaving is proceeding at a furious pace. But I lack the time at the
moment to review the techniques in question in intelligible detail. I am
hoping that this outline will be intelligible to the cognoscenti.

	--Bob Solovay



On Tue, 21 Dec 2004, Robert M. Solovay wrote:

> As I recall, I had an example where A and B were sentences
> such that Q[A} and Q[B] are interpretable
> in Q but Q[A & B]  is not. Unpublished and I certainly don't recall the
> details now. My memory was that the example wasn't terribly difficult.
>
> 	--Bob Solovay
>
>
> On Mon, 20 Dec 2004, Edward T. Dean wrote:
>
> >
> > I have been skimming through Edward Nelson's _Predicative Arithmetic_
> > recently, and he writes (at the tail end of Ch. 15) that he does not
> > know the answer to a certain compatibility problem regarding
> > interpretability in Robinson arithmetic: for formulas A and B, if both
> > Q[A] and Q[B] are interpretable in Q, then is Q[A,B] interpretable in Q?
> > I'm just wondering if anyone on FOM does know the answer, as the book is
> > decently aged.
> >
> > ~~~~~
> > Edward T. Dean
> > edean at post.harvard.edu
> > ~~~~~
> >
> > _______________________________________________
> > No banners. No pop-ups. No kidding.
> > Make My Way your home on the Web - http://www.myway.com
> > _______________________________________________
> > FOM mailing list
> > FOM at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/fom
> >
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>