I’m coming round to see things like this. Despite its centrality in the reverse mathematics programme, ACA_{0} 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 ACA_{0} proves ∀x(Fx v ¬Fx). But if, from ACA_{0}‘s viewpoint each number indeed determinately falls under F or doesn’t, then what good reason can someone who accepts ACA_{0} have for not allowing F also to appear in instances of induction? But following that reasoning inflates ACA_{0} to the much stronger full ACA.

So in fact, I want to argue that the usual conceptual grounding for ACA_{0} 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.