My favorite example is the 5-quantifier definition of an [almost-periodic function][1]: $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. [1]: https://en.wikipedia.org/wiki/Almost_periodic_function