ACA0 is the two-sorted arithmetic you get when you restrict the φ(x) we can substitute into the Comprehension Scheme to those which lack bound set variables. Note, however, that banning bound set variables in φ(x) still allows free set variables/parameters to occur. But why should we want to allow them? Unless I’ve missed a discussion, this obvious question seems usually to be passed over without very much comment. So let me try to plug the gap. (Not that it’s hard!)
Certainly, allowing free variables/parameters in the wffs φ(x) substituted into the Comprehension Scheme makes things technically sweet. But, as I’ve insisted here before, formal attractiveness is one thing, a decent conceptual motivation is something else. So — given a choice between either avoiding impredicativity by banning bound set variables in φ(x) or going the extra step and banning all set variables, bound or free — what principled reason is there for choosing between the resulting theories?
Well, let T be the theory which you get by banning all set variables from instances of φ(x); in other words, T requires instances of φ(x) to be open wffs of the language L1 of first-order arithmetic. Now, endorsing theory T requires us to hold that the open sentences of the L1 do indeed express cogent conditions which determine sets as their extensions — ‘arithmetical’ sets, as we’ll call them (otherwise, of course, we shouldn’t be endorsing even the restricted comprehension principle saying that there are such sets). Then, if X is such an arithmetical set, there is — according to us — a fact of the matter whether n ∈ X. So an open sentence of the language of first-order arithmetic augmented with a way of expressing that some number is in X also expresses a fully determinate condition. But then what reason can we possibly have for supposing that conditions expressed in the language of first-order arithmetic do determine sets as their extensions, while equally determinate conditions expressed in the augmented language which allows parameters acting as temporary names for arithmetic sets don’t have extensions? After all, if we arithmetically define a condition in terms of membership of some arithmetic set, then it will be equivalent to some purely arithmetical condition – so of course it has an extension!
Hence, if we are going to seriously countenance arithmetical sets at all and start quantifying over them, as in theory T, it seems we should also countenance sets arithmetically defined in terms of particular arithmetical sets. Which formally comes to allowing free set-variables/parameters in our comprehension principle after all, giving us ACA0.
‘Hold on! You just said that if we accept arithmetical sets, we should equally accept sets defined with parameters acting as temporary names for arithmetic sets. Fair enough. But the specification of ACA0 allows the wffs substituted into the comprehension schema to have parameters – free set-variables – without restriction. So doesn’t that overshoot?’ No. It is in fact not hard to show that the smallest model of ACA0 where the domain of the first sort of quantifier is the natural numbers has just the arithmetical sets as the domain of the second sort of quantifier (see Simpson, SOSAS, p. 317, Corollary VIII.1.11). So accepting ACA0 indeed commits us to no more than the arithmetical sets that we are committed to by T, just as we wanted.
As I said, this point about ACA0’s allowing set parameters in the comprehension principle usually seems to be passed over without real comment. Tim Storer, however, has reminded me that there is a relevant discussion by Azriel Levy, writing about the relation of VNB to ZF (see Fraenkel/Bar-Hillel/Levy, Foundations of Set Theory, 1973, ch. 3, §7, slightly reworked in Levy 1976). For the relation between ZF and VNB – also known as NBG – is in the key respect close to that between first-order PA and ACA0. In each case a single-sorted first-order theory is extended by adding a second sort of variable, running over sets/classes, whose use is governed by a predicative comprehension principle where substitutions for φ(x) lack quantifiers of the second sort. Levy’s central argument for allowing class parameters when substituting into Comp in the case of VNB turns out to be parallel to the argument above for allowing set parameters into φ(x) in the case of ACA0.
Or at least, I think that’s how things go …
Reading my comment I can’t see what I was thinking with “(iterating the Turing jump)”. Iterating the Turing jump has to do with the sets of ACA_0, not with the full induction axiom.
It occurs to me another thing people sometimes wonder about is just why ACA is stronger than ACA_0; that is, why does adopting the full induction scheme add strength? The answer, of course, is rather obvious: we get induction not only for arithmetical properties, but also for properties defined by quantification over arithmetical properties (iterating the Turing jump).
My favourite illustration of this is that there is a Sigma-1-1 truth predicate in ACA_0, that is, there is a Sigma-1-1 formula True(x) in the second-order language of arithmetic such that, provably (instance by instance) in ACA_0, True(“A”) <--> A. Applying induction to this formula, as we can do in ACA but not in ACA_0, we can carry out the trivial consistency proof for PA (and thus for ACA_0 which is, provably in ACA_0, conservative over PA). The formula can also be used to provide a finite axiomatisation for ACA_0.
Which brings me to my question: there is certainly a finite axiomatisation of ACA_0 analogous to the usual finite axiomatisation of NBG, not relying on the truth predicate. Being a lazy bastard, I’m disinclined to work out the details myself and thus would appreciate a pointer to such an axiomatisation. Perhaps it is found in SOSOA — which I don’t have access at the moment — or in _Metamathematics of First-Order Arithmetic_?