The two-variable fragment of first-order logic (short: \(\mathrm {FO}^2 \) ) restricts first-order logic to the use of only two variables, which can be reused arbitrarily in a formula. The two-variable fragment of existential second-order logic (short: \(\mathrm {ESO}^2 \) ) consists of all formulas of the form \(\exists R_1\ldots \exists R_k \varphi \)  where \(R_1,\ldots ,R_k\)  are relation variables and \(\varphi \)  is a \(\mathrm {FO}^2 \) -formula. Since each \(\mathrm {FO}^2 \) -atom can contain at most two variables we assume, from now on and without loss of generality, that all relation symbols are of arity at most two; see [1]} for a justification. Restricting the set quantifiers of \(\mathrm {ESO}^2 \)  to be unary yields the fragment \(\mathrm {EMSO}^2 \) .
