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?



Subscript 0 in Reverse Mathematics
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>


