Aatu (in his comment on a previous post) raises two issues, one about the finite axiomatiability of ACA0, and one about the relation between ACA0 and ACA. I think there are some conceptually slightly puzzling issues about the second issue, and I’ll come back to that when I feel I’ve got them straighter. As to finite axiomatiability, here’s one line of proof (essentially, Simpson’s, I hope!).
ACA0 is equivalent to the theory we could dub ΣCA, which is what you get by restricting the comprehension principle to Σ1 wffs (with second-order parameters), by an induction proof relying on the easy observation that Σn comprehension implies Σ(n+1) comprehension. So it is enough to show that ΣCA is finitely axiomatizable.
Now recall that the extension of a Σ1 wff φ(x) (without second-order parameters, for the moment) has as its extension a recursively enumerable set that can be enumerated by some Turing machine or other (the e-th machine in a certain enumeration). And recall too the possibility of universal Turing machines: there is, in a particular, a universal machine which takes as input the index e and enumerates the set enumerated by the e-th machine. That means that there is a ‘universal’ Σ1 wff U(w, x) such that for any Σ1 wff φ(x) there is some e such that it is provable in first-order arithmetic that φ(x) ↔ U(e, x), where ‘e’ is the numeral for e.
We can now generalize that line of thought, to the case where φ(x) has second-order parameters, and show similarly that there is a ‘universal’ Σ1 wff U(w, x, Y) such that for any Σ1 wff φ(x, Y) there is some e such that it is provable in first-order arithmetic that φ(x, Y) ↔ U(e, x, Y). So a comprehension schema that allows all instances for Σ1 wffs φ(x, X) can be replaced by a single comprehension axiom
∀w∃X∀x(x ∈ X ↔ U(w, x, Y)).
Adding a few bells and whistles, it quickly follows that ΣCA can be finitely axiomatized.