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.



Independence of $\Pi^1_1$-induction from ATR$_0$
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$.


