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.