Real Closed Fields with Predicate for a Dense Subfield

Question

Consider $M = (\mathbb{R};+,<, \times, 0, 1, K)$ where $K$ is a unary predicate which holds on $\mathbb{Q}$ (or any dense subfield of $\mathbb{R}$).

Question: Is it true that the parametrically definable sets in 1-free variable is the finite union of points and 'locally dense' sets?

(I'm not sure if locally dense is a real term, so I will definite it as such: $U$ is locally dense if there exists some interval $I \subset M \cup \{\pm \infty\}$ such that for every $a,b \in I$ there exists a $q \in U$ such that $a<q<b$).

Motivation: It is a corollary of the Tarski–Seidenberg theorem that $(\mathbb{R};<, +, \times, 0, 1)$ is O-minimal (i.e. every parametrically definable subset is the finite union of points and intervals).

If $\varphi(x)$ is a quantifier free formula in the language (with parameters), then $\varphi(x)$ is equivalent to a boolean combination of $p(x) = 0$, $q(x) >0$, $K(x)$ and $\neg K(x)$. This case is clear. When we begin to add quantifiers, things become much more tricky to pin down. For instance, $(\exists y)(K(y) \wedge y^2 = x)$ - there does not seem to be a way to eliminate quantifiers.

Answer 1

In Definability and decision problems in arithmetic Julia Robinson has proven (among other interesting things) that $\mathbb{Z}$ was definable in $(\mathbb{Q},+,.,0,1)$.

So if $K$ is interpreted as $\mathbb{Q}$, definable sets in $\mathcal{M}$ can be more complicated than that, and there is no quantifier elimination in $\left\langle +,.,0,1,<,K \right\rangle$.

Now, if $K$ is interpreted as another dense subset of $\mathbb{R}$, then it probably depends on the subset. I guess the result holds for some real closed subfields of $\mathbb{R}$ and fails for some other subsets, among which there is $\mathbb{Q}$.

edit: I thought Definability and decision problems in arithmetic was free in JSTOR but it seems to have changed. The collected works of Julia Robinon can still be found in librairies.