I say this is impossible: any expansion of the theory of reals by anything vaguely resembling sets is doomed to undecidability.

**Theorem:** Let $T$ be a two-sorted theory with one sort for reals, and the second sort for sets of reals, which includes the theory of ordered rings (on the first sort). Assume that for each standard $n\in\mathbb N$, it is consistent with $T$ that the set $\{0,1,\dots,n\}$ exists.

Then it is undecidable if $T$ proves a given formula $\phi(X)$, where $X$ is a set variable, but $\phi$ contains no set quantifiers.

(The assumptions could still be weakened. For example, it would be enough if $T$ does not disprove the existence of a set whose intersection with the interval $[0,n]$ is $\{0,1,\dots,n\}$.)

This can be shown by mimicking the usual proof that consistency of $\Sigma_1$ sentences with theories containing Robinson’s $R$ (not to be confused with Robinson’s arithmetic $Q$) is undecidable, using a definition of $\mathbb N$ in $\mathbb R$ by a formula with an existential set quantifier.

Specifically, let us fix a recursively inseparable pair of disjoint r.e. sets $A_0,A_1\subseteq\mathbb N$. By the MRDP theorem, we can write
$$x\in A_i\iff\mathbb N\models\exists\vec y\,p_i(x,\vec y)=0$$
for some integer polynomials $p_0,p_1$. Define
$$\begin{align}
N(X)&\iff\begin{aligned}[t]&0\in X\land1\in X\land\forall x\in X\,(x=0\lor1\le x)\\
&\land\forall x,y\in X\,\bigl(y\le x\to x-y\in X\bigr),\end{aligned}\\
W_i(X,x,w)&\iff\exists\vec y\in X\,\bigl(x\le w\land\vec y\le w\land p_i(x,\vec y)=0\bigr),\\
\phi(X,x)&\iff N(X)\land\exists w\in X\,\bigl(W_0(X,x,w)\land\neg W_1(X,x,w)\bigr).
\end{align}$$
(The intention is that $N(X)$ means “$X$ is an initial segment of $\mathbb N$”, $W_i(X,x,w)$ means “in $X$, there are witnesses for $x\in A_i$ below $w$”, and $\phi(X,x)$ means “in the initial segment $X$, there are witnesses for $x\in A_0$ smaller than any witnesses for $x\in A_1$”.)

The result now follows from the next two claims, which imply that
$$\{n\in\mathbb N:T\vdash\neg\phi(X,n)\}$$
is undecidable.

**Claim 0:** If $n\in A_0$, then $T+\exists X\,\phi(X,n)$ is consistent.

**Proof:** Fix $\vec a\in\mathbb N$ such that $p_0(n,\vec a)=0$, and let $m=\max\{n,\vec a,1\}$. By assumption, it is consistent with $T$ that
$$X=\{0,1,\dots,m\}$$
is a set. Then we verify in $T$ easily that $N(X)$, $W_0(X,n,m)$, and $\neg W_1(X,n,m)$: in particular, there are no witnesses for “$n\in A_1$” in $\{0,\dots,m\}$, as there are in fact no witnesses in $\mathbb N$ by disjointness of $A_0$ and $A_1$.

**Claim 1:** If $n\in A_1$, then $T+\exists X\,\phi(X,n)$ is inconsistent.

**Proof:** As above, fix $\vec a\in\mathbb N$ such that $p_1(n,\vec a)=0$, and let $m=\max\{n,\vec a\}$. Work in $T$, and assume for contradiction that $X$ and $w\in X$ satisfy $N(X)$, $W_0(X,n,w)$, and $\neg W_1(X,n,w)$.

First, assume $w\ge m$. The definition of $N(X)$ easily implies $0,1,\dots,m\in X$. But then in particular, $\vec a\in X$, hence $W_1(X,n,w)$, a contradiction.

On the other hand, assume $w\le m$. The definition of $N(X)$ implies that the only elements of $X$ below $m$ are $0,1,\dots,m$. However, “$n\in A_0$” has no witnesses among $\{0,\dots,m\}$, as it has no witnesses in $\mathbb N$. Thus, we obtain a contradiction with $W_0(X,n,w)$.

nonemptyset.) So, clearly you need more than that. $\endgroup$ – Emil Jeřábek 3.0 Jun 5 '18 at 8:20