Proving that first-order formulas can not distinguish sets of a certain size

first-order-logicinductionlogicquantifiers

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.

Best Answer

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$.

Related Question