Finite list of axioms of $\mathsf{ACA}_0$ - reference? It seems to be common knowledge that $\mathsf{ACA}_0$ can be finitely axiomatized, see for example
Can a finite axiomatization of PA be expressed in a finitely axiomatizable first order set theory?
However, I cannot seem to find a reference where $\mathsf{ACA}_0$ is given explicitly with the finite list of axioms. It is always defined as an extension of $\mathsf{PA}$ which already has an infinite axiom scheme.
Is there some reference giving the finite axiom list explicitly or is the above result of finite axiomatizability a non-constructive existential statement?
I hope this is the right place to ask for references. Delete this and PM/Mail me if not.
 A: A finite axiomatisation for $\mathsf{ACA}_0$ is given by lemma VIII.1.5 of Simpson [2009], on pages 311–312. Fix a universal lightface $\Pi^0_1$ formula $\pi(e, m_1, X_1)$ with exactly the displayed free variables. Then we can give a finite axiomatisation of $\mathsf{ACA}_0$ as follows.
1) The basic axioms, essentially the axioms of Peano arithmetic minus the induction scheme (see definition I.2.4 on page 4 of Simpson [2009]).
2) A pairing axiom,
$$\forall{X}\forall{Y}\exists{Z} (Z = X \oplus Y).$$
3) $\Sigma^0_1$ induction in the form
$$\forall{X}(\neg\pi(e, 0, X) \wedge \forall{m}(\neg\pi(e, m, X) \rightarrow \neg\pi(e, m + 1, X))) \rightarrow \forall{m} \neg\pi(e, m, X)).$$
4) $\Sigma^0_1$ comprehension in the form
$$\forall{X}\exists{Y}\forall{m}(m \in Y \leftrightarrow \neg\pi(e, m, X)).$$
The universal $\Pi^0_1$ formula $\pi$ will of course be something of the sort discussed in Peter Smith's blog post.
S. G. Simpson. Subsystems of Second Order Arithmetic. Cambridge University Press, 2nd edition, 2009. doi:10.1017/cbo9780511581007.
A: I have a blogpost about this at http://www.logicmatters.net/2007/09/14/aca0-3-finite-axiomatizability/ (as has been pointed out!).
The finite axiomatization you get this way, however, is not particularly pretty or illuminating or, you might think, so "natural".
