Interpretation of one theory in another I'm reading a review of Nelson's book "Predicative Arithmetic". In the review Wilkie writes:

Of course the spirit of the program is that a sentence, $A$, is to be
regarded as predicatively established if $Q \cup \{A\}$ can be (explicitly)
interpreted in the minimal theory $Q$. However, this cannot be taken as
the definition because, by a result of Solovay, there are sentences $A$,
$B$ such that $Q \cup \{A\}$ and $Q \cup \{B\}$ are both interpretable in $Q$ but $Q \cup \{A \land B\}$ is not

Here $Q$ is Robison Arithmetic.
Questions:

*

*What does it mean for one theory to be (explicitly) interpretable in another? And what is the significance of the existence of such an interpretation?

*What is the significance of Solovay's result?

 A: The issue raised by Wilkie is remarked upon by Nelson on p. 63 of Predicative Arithmetic. Given what he says there, I'm pretty sure he has Shoenfield's definition of interpretation in mind (which can be found on p. 61ff of his Mathematical Logic---another, possibly cheaper source for these notions is Tarski, Mostowski & Robinson's Undecidable Theories; also, Nelson himself gives a definition of interpretation on pp. 6ff of his book, though it is very terse and he references Shoenfield). If for some reason you don't have access to the book, here's his definition, almost verbatim. We say that $I$ is an interpretation of $L$ in $L'$, where $L$ and $L'$ are first-order languages, if it specifies:
i) a universe for $I$, represented by a unary predicate symbol $U_I$ of $L'$;
ii) for each $n$-ary function symbol $f$ of $L$, a corresponding symbol $f_I$ of $L'$;
iii) for each $n$-ary predicate symbol $P$ of $L$ (with the exception of $=$, which is generally taken to be a logical symbol), a corresponding symbol $P_I$ of $L'$.
Moreover, we say that $I$ is an interpretation of $L$ in a theory $T'$ if $I$ is an interpretation of $L$ in the language of $T'$ and also:
a) $T' \vdash \exists x U_Ix$ (it proves that the domain is non-empty);
b) for each $f$ in $L$, $T' \vdash (U_Ix_1 \wedge \dots \wedge U_Ix_n) \rightarrow U_If_I(x_1, \dots, x_n)$ (it proves that the domain is closed under functions).
Now, if $\phi$ is a formula of $L$ and $I$ an interpretation of $L$ in $L'$, then we can define for $\phi$ its interpretation in $L'$, $\phi^{(I)}$. We start by defining a formula $\phi_I$ of $L'$ which is obtained by starting with $\phi$ and replacing each symbol of the original language by its interpretation in $L'$ (e.g., if $\phi$ is $f(x)=y$, then we replace $f$ by $f_I$ to obtain $f_I(x)=y$), and then relativizing the existential quantifiers to the domain (i.e. replace every $\exists x \psi$ by $\exists x (U_Ix \wedge \psi)$. As the last step, if $x_1, \dots, x_n$ are the free variables of $\phi$, set $\phi^{(I)}$ to be $(U_Ix_1 \wedge \dots \wedge U_Ix_n) \rightarrow \phi_I$.
Finally, an interpretation of a theory $T$ in a theory $T'$ is an interpretation $I$ of the language of $T$ in $T'$ such that $T' \vdash \phi^{(I)}$ for every nonlogical axiom of $T$.
Anyway, moving on to your second question about Solovay's result. The problem is the following. As Nelson puts it (p. 63), "we would like to have a formula $A$ in the language of $Q$ be a theorem of Predicative Arithmetic if and only if $Q[A]$ is interpretable in $Q$." Suppose this definition is correct. By Solovay's result, we have that there are formulas $A_1, A_2$ such that $Q[A_1], Q[A_2]$ are interpretable in $Q$, and hence, by the definition, theorems of Predicative Arithmetic, but also such that $Q[A_1 \wedge A_2]$ is not interpretable in $Q$. Therefore, again by the definition, $A_1 \wedge A_2$ is not a theorem of Predicative Arithmetic. But this is absurd, since, for any $A_1$ and $A_2$, if they both are theorems of a given theory, by (say) conjunction introduction (or the equivalent of your favorite deduction system) $A_1 \wedge A_2$ is also a theorem of the given theory. Hence, the definition cannot be correct.
Incidentally, Solovay's result is unpublished, but you can find a sketch in this nice article (cf. section 8).
