*Question*: Is there a decidable theory sufficient to formulate and prove (many) theorems of classical analysis?


What I have in mind is a theory with two kinds of objects, reals (which are introduced as a Dedekind complete ordered field) and subsets of ${\mathbb R}^n$.
For each ${\mathbb R}^n$ there are axioms of Extensionality and Specification
but not Adjunction (<https://en.wikipedia.org/wiki/General_set_theory>).


If I am not mistaken, this is not sufficient to introduce arithmetic, neither algebraically (writing down a predicate for $x\in{\mathbb Z}$) nor logically. 
So, the theory must be fairly weak. On the other hand, this must be enough to build up quite a bit of analysis, although I am not sure how much exactly. Chain rule, mean value theorem, intermediate value theorem - no doubt. Taylor's theorem - yes, but for each degree separately (we do not have induction.) Riemann integral - probably, but I am not certain. 


Did I get it right?


[EDIT] To avoid misunderstanding, there are in fact two different questions, is there *any* decidable theory on the basis of which some analysis can be built, and if such a theory can be constructed along the lines suggested above. 


[EDIT] About the second question: no, this approach does not work. (See the answer by Emil Jeřábek.) 



A weak fragment of analysis?
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)$.


