First order decidability of rings vs Diophantine decidability Are there known (preferably ``concrete'') examples of a ring $R$ (commutative, with 1) such that:  
$\bullet$ the first order theory of $R$ is undecidable, but
$\bullet$ the positive existential (= Diophantine) theory of $R$ is decidable?
The Diophantine theory consists of formulas of the form $\exists x S(x)$ where $x$ is an $n$-tuple of variables and  $S$ denotes a finite system of polynomial equations, with coefficients in (some subring of) $R$.
 A: Let $F=\mathbb{R}(t)$ be the field of rational functions in the variable $t$ with real coefficients. We regard $F$ as a structure of type $(+ \times -\,\, 0\,\, 1)$. Then


*

*The (positive) existential theory of $F$ is effectively computable (e.c.)

*The full first-order theory of $F$ is not e.c.
Proof of 1: Suppose that a system of polynomial equations has a solution $\bar{r}$ in $F$. Here $\bar{r}$ is a tuple of rational functions. Choose a real number $s$ that  is not a root of any of the denominators of the rational functions $r_i$ and substitute $s$ for $t$ in $\bar{r}$, to obtain a tuple of real numbers that satisfies the same system of equations. Conversely, a tuple of reals that satisfies a given system of equations is already a tuple of rational functions. It follows that the existential theory of $F$ is e.c. if and only if the existential theory of $\mathbb{R}$ is e.c. But the last statement is true, by a well-known theorem of Tarski.
Proof of 2: A proof of the undecidablity of the first-order theory of $F$ (actually $\mathbb{R}$ can be replaced by any archimedian formally real field) is the subject of a 1961 paper by Raphael Robinson here.  Especially, look at Section 3, "The Method of Julia Robinson." The argument shows (amazingly) that the natural numbers can be defined in $F$. 
