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$?
P.S. The following paper provides an excellent expository account of Robinson's theorem (and related results).
D. Flath and S. Wagon, How to Pick Out the Integers in the Rationals: An Application of Logic to Number Theory, American Mathematical Monthly, Nov. 1991.
