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:10Theory of Recursive Functions and Effective Computabilityby Hartley Rogers (1987, 2nd edition; also appears in 1967 1st edition):As has been occasionally remarked, the human mind seems limited in its ability to understand and visualize beyond four or five alternations of quantier. Indeed, it can be argued that the inventions, subtheories, and central lemmas of various parts of mathematics are devices for assisting the mind in dealing with one or two additional alternations of quantier.$\endgroup$ – Dave L Renfro Jun 5 '19 at 11:15