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.

  • $\begingroup$ I guess there's no point asking what $\operatorname{qr}(\phi)$ and $\operatorname{free}(\phi)$ mean? If I have to ask, then the question is over my head, is that it? $\endgroup$
    – bof
    Nov 11 '18 at 12:27
  • $\begingroup$ @bof Well, I've used pretty standard notation, but I'll add this in. $\endgroup$
    – blub
    Nov 11 '18 at 13:29
  • $\begingroup$ Is this from some text book or paper? Do you have a reference? I guess this is a very simple form of path reasoning à la Voevodsky homotopy type theory. I saw some paper already mentioning this simple case, cant find it right now. $\endgroup$
    – user4414
    Nov 12 '18 at 12:51
  • $\begingroup$ @j4n bur53 This is an old exercise I've found on a sheet from my university. I did not find it in any text book. $\endgroup$
    – blub
    Nov 12 '18 at 13:17

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


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

  • $\begingroup$ I am aware of this. The heading of my question is a mere appetizer for the underlying concept, however I'm trying to prove the exact claim as posed by me and not to distinguish sets of certain sizes per se. $\endgroup$
    – blub
    Nov 11 '18 at 18:29
  • $\begingroup$ There was a gap, I hope its now closed. The boolean combination is not along Libkins $\lambda_n$, something a little bit more general is needed. $\endgroup$
    – user4414
    Nov 12 '18 at 12:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.