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$.



First order decidability of rings vs Diophantine decidability
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


1. The (positive) existential theory of $F$ is effectively computable (e.c.)
2. 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.](http://booksc.org/dl/1744752/01a731) Especially, look at Section 3, "The Method of Julia Robinson." The argument shows (amazingly) that the natural numbers can be defined in $F$. 


