MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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
up vote 10 down vote accepted

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

share|cite|improve this answer
+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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.