[FOM] Re: Interpretability in Q (Edward T. Dean)

[Sam Buss]

     This compatibility problem is known to have a negative answer 
(Solovay, unpublished, 1986).   Here is Solovay's construction:

    Define  superexp(k) to be 2^{2^{2^.....2}}, an iterated exponential 
with k  2's.

    Define   log_even(N) to mean that superexp(k) <= N < superexp(k+1) for 
some even value of k.
    Define  eventually_log_even to mean that there is an M s.t. every N>M 
is log_even.
     Define log_odd(N) and eventually_log_odd in the analogous way.

     Define "exp" to mean that exponentiation is total.

     Let A := (exp    or   eventually_log_even)
     Let B := (exp    or   eventually_log_odd)

      Then  Q[A}  and Q[B] are individually interpretable in Q, but Q[A,B] 
is not.

      Note that (A and B) implies exp.

-- Sam Buss




>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
>~~~~~