Proving that first-order formulas can not distinguish sets of a certain size Consider the set of first-order formulas over the empty signature, i.e. $\mathrm{FO}(\emptyset)$ (with variable set $Var$). The models over this signature are just characterized by their plain carrier set. Also, let $\mathrm{qr}(\phi)$ be the quantifier rank of a formula $\phi$ and $\mathrm{free}(\phi)$ the set of free variables.
For convenience, I consider first-order formulas just of being constructed by atomic formulas, negation, disjunction and existential quantification with the other common operations introduced as abbreviations. I want to show, that
For $\phi\in\mathrm{FO}(\emptyset)$ and sets $A\subseteq A'$ with $\beta:Var\to A$:
$$\text{If }|A|\geq\mathrm{qr}(\phi)+|\mathrm{free}(\phi)|\text{, then }A,\beta\models\phi\text{ iff }A',\beta\models\phi$$
by induction on $\phi$(or more specifically the quantifier rank of $\phi$).
I've already carried out the induction as far as I could. The base case, just consisting of atomic relational and equality formulas follows from the substructure lemma for quantifier free formulas. The cases for negation and disjunction are simple applications of the induction hypothesis.
What troubles me is the existential case: 
Assuming that $A,\beta\models\exists x\psi$ for some $A\subseteq A'$ with $|A|\geq\mathrm{qr}(\exists x\psi)+|\mathrm{free}(\exists x\psi)|$, we obtain that $\exists a\in A:A,\beta\frac{a}{x}\models\psi$. Now, as $|A|\geq\mathrm{qr}(\exists x\psi)+|\mathrm{free}(\exists x\psi)|$, we have $|A|\geq\mathrm{qr}(\psi)+|\mathrm{free}(\psi)|$ and thus by IH, we have that $\exists a\in A:A',\beta\frac{a}{x}\models\psi$ and as $A\subseteq A'$, we have that $A',\beta\models\exists x\psi$.
For the other directions, we suppose that $A',\beta\models\exists x\psi$, i.e. $\exists a\in A':A',\beta\models\psi$. I do not understand how I should now show that $A,\beta\models\exists x\psi$. I've tried augmenting or reducing $A$ by certain elements while keeping the prescribed bound, but this lead me nowhere.
 A: Assume $A', \beta \models \exists x\, \psi$. 
It means there's an $a'\in A'$ such that $A', \beta\frac{a'}x\models\psi$. 
If $a'\in A$, then we are done. 
Otherwise, since $A$ has at least as many elements as the variables used in $\psi$, there's an element $a\in A$ which is not assigned to any variable of $\psi$ by $\beta$. 
Because the only atomic formulas are equations, they become valid under the substitution $\beta\frac ax$ exactly when they do so under $\beta\frac {a'}x$ (because $a$ is different from each $\beta(y)$ where $y$ is another variable of $\psi$, just as much as $a'$ is). 
This proves $A, \beta\models\exists x\, \psi$. 
A: I would say your class of formulas admits a form of quantifier elimination. The result would be that every formula is equivalent to a boolean combination of these formulae:
a) Formulas of the form: $x = y$
b) Formulas of the form: $\exists x_1,..,x_m(x_{i1} \neq x_{j1} \wedge\,... \wedge\,x_{in} \neq x_{jn})$
Lets say a) are the positive formulas and b) are the negative formulas. The negative formulas $\phi = \exists \underline{x}\,\psi$ need not amout to Libkins $\lambda_n$. They can have $\mathrm{free}(\phi) \neq \emptyset$ and the matrice need not be a complete all distinct constraint.
The following rules contrribute to produce boolean combinations of formulas of the form a) and b):
$$\exists x(A \vee B) \Leftrightarrow \exists x A \vee \exists x B$$
$$\exists x(x = y \wedge A) \Leftrightarrow A\frac{y}{x}$$
But more is needed, the crucial lemma will be to reduce:
$$\exists \underline{x}(\psi \wedge
    \neg \exists \underline{x_1} \psi_1 \wedge\,... \wedge\,\neg \exists \underline{x_k} \psi_k)$$
Since $\psi$ gives a lower bound, and then the $\neg \psi_1, .., \neg \psi_k$ give upper bounds, I believe it can be shown that this amounts to:
$$\exists \underline{x}\psi \wedge
    \neg \exists \underline{x}\underline{x_1} (\psi \wedge \psi_1) \wedge\,... \wedge\,\neg \exists \underline{x}\underline{x_k} (\psi \wedge \psi_k))$$
See also, Definition (3.1) here:
Elements of Finite Model Theory
Leonid Libkin - 2012
http://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
