Question about proof of Kannan's Theorem
Following your way:

Let us denote by $C_{n,s,i}$ the i'th $n$ inputs, $s$ size circuit (relative to the lexicographic ordering of the strings describing such circuits), Then:

$x\in L \iff \exists i \hspace{1mm} \phi\left(C_{|x|,|x|^{k+1},i}\right)\forall j&lt;i : \neg \phi\left(C_{|x|,|x|^{k+1},j}\right)\land C_{|x|,|x|^{k+1},i}(x)=1$.

$\phi(C)$ is a formula which states that $C$ cannot be computed by an $n^k$ size circuit, and can be written as a $\Pi_2$ statement (as you did in your original post).

The idea is the same as yours, trying to decide some language in $SIZE(n^{k+1})\setminus SIZE(n^k)$. The only addition is using the lexicographic ordering and forcing minimality. This way we force that for any length $n$ string, the quantification over the circuit index $i$ yields the same circuit.

After grouping the quantifiers (and moving $\forall j&lt;i$ right after $\exists i)$ you get a $\Sigma_4$ formula.