The second approach for relating formal arithmetic to \(\textbf{PH}\) employs a series of second-order theories \(\mathsf{V}^0 \subseteq \mathsf{V}^1 \subseteq \ldots\) originally introduced by Zambella (1996) (see also Cook and Kolokolova (2001) and Cook and Nguyen 2010). These extend the first-order language \(\mathcal{L}_a\) with symbols \(\in\) and \(\lvert \cdot\rvert\) as well as the quantifiers \(\forall X\) and \(\exists X\) intended to range over finite sets of natural numbers. The theory \(\mathsf{V}^1\) extends \(\mathsf{Q}\) with second-order quantifier axioms, extensionality for sets, axioms formalizing that \(\lvert X\rvert\) is intended to denote the largest element of \(X\), and a second-order comprehension schema for \(\Sigma^B_1\)-formulas – i.e. formulas containing only bounded first-order quantifiers and set quantifiers of the form \(\exists  X(\lvert X\rvert \leq t)\) (where \(t\) is a first-order term not containing \(X\)). In parallel to Theorem 4.7, it can be shown that a function \(f(\vec{x})\) is in \(\textbf{FP}\) just in case it is definable by a \(\Sigma^B_1\)-formula relative to which it is provably total in \(\mathsf{V}^1\). Similar characterizations of the classes \(\Box^P_i\) may be obtained by considering the theories \(\mathsf{V}^i\) (for \(i &gt; 1\)) obtained by extending comprehension to wider classes of bounded second-order formulas.