[FOM] ACA

[pax0 at seznam.cz]

Suppose we have the comprehention scheme in Z_2
EXAn(n in X <--> phi(n))
and phi is not Arithmetical.

Are there some trivial cases in which we can make phi arithmetical by pushing
some quantifiers in front of the whole formula, especially this:
phi(n) is prefixed by a string of universally quantified 2nd order variables.
Can we push them in front of the whole formula thus making them parameters
and the whole formula arithmetical, and yet the two formulas left equivalent?
Thank you, Jan Pax