The proof that all formulas of second-order arithmetic are $\Pi^1_n$ for some $n$ (i.e. can be written with a bloc of second-order quantifiers followed by an arithmetical formula) uses the axiom of countable choice, which is independent of $Z_2$. Does comprehension for formulas with all the second-order quantifiers in front imply comprehension for all formulas anyway?
More generally, does this hold level-by-level of the analytical hierarchy? More precisely, say that a formula is weakly $\Pi^1_n$ if it can be written with $n-1$ second-order quantifier alternations starting with $\forall$, but also allowing arithmetical quantifiers interspersed between the second-order quantifiers (i.e. the formulas that countable choice implies are $\Pi^1_n$). Does $\Pi^1_n-CA_0$ imply comprehension for weakly $\Pi^1_n$ formulas?
