Theorem in ACA that is unprovable in $Π^1_1$-CA$_0$? Question
Is there a (preferably natural combinatorial) theorem in ACA that cannot be proven in $Π^1_1$-CA$_0$?
Motivation
On reading many introductory materials on reverse mathematics, there seems to be a focus on subsystems of arithmetic that do not have the full induction schema. In particular there are two systems ACA$_0$ and $Π^1_1$-CA$_0$, the former being predicative while the latter being impredicative. By predicative I mean that one is only allowed to construct collections that quantify over previously constructed collections.
However, in my mind the motivation for ACA$_0$ is that we already assume the existence of natural numbers, and that membership of a natural number in an arithmetical set has a definite answer, even if we cannot figure out the answer. (The justification for the latter could be via using game semantics to interpret quantified statements, and then arguing that finite games are determined, but that is not the point of my question.) Since we assume the natural numbers as some fixed and complete collection, which is somewhat necessary to justify that arithmetical sets are well-defined, we also would not be wrong in adding full induction in the form of the second-order axiom schema "$P(0) \land \forall n\ ( P(n) \to P(n+1) ) \to \forall n\ ( P(n) )$" for every predicate $P$ (which can have second-order quantifiers).
But that gives us ACA and not just ACA$_0$. I am aware that ACA proves Con(PA) unlike ACA$_0$, so ACA is strictly stronger. At the same time $Π^1_1$-CA$_0$ is strictly stronger than ACA$_0$ and also proves Con(PA), but is it strictly stronger than ACA? I guess I am asking a well-known question with a well-known answer, but I do not know how to find it.
 A: $\Pi^1_1$-CA is indeed strictly stronger than ACA. They both share the full induction scheme, so to compare them we only need to look at their comprehension parts. ACA contains comprehension for arithmetic formulas, while $\Pi^1_1$-CA contains comprehension for $\Pi^1_1$ formulas; since every arithmetic formula is $\Pi^1_1$ but not conversely, $\Pi^1_1$-CA is strictly stronger than ACA.
Meanwhile, the systems $\Pi^1_1$-CA$_0$ and ACA are incomparable: there are models of $\Pi^1_1$-CA$_0$ which fail the full induction scheme, and hence are not models of ACA, but e.g. the $\omega$-model of arithmetic sets is a model of ACA in which $\Pi^1_1$-CA$_0$ fails.
However, $\Pi^1_1$-CA$_0$ does have quite a lot of induction: we trivially get induction for all $\Pi^1_1$ formulas. And this means it's going to be hard to find the examples you want. Classical combinatorial principles like Ramsey's theorem, Koengi's lemma, and the like tend to use only arithmetic induction, and not much of that. I'm not aware of a single combinatorial principle which requires high-level induction, which does not also require high-level comprehension (which would push it out of the range of ACA). So I don't think you're going to find a natural example of a combinatorial consequence of ACA which is not provable in $\Pi^1_1$-CA$_0$.
Interestingly, any model $M$ of $\Pi^1_1$-CA$_0$ can be "cut down" to a model of ACA: let $N$ have the same first-order part as $M$, and have second part consisting of the arithmetic sets in $M$. Then it's not hard to check that $N$ satisfies ACA, the point being that each instance of the full induction scheme in $N$ corresponds to a $\Pi^1_1$ instance of the induction scheme in $M$, which holds there. I suspect that this can easily be tweaked to get an argument that $\Pi^1_1$-CA$_0$ proves the consistency of ACA, but I don't immediately see it.
