 where \(\phi(x)\) can be any formula of the language of PA\(^2\) in which \(X\) doesn’t occur free. (It should be mentioned that PA\(^2\) can also be formulated by adding the primitive notion of  set membership \((\in)\) to the language, regarding the variables \(X, Y, Z,\ldots\), as explicitly ranging over sets, and reformulating second-order comprehension as \(\exists X\forall x[x \in X \leftrightarrow \phi(x)\)].)