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.

shouldgo through in $EFA$ (based on $EFA$'s track record in handling "elementary" number theory); my question is whether anyone has actually shown - in a publishd source - that this is indeed the case. – Ali Enayat May 22 '11 at 16:37