The [Interchange lemma][1] 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.

  [1]: https://en.wikipedia.org/wiki/Interchange_lemma