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.