I am posing this question based on this answer which asserts that the Riemann Hypothesis is a $\Pi_1^0$ statement while $\mathsf{P}$-vs-$\mathsf{NP}$ is a $\Pi^0_2$ statement ("for every code for a machine of such and such kind there is a code for a machine of such other kind such that ..."). I found it quite surprising that even some of the most complex and deep open questions in mathematics are expressible with formulas of such low complexity. I suppose that formula complexity has nothing to with the question of "how hard is it to prove this statement".
This leads me to my questions:
Are there any known useful mathematical theorems or statements that are only expressible as hyperarithmetic or analytic statements, i.e. that are known to strictly lie above $\Delta^1_0$ on the arithmetic or analytic hierachy?
In other words, what is the highest complexity theorem that exists? (If that even is a sensible question to ask.)
Any mathematical or philosophical answers would be much appreciated!
I don't know what counts as "useful" to you, but one example is the following sentence $\varphi$: "There is a well-founded model of ZFC."
$\varphi$ is presumably true, although of course this can't be proven in ZFC because of Gödel's incompleteness theorem. (It can be proven, for example, in the theory ZFC + "there exists a strongly inaccessible cardinal," although that's actually much stronger than $\varphi.)$
$\varphi$ is $\Sigma^1_2,$ as you can see by writing out what it means, coding countable structures as real numbers.
But $\varphi$ is not $\Pi^1_1.$ This is because $\Pi^1_1$ sentences are downward absolute: any true $\Pi^1_1$ sentence holds in every transitive model of ZF. But $\varphi$ is not true in the minimal transitive model of ZFC, even though $\varphi$ is actually true. (Again, the existence of that model is presumably true but requires a little bit more than ZFC to prove.)