What are some natural properties, definitions, and statements that require many alternating quantifiers?

The complexity could be $Π^0_k$, $Π^1_k$, $Π^V_k$, or something else entirely, as long $k$ is not too small, and the statement is naturally viewed for a fixed $k$, as opposed to a part of a schema that works independent of $k$. More obscure/complicated examples require a higher $k$ to qualify.

Here are five examples:

Definition/existence of a limit (and many related concepts) is $Π^0_3$-complete. (Also, there should be natural $Σ^0_4$/$Π^0_4$-complete properties related to limits, but I have not really found them -- except for the next item.)

I conjecture that existence of an $n^{1+o(1)}$ algorithm for a given decision problem is $Σ^0_4$-complete (even if the problem is in P and coded as such).

"Every closed set is the union of a countable set and a perfect set" is $Π^1_3$ (and equivalent to $Π^1_1-\mathrm{CA}_0$ over $\mathrm{RCA}_0$).

The axiom of choice is $Π^1_4$ conservative over ZF (but without large cardinal axioms, it is not $Σ^1_4$ conservative).

Existence of a proper class of extendible cardinals is $Π^V_5$.

First order logic allows an arbitrary number of quantifiers, but other than through schemas (which can often be viewed as an approximation to a single higher order quantifier), mathematical practice rarely uses many alternating quantifiers. So rarely that quantifiers were not formalized in a general form until the second half of the 19th century. The high quantifier complexity of limits is essentially the reason that limits were not formally defined until after much of mathematical analysis was developed. However, 'rarely' does not mean 'never', and the question is to identify some of the exceptions.

*Update:* Here are three more examples:

Whether $f(x)$ is continuously differentiable at $x_0$ is $Σ^0_4$-complete. By contrast, differentiability at $x_0$ or continuous differentiability on $(a,b)$ is $Π^0_3$.

Given a countable metric space (coded by an enumeration of all points and distances) that we are promised is locally complete (or even complete), whether the space is locally compact is $Π^0_5$-complete. Note that a metric space is locally compact iff it is locally complete (which for countable spaces is $Π^1_1$-complete) and every point has a totally bounded neighborhood (which for countable spaces is $Π^0_5$-complete).

In set theory, "$κ$ is ineffable" is $Π^1_3$ in the second order logic over $V_κ$.

How complicated can structures be?. Nieuw Archief voor Wiskunde. Juni 2008. Note that $\bigcap\bigcup$-alternations, while not strictly speaking 'quantifier-alternations' are 'quantifier-alternations-in-disguise'. $\endgroup$ – Peter Heinig Sep 24 '17 at 16:10