Motivation for the (arithmetic) 'collection axioms' $B\varphi$

Question

I am reading Richard Kaye's Models of Peano Arithmetic. In chapter 7 we define the collection axioms $B\varphi$ for $\mathscr L_A$-formulas $\varphi$ which are, to quote, 'the arithmetic analogue of Fraenkel's collection principle in set theory'. I could not find other sources which mention them, so I copied the definition below.

What is the motivation for this definition? Is there a way to simplify the definition of the theory $B\Sigma_n$ in words?

Thank you!

---

Let $\varphi(x,\overline y,\overline z)$ be a formula of $\mathscr{L}_A$. The collection axiom for $\varphi$ is the sentence $B\varphi$, which is $$\forall\overline z,t\big(\forall x<t\;\exists \overline y\;\varphi(x,\overline y,\overline z)\rightarrow \exists s\;\forall x<t\;\exists\overline y<s\;\varphi(x,\overline y,\overline z)\big).\tag{1}$$ Then $B\Sigma_n$ is the theory $$I\Delta_0+PA^-+\{B\varphi:\varphi\;\text{is a}\;\Sigma_n\;\mathscr{L}_A\text{-formula}\}.$$

$(1)$ seems to say that whenever for certain $t$s we can find arbitrary $\overline y$s to satisfy $\varphi$, then we can do it for $\overline y$s bounded by a certain $s$. In passing it is remarked that the collection axioms can be used to show that the classes $\Sigma_1$ and $\Pi_1$ are closed under bounded quantification—which I take to mean that if $\varphi$ is $\Sigma_1$ (or $\Pi_1$), then for any $x$, $\exists x<a\varphi$ (or $\forall\dots$) is also $\Sigma_1$ (or $\Pi_1$)—though this is not obvious to me.

Answer 1

The "collection axioms" are also called the "bounding scheme".

More intuitively put, the bounding principle for a formula $\phi(x,y)$ says that, for all $t \in \mathbb{N}$, if $\phi(x,y)$ defines a function (call it $f$) from $\{0, \ldots, t\}$ to $\mathbb{N}$, then the range $\{f(0), \ldots, f(t)\}$ is bounded. As stated in the axiom, though, $f$ might be a multifunction, and we just need each $x < t$ to have some witness less than the bound.

Another intuitive way of stating the scheme is as a dual to the pigeonhole principle about an infinite number of pigeons and a finite number of boxes. The bounding scheme says that we cannot fill an infinite (i.e. unbounded) set of boxes with a finite number of pigeons.

The bounding scheme is a consequence of the induction scheme, of course, but it is of independent interest. The bounding scheme is discussed in other books on formal arithmetic, such as Metamathematics of First-Order Arithmetic by Hajek and Pudlak.

For bounded quantification in particular, one important case is when we have a formula of the form $(\forall x < t)(\exists y)\, \psi(x, y, \ldots)$ and we want to move the $\exists$ quantifier outward. By the bounding scheme, our starting formula is equivalent to $(\exists p)(\forall x < t)(\exists y < p)\, \psi(x,y,\ldots)$. So we can push a bounded universal formula across an unbounded existential formula.

The other important case is when we have $(\exists x < t)(\forall y) \, \psi(x,y,\ldots)$. We rewrite this as $\lnot \lnot (\exists x < t)(\forall y)\,\psi(x,y,\ldots)$, i.e. $$\lnot [ (\forall x < t)(\exists y)\,\lnot\psi(x,y,\ldots)] .$$ By the method above, rewrite this as $$\lnot [(\exists p)(\forall x < t)(\exists y < p) \, \lnot \psi(x,y,\ldots)].$$ Then we have the original formula equivalent to $(\forall p)(\exists x < t)(\forall y < p) \psi(x,y,\ldots)$. So we can push a bounded existential quantifier over an unbounded universal quantifier. (It may not be immediately clear that the latter formula is equivalent to the starting one, even in the standard model, but remember that every $t$-coloring of $\mathbb{N}$ has an infinite monochromatic set.)