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

-
The coefficients of the polynomials in $S$ need to have some cannonical, finitary presentation in order for the question to be well-posed. Perhaps you would be content with coefficients in the prime subring? – SJR May 6 '13 at 10:27
The subring of coefficients is fixed in advance? – Mark Sapir May 6 '13 at 10:28
As SJR notes, I guess equations should have coefficients in some fixed (recursive) subring of $R$ in order for decidability to make sense. Likewise, first order formulas are in the language of rings augmented with constants from such a subring. – Laurent Moret-Bailly May 6 '13 at 10:42
We don't know yet whether the Diophantine theory of $\mathbb{Q}$ is decidable, but if it is that would definitely be a concrete example. – François G. Dorais May 6 '13 at 15:06
Does anybody think that the diophantine theory of the rationals is decidable? – Felipe Voloch May 8 '13 at 19:07

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. Especially, look at Section 3, "The Method of Julia Robinson." The argument shows (amazingly) that the natural numbers can be defined in $F$.

-
+1. Very nice! I guess you intend that the subring here is $\mathbb{Q}$, so that your polynomial equations have all rational coefficients? – Joel David Hamkins May 8 '13 at 16:13
Are you sure about replacing $\mathbb{R}$ by any formally real field, not just Arhimedean ones? – François G. Dorais May 8 '13 at 16:43
Whoops! Archimedian is necessary. I've edited. And hello Joel! Greetings from Thailand. Yes, the subring here can be the rationals, or the integers. – SJR May 8 '13 at 16:59
At least "archimedian" is necessary for Robinson's argument. Whether it is actually required I don't know – SJR May 8 '13 at 17:03
I always knew that was you, by your posts (and your initials). – Joel David Hamkins May 8 '13 at 17:04