Examples of statements with a high quantifier complexity 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_κ$.
 A: Consider the statement:


*

*"Neither player has a winning strategy in the game of Tic-tac-toe."


This is a natural statement, often asserted and believed, and the most natural formulation of it has complexity $\Sigma_9\wedge\Pi_9$. 
To be sure, statements about game strategies often generally involve very high quantifier complexity. The assertion that player I has a winning strategy in a game of length $k$, after all, is most naturally a $\Sigma_k$ assertion, of the form: 

"There is a move for player I, such that for any reply, there is a further move for player I, such that for any reply, there is a further move,... after which player I has won the game."

In the case of tic-tac-toe, the game has at most nine moves, and so we have nine quantifiers in the statement. The assertion that neither player has a winning strategy is equivalent, by the fundamental theorem of finite games, to the assertion that both players have drawing strategies.
Longer games naturally give rise to assertions with even more quantifiers. For example, the corresponding statement about chess would have enormous quantifier complexity, bounded essentially by the length of the longest chess game.
Meanwhile, of course, one can subsume the first-order quantifiers into a higher-order quantifiers by talking about strategies. This amounts to trading high first-order quantifier complexity for low higher-order quantifier complexity.
A: One example from dynamical systems is the specification property, which needs 5 quantifiers.  It was introduced by Rufus Bowen in the 1970s to study equilibrium measures of dynamical systems; for example, it implies that the limiting distribution of periodic orbits is the unique measure that maximizes entropy as long as the system is expansive.  It comes in various versions, which are not quite all equivalent, but let me ignore these subtleties and just quote one.
Given a compact metric space $X$, a continuous map $f\colon X\to X$ has the specification property if $\forall\epsilon>0$, $\exists T>0$ such that $\forall (x_1,n_1),\dots,(x_\ell,n_\ell)\in X\times \mathbb{N}$, $\exists y\in X$ such that $\forall 1\leq k\leq \ell$ and $0\leq j < n_k$, we have $d(f^{N_k + j}(y),f^j(x_k)) < \epsilon$, where $N_k = \sum_{i=1}^{k-1} (n_i + T)$, and we also have $f^{N_\ell+n_\ell+T}(y)=y$.
Roughly speaking it says that any finite collection of orbit segments can be shadowed by a periodic orbit that takes a bounded time $T$ to transition from each one to the next, and that $T$ depends only on how precise the shadowing is required to be.
A: In computability theory, a set of integers $A$ is infinitely often computably traceable if there is a computable function $h$ such that for all functions $g\le_T A$ ($g$ computable from $A$), there is a computable sequence $T$ of finite sets $T_n$, $n\ge 0$, such that for infinitely many $n$, $g(n)\in T_n$, and for all $n$ the size of $T_n$ is at most $h(n)$.
If you unpack this it is $\Sigma^0_5$: there is an $h$ such that for all $g$ there is a $T$ such that for all $m$ there is an $n>m$ with $g(n)\in T_n$.
A: The pumping lemma (for rational languages) states that


*

*for every rational language $L \subseteq \Sigma^*$ (over a finite alphabet $\Sigma$),

*there exists an integer $p$ such that,

*for every word $w\in L$ with $|w|\geq p$,

*there exists a factorization $w = xyz$ such that $|y|\geq 1$ and $|xy|\leq p$ and

*for every $i\geq 0$ we have $xy^iz\in L$.
So it has quantifier complexity $5$.
I like this example because it is not too sophisticated, but still pedagogically interesting.  I teach an elementary course in formal languages theory in which this lemma is discussed, and many students have difficulty coming to terms with it (or how to use it) because of the quantifier subtlety; so it's worth taking the time to explain the logic.  I try to emphasize (in a sort of game-theoretic point of view) that, when you apply a result like this, you get to choose every object that is introduced with "for all" but those quantified by "there exists" are imposed upon you (whereas when proving such a result, things are the other way around).  Despite this, many students continue to believe they can choose the factorization they want.
A: My favorite is still the Hilbert-Waring theorem.  It is only $\Pi_3^0$ but it is a natural statement understandable by anyone, that has a venerable mathematical history.
A: My favorite example is the 5-quantifier definition of an almost-periodic function: $f$ is almost-periodic iff
$$\forall \epsilon>0\, \exists t>0\ \forall a\ \exists s \in [a,a+t]\ \forall x\, |f(x+s)-f(x)| \leqslant \epsilon.$$
Using the fact that almost periodic functions are uniformly continuous, one can show that this is equivalent to a 3-quantifier property.  The 5-quantifier definition remains the more natural one, especially for the purpose of stating the above fact.
So Bohr's theorem that every almost-periodic function has arbitrarily good appropximations by trigonometric polynomials is naturally written as a 6-quantifier statement.
PS Thanks to @FrancoisZiegler and @DmytroTaranovsky for sorting me out on this.
A: I believe the notion of a pseudo-convergent sequence in an Abelian group with valuation is a good candidate -- it is a generalization of the notion of convergent sequences and limits over the reals.

Let $\mathbb{G}$ be an additively written ordered Abelian group with extended value class $EVC(\mathbb{G})$ ordered by anti-inclusion, and valuation $\nu:\mathbb{G}\rightarrow EVC(\mathbb{G})$. Also let $\lambda$ be a non-zero limit ordinal, with $\{g_\alpha\}_{\alpha<\lambda}$ a $\lambda$-termed sequence in $\mathbb{G}$. We say that $\{g_\alpha\}_{\alpha<\lambda}$ is pseudo-convergent in $\mathbb{G}$ relative to $\nu$ iff for all $\alpha<\beta<\gamma<\lambda$, $$\nu(g_\alpha-g_\beta)\prec\nu(g_\beta-g_\gamma).$$ Further, $x$ is a pseudo-limit of $\{g_\alpha\}_{\alpha<\lambda}$ iff $$\nu(g_\alpha-x)=\nu(g_\alpha-g_{\alpha+1})$$ for all $\alpha<\lambda$.

A: The Interchange lemma in the theory of formal languages has a $\Pi_5$ form:

$\forall L$, if $L$ is a context-free language, then
$\exists c$, $c$ is a positive integer, such that
$\forall n\ge 2$, $R\subseteq L\cap\{0,1\}^n$, $2\le m\le n$,
$\exists Z\subseteq R$, $Z=\{z_1,\dots,z_k\}$, $z_i=w_ix_iy_i$, $k\ge \frac{|R|}{c(n+1)^2}$, and lengths $a,b,c$, such that
$\forall i,j$ with $1\le i,j\le k$, [$|w_i|=|w_j|$, etc. etc.]

The most famous application is to let $L$ be the set of not-square-free words, assume it's context-free, and then carefully choose $R$ and $n$ so as to get a contradiction.
