Aatu (in his comment on a previous post) raises two issues, one about the finite axiomatiability of ACA_{0}, and one about the relation between ACA_{0} 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!).

ACA_{0} 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.

Duh! I should have remembered that Sigma-n comprehension implies Sigma-n+1 comprehension… (The proof, incidentally, is essentially just what you get if you spell out the proof based on the truth predicate, or, rather, the portion about the existence of the truth predicate). Ah well, so it goes.

As to the conceptual conundrum, perhaps you’re referring to the problem of why should we find full induction acceptable while accepting comprehension only for arithmetical formulas? This is something I’ve been idly puzzling over now and then, with no conclusion or insight, alas; it is perhaps also related to the question of what exactly counts as “natural motivating conceptual picture”. I’d be interested in anything you have to say on this.