Am I counting quantifiers correctly?

Question

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?

Answer 1

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.