Is it known that $\Pi^1_1$-induction is independent of ATR$_0$? Simpson's book shows this for $\Pi^1_1$ transfinite induction ($\Pi^1_1$-TI), but I'm only interested in inducting on $\omega$.
I can show that ATR$_0$ + $\Pi^1_1$-induction implies $\Sigma^1_1$-TI, but unlike simpler inductions, it's not clear that the $\Pi$ and $\Sigma$ forms are equivalent here.
Let me sketch the proof that $\mathsf{ATR}_0+\Pi^1_1\textsf{-Ind}\vdash\mathsf{Con}(\mathsf{ATR}_0)$ (by Gödel's 2-nd incompleteness this implies that $\mathsf{ATR}_0$ doesn't prove $\Pi^1_1\textsf{-Ind}$).
We reason in $\mathsf{ATR}_0+\Pi^1_1\textsf{-Ind}$. Assume for a contradiction that $\mathsf{ATR}_0$ isn't consistent. Recall that $\mathsf{ATR}_0$ could be axiomatized over first-order logic by a single $\Pi^1_2$ sentence (i.e. sentence of the form $\forall \vec{X}\exists \vec{Y}\;\varphi$, where $\varphi$ doesn't contain second-order quantifiers). By our assumption there is a FOL proof of $\lnot \forall \vec{X}\exists \vec{Y} \;\varphi$. So we have a cut-free Tait calculus proof $P$ of the sequent $\exists \vec{X}\forall \vec{Y} \;\lnot \varphi$. We prove by $\Pi^1_1$-induction on the $P$-subproofs $$\displaystyle\frac{\ldots}{\Gamma}$$ that the universal closure of $\bigvee (\Gamma\cap \Pi^1_1)$ is true. The main point in this proof by induction is that when some new non-$\Pi^1_1$ arise the last rule should have been of the form $$\displaystyle \frac{\Delta,\forall \vec{Y}\;\lnot \varphi}{\Delta,\exists X_n\forall \vec{Y}\;\lnot \varphi}$$ and since we know that actually $\forall \vec{X}\exists \vec{Y} \varphi$, in fact $\forall \vec{Y}\;\lnot \varphi$ was false on any value of parameters $\vec{X}$ and hence the universal closure of $\bigvee (\Delta \cap \Pi^1_1)$ was true. For the case of the whole derivation $P$ we see that the universal closure of the empty disjunction is true, contradiction.
Note that the same argument shows that over $\mathsf{RCA}_0$ the principle $\Pi^1_1\textsf{-Ind}$ is equivalent to uniform $\Pi^1_3$-reflection for $\mathsf{RCA}_0$.
