I think this is right but I want to check. The theory $\mathsf{WKL}^\*\_0$ is conservative over EFA for $\Pi^0\_2$ sentences. And the first order part of $\mathsf{WKL}^\*\_0$ is axiomatized by EFA plus the following formula scheme, known as the $\Sigma^0\_1$ bounding principle. 


For every $\Sigma^0\_1$ formula $\varphi(i,j)$ ( with $n$ not free):
$$(\forall i<m)\, \exists j\, \varphi(i,j) \rightarrow \exists n\,(\forall i<m)(\exists j<n)\varphi(i,j).$$


So this formula scheme is not $\Pi^0\_2$ and I want to check that I see this correctly. 


I was puzzled at first because the quantifier on $i$ in the antecedent is bounded, so I ignored it. But I believe the correct point is that this quantifier comes before an unbounded quantifier on $j$, so when you prenex this formula it starts with $\exists i\,\forall j$, placed before a $\Sigma^0\_1$ formula. 


To state the general rule: when counting quantifier changes, you ignore bounded quantifiers that come after all unbounded ones. But even a bounded quantifier, if it comes before an unbounded one, must be counted.


Is that right?



Am I counting quantifiers correctly?

> 
> To state the general rule: when counting quantifier changes, you ignore bounded quantifiers that come after all unbounded ones. But even a bounded quantifier, if it comes before an unbounded one, must be counted.
> 
> 
> 


That's correct, at least when working in weak fragments of PA.


The complication is that when you're working in a theory that includes the bounding axiom, you can use it to move bounded quantifiers inside unbounded ones. Over PA, that formula *is* (equivalent to) a $\Pi^0\_2$ formula. So when people are used to working over stronger theories, they often just skip bounded quantifiers entirely when counting quantifier changes, and that's correct...as long as you stick to theories with a strong enough bounding axiom.


