I’m coming round to see things like this. Despite its centrality in the reverse mathematics programme, ACA0 is in fact (as it were) conceptually unstable. For take any open sentence F(x) of the language of second-order arithmetic which may embed set-quantifiers. Then ACA0 proves ∀x(Fx v ¬Fx). But if, from ACA0‘s viewpoint each number indeed determinately falls under F or doesn’t, then what good reason can someone who accepts ACA0 have for not allowing F also to appear in instances of induction? But following that reasoning inflates ACA0 to the much stronger full ACA.
So in fact, I want to argue that the usual conceptual grounding for ACA0 in fact shouldn’t take you quite as far as that theory: roughly, it takes you to a more restricted theory with parametric (rather than quantified) versions of induction and comprehension and lacking formulae with embedded set quantifiers, though you can allow prenex existentials. That still — or so it seems to me at the moment — gives you all the usual constructions for proving proxies of theorems of analysis: it’s just we can lose the unwanted stuff like ∀x(Fx v ¬Fx) when F embeds set-quantifiers.
I’m going to talk about this and related matters in Oxford in about a week’s time. If the suggestion survives its outing, I’ll put a souped-up version of this stuff on my webpage. Fingers crossed.