In 1949 Julia Robinson showed the undecidability of the first order theory of the field of rationals by demonstrating that the set of natural numbers $\Bbb{N}$ is *first order definable* in $(\Bbb{Q}, +, \cdot$).

It is not hard to see that Robinson's result can be reformulated in the following symmetric form.

**Theorem A.** *The structures* ($\Bbb{N}, +, \cdot$) *and* $(\Bbb{Q}, +, \cdot$) *are bi-interpretable.*


The following generalization of Theorem A is considered folkore (I am not aware of a published reference).

**Theorem B.** *If $(M, +, \cdot)$ is a model of $PA$  (Peano arithmetic), then the field of rationals $\Bbb{Q}^M$ of $(M, +, \cdot)$ is bi-interpretable with $(M, +, \cdot )$.*

Let $EFA$ denote the *exponential function arithmetic* fragment of $PA$, a fragment also known as $I\Delta_{0}+exp$.  

Based on *a posteriori* evidence *classical* theorems of Number Theory do not require the full power of $PA$  since they can be already verified in $EFA$ (indeed Harvey Friedman has conjectured that even FLT can be verified in $EFA$, with a proof that would be very different from Wiles'). 

This suggests that in Theorem B one should be able to weaken $PA$ to $EFA$, hence my question:


**Question**. *Is there a published reference for the strengthening of Theorem B, where $PA$ is weakened to $EFA$?*