Necessity of omega-models in second order arithmetic

Question

Are there examples of independence results over subsystems of true second order arithmetic that cannot be established using omega-models? To rule out trivial examples, let us assume that the base theory extends true first order arithemtic. A non example of such a statement would be Ramsey theorem for pairs since there is a computable coloring of pairs of integers into two colors without a computable (even from the halting problem, Jockusch) infinite homogeneous set.

An example of a use of non-omega models appears here - Also, see the introduction and question 6.1 in this paper.

I am not an expert in reverse mathematics so please feel free to offer any interesting known facts known to you here.

Answer 1

Yes, of course there are. Any result that is equivalent to extra induction axioms will require nonstandard models for a semantic separation.

For example, Hirst proved that the pigeonhole principle $\mathsf{RT}^1_{<\infty}$ is equivalent to $B\Sigma^0_2$, and thus is not provable in $\mathsf{RCA}_0$. But $B\Sigma^0_2$ holds in every $\omega$-model.

Similarly, there is a variation of $\mathsf{ACA}_0$, denoted $\mathsf{ACA}'_0$, which has an axiom asying that for all $n$, $0^{(n)}$ exists. In contrast, $\mathsf{ACA}_0$ only proves that $0^{(n)}$ exists for standard $n$. So every $\omega$-model of $\mathsf{ACA}_0$ is a model of $\mathsf{ACA}'_0$.

For an example with non-arithmetical induction: $\mathsf{ACA}_0$ plus $\Sigma^1_1$ induction proves the consistency of $\mathsf{ACA}_0$, so $\mathsf{ACA}_0$ does not prove $\Sigma^1_1$ induction.