Question

What does the subscript 0 mean on terms like $\mathsf{ATR}_0$? Does it mean the same thing in $\Pi^1_k\text{-}\mathsf{CA}_0$?

If I frame higher order analogues of these, should I change that subscript?

Answer 1

As the other answer points out, the subscript 0 means restricted induction. However, without the subscript 0, there are two conventions:

• The older convention was that the systems without the subscript 0 have the full second-order induction scheme. Thus $\mathsf{ACA}$ is the system consisting of $\mathsf{ACA}_0$ plus the full induction scheme, and the same for e.g. $\mathsf{WKL}$ vs. $\mathsf{WKL}_0$. Historically, the systems with full induction were studied first (as in Feferman's article in the Handbook of Mathematical Logic), and the systems with restricted induction were of secondary interest. The restricted systems drew more interest once it was apparent how many mathematical results they can prove, so that in the context of reverse mathematics the systems with full induction seem less natural.

• Some authors, however, use ACA to mean "Arithmetical Comprehension Axiom" and WKL to mean "Weak König's Lemma". For these authors, $\mathsf{ACA}_0$ is $\mathsf{RCA}_0$ plus "ACA". Similarly $\mathsf{WKL}_0$ means $\mathsf{RCA}_0$ plus "WKL". This terminology appears in various papers, even some published by respected proof theorists, and so you have to watch for it. Note that ACA here can be taken to be a single sentence "for all $X$ the Turing jump of $X$ exists" and similarly WKL is a single sentence.

For higher-order analogues, it is still a question whether restricted induction or full induction is included. Kohlenbach [1] has used notation such as $\mathsf{ACA}_0^\omega$ to refer to the analogue of $\mathsf{ACA}_0 $ formalized in arithmetic in all finite types. In this context, though, there are many different ways in which induction can be restricted. So notation like $\widehat{\mathsf{E\text{-}HA}}^\omega_\upharpoonright $ is used in the literature, where the hat and the harpoon refer to different sorts of restrictions. These notations are explained in Kohlenbach's Applied Proof Theory or in Troelstra's Metamathematical Investigations.

1: Ulrich Kohlenbach, "Higher Order Reverse Mathematics", Reverse Mathematics 2001, Lecture Notes in Logic, 2005, ftp://ftp.daimi.au.dk/BRICS/RS/00/49/BRICS-RS-00-49.pdf

Answer 2

The subscript $0$ is meant to indicate the amount of induction that the theory has.

The wikipedia entry on Reverse mathematics says of the big five theories of reverse mathematics that

The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme (Simpson 2009, p. 6). For example, $\text{ACA}_0$ includes the induction axiom (0∈X ∧ ∀n(n∈X → n+1∈X)) → ∀n n∈X. This together with the full comprehension axiom of second order arithmetic implies the full second-order induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀n φ(n) for any second order formula φ. However $\text{ACA}_0$ does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.