I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that are not $\Pi^0_2$) you can express things, but they are not really necessary for proving a $\Pi^0_2$ theorem.

As part of this research I like to know if there are interesting/notable theorems in literature that actually proves a $\Sigma^0_n$ or $\Pi^0_{n+1}$ with $n \geq 2$ sentence (which is not $\Pi^0_2$). Such example would contradict my idea, because if according to my idea those sentences are not necessary, they are likely not be interesting. So, if they exists I like to study it.

Note, that if you use the axiom scheme for induction (in a notable proof) you may temporarily have a $\Pi^0_3$ sentence, but the obtained implication is mostly directly used and than falls back to a $\Pi^0_2$ sentence. So, I am not looking for that.

Finally, the result is different than with allowing to quantify over predicates, which does add strength and can prove things about ordinals etc.

Thanks in advance