In finite model theory, Ehrenfeucht-Fraïssé games gives us tools to prove inexpressibility results for FOL. Pebble games do the same for infinitary logic with finitely many variables.
Do we have such a framework to deal with Second order logics ? At least with $\Sigma_1^1$ and $\Pi_1^1$ ?
