*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] Emil Jeřábek pointed out that there is a  predicate $x\in{\mathbb N}$ in the form 
$$\forall X(0\in X\wedge \forall y(y\in X\to y+1\in X)\to x\in X).$$
Originally, I though about restricting (or forbidding) quantifiers over sets to 
avoid something like this, but now I think it may be unnecessary. This predicate is useless (for its intended purpose) if we cannot prove existence of sufficiently many sets $X$ with this property, and I think it might be the case.

[EDIT] Following Jeřábek, denote the above predicate by $N(x)$. If we have
$$(N(x)\wedge x\neq 0)\to N(x-1),$$ 
then we already have Robinson arithmetic (which is undecidable). The thing is, I do not see how to prove this implication by the means available.