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.

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.