Bounded quantifiers don't count in arithmetic hierarchy

Question

I was wondering what exactly the statement that "bounded quantifiers don't count" means in arithmetic hierarchy, and why it is the case formally.

For example, consider the set $S$ of programs $p$ that have finite domain. Then $$p\in S\iff (\exists N)(\forall x > N) (\forall z) \neg T(p,x,z)$$ where $T$ is the Kleene $T$-predicate. I suppose formally speaking, the RHS is $(\exists N)(\forall x) (x> N \to (\forall z) \neg T(p,x,z))$. How to show formally that $S$ is $\Sigma_2$? I'm okay with having sequences like $\forall x\forall z$ but I'm not sure how to handle bounded quantifiers.

Similarly, if $T$ is the set of programs with infinite domain, then $$p\in T\iff (\forall N)(\exists x)(x > N \to \forall z T(p,x,z))$$ in which case it's not clear to me why this is a $\Pi_2$ set.

Another kind of example: the set of programs $R$ that halt on all $x$ less than 100. Here we have $$p\in R\iff (\forall x)(x < 100 \to \exists z T(p,x,z))$$ Does the fact that "bounded quantifiers don't count" mean that I can completely ignore such quantifiers, and the set above is just $\Sigma_1$? If so, how to justify this?

Answer 1

The point is that bounded quantifiers can be "folded in" to the unbounded ones.

Consider for example an expression of the form $\exists x\forall y<x\exists z\varphi(x,y,z)$; let's show that this is $\Sigma_1$.

The idea is to borrow the "flavor" of Skolemization. There an expression of the form "$\forall a\exists b$" was reinterpreted as "$\exists F\forall a$" with $F$ a function designed to assign to each $a$ an appropriate $b$. Now in general that makes things more complicated, but here something very nice is going on: fixing $x$, a function sending each $y<x$ to some appropriate $z$ is actually a finite object and so can be coded by a single natural number.

So we rewrite our original expression as follows:

There is some pair $x,n$ where $n$ codes a sequence of length $x$ such that for every $y<x$ we have $\varphi(x,y, n[y])$ (where "$n[y]$" denotes the $y$th term of the sequence coded by $n$).

This is straightforwardly $\Sigma_1$ since the "coding/decoding apparatus" is all appropriately simple. The point is that now the bounded quantifier "$\forall y<x$" lives inside all of the unbounded quantifiers.