For any two non-isomorphic graphs $G, H$, does there exist a polysize, polylog quantifier depth first order formula which witnesses this? I want to be very specific. Does anyone know of a disproof or a proof of the following proposition:

$\exists p \in \mathbb{Z}[x], n, k, C \in \mathbb{N},$ 

$\forall G, H \in STRUC[\Sigma_{graph}] (min(|G|, |H|) = n, G \not\simeq H),$

$\exists \varphi \in \mathcal{L}(\Sigma_{graph}),$ 

$|\varphi| \leq p(n) \wedge qd(\varphi) \leq Clog(n)^k \wedge G \vDash \varphi \wedge H \nvDash \varphi.$

Intuitively, this should be true if all non-isomorphic graphs can be distinguished using "$Clog(n)^k$ local" statements, and I'd imagine that this is false. Of course any graph can be distinguished using polynomial quantifier depth, as you can simply specify your graph modulo isomorphism:

$\varphi = \exists x_1 \exists x_2 \exists x_3 ... \exists x_n (\forall x (\bigvee_{i \in V_G} x = x_i) \wedge (\bigwedge_{(i, j) \in E_G} E(x_i, x_j))) \wedge (\bigwedge_{(i, j) \notin E_G} \neg E(x_i, x_j))) \wedge (\bigwedge_{(i, j) \in V_G^2 \mid i \neq j}x_i \neq x_j).$

Edit: So it seems that the locality intuition I had is false. A formula of quantifier depth $k$ has Gaifman locality bounded by $O(3^k)$, which means that a log depth formula is basically global. For this reason, I have a hunch the proposition will turn out to be true, which would be much harder to prove in my opinion.
Thanks to my colleague Maxim Zhukovskii for suggesting this answer.

It turns out that the answer is negative, and the counterexample is rather simple. Just take $G=K_m\sqcup \overline{K_m}$ and $H=K_{m+1}\sqcup \overline{K_{m-1}}$ for $n=2m$ and $G=K_m\sqcup \overline{K_{m+1}}$ and $H=K_{m+1}\sqcup \overline{K_m}$ for $n=2m+1$. (Here $K_s$ is an $s$-clique and $\overline{K_s}$ is a set of $s$ isolated vertices). By considering the Ehrenfeucht game one can show that in the first case the minimal possible depth is $m$ and in the second case it is $m+1$.

It was shown in the paper "The first order definability of graphs: Upper bounds for quantifier depth" by Oleg Pikhurko, Helmut Veith and Oleg Verbitsky that this bound is almost tight and any two $n$-vertex graphs are distinguishable by a formula of depth $\frac{n+3}{2}$.