# Proving a biconditional relation between wfs $B$ and $C$, where $C$ is obtained by erasing all quantifiers from $B$

I work on the following problem in first order logic: If $C$ is obtained from $B$ by erasing all quantifiers $(\forall x) \mbox{ and } (\exists x)$, whose scope does not contain $x$ free, prove that $\vdash B \leftrightarrow C$.

First I have a question about this problem: Does it mean that we remove all quantifiers from $B$? Because if there is a quantifier, it's scope either does not contain $x$, or it contains $x$ and then $x$ is not free, since it is in the scope of the quantifier. Hence, it's scope never contains $x$ free..

Now my approach to a solution, I first tried to make up a simple example. For instance, denote $B$ as $(\forall x)(\exists y) A(x,y)$. Then $C$ would become $A(x,y)$ and we need to prove that $\vdash B \leftrightarrow C$ (which we can prove by proving $\vdash B \implies C$ and $\vdash C\implies B$ seperately and using Biconditional Introduction.

Already here I am stuck. In the case of $\vdash B \implies C$, with the particularization rule, we can get rid of $\forall x$, but to get rid of $\exists y$, we need $x$ to be not free in $A(x,y)$, which it clearly is. In the case of $\vdash C\implies B$, we can add the $\exists y$ by using the existential rule, but if we want to use generalization on $x$ (which is not free in $C$) we cannot use the deduction theorem anymore to prove $\vdash C\implies B$.

I have the feeling that if I can prove this simple example, I can remove all quantifiers by using the replacement theorem: If $C$ is a subformula of $B$, $B'$ is the result of replacing zero or more occurences of $C$ in $B$ by a wf $D$, then if $\vdash C \leftrightarrow D$, then $\vdash B \leftrightarrow B'$. Is that correct?

• In a formula $\forall x \phi$ the scope of the leading quantifier $\forall x$ is $\phi$. – Mauro ALLEGRANZA Mar 6 '17 at 16:17
• The formal syntax licenses formulas $\forall x \phi$ with $x$ not occurring in $\phi$. Example: $\forall x (0=1)$ is formally correct. – Mauro ALLEGRANZA Mar 6 '17 at 16:17
• Thus, the problem ask to prove that e.g. $\forall x \phi \leftrightarrow \exists x \phi \leftrightarrow \phi$ if $x$ is not free in $\phi$. In simple words, to add a "dummy" quantifier (i.e. quantifying a variable that is not free) does not "change the meaning" of a formula. – Mauro ALLEGRANZA Mar 6 '17 at 16:19

A quantifier that quantifies a variable that otherwise does not occur in the scope of that quantifier is called a 'null' quantifier. For example, in $(\forall x) A(y)$, the quantifier is a null quantifier.

The exercise you have to do is to show that once you remove all (and only) the null quantifiers from $B$, the result $C$ is equivalent to $B$.

The way they phrase this: 'erase all quantifiers whose scope does not contain x free' is a little confusing, but what they mean is this:

Say you have the following statement:

$(\forall x)(\forall y)(A(y) \rightarrow (\exists x)(B(x)\land C(x,x)))$

The $x$'s in $B(x)$ and $C(x,x)$ are bound by the $(\exists x)$, and the $(\forall x)$ is in fact a null quantifier. So: even though the $B(x)$ and $C(x,x)$ occur in the scope of the $(\forall x)$, they do not become free once you remove the $(\forall x)$. Indeed, within the scope of $(\forall x)$ they are not free ... they are bound ... just not by the $(\forall x)$ itself. So that's what they mean by 'erase all quantifiers $(\forall x)$ and $(\exists x)$ whose scope does not contain x free'.

$B = (\forall x)(\exists y) A(x,y)$

the $x$ in $A(x,y)$ is not free, exactly because it is bound by the $(\forall x)$ before it. So, the $(\forall x)$ is not a null quantifier, and you therefore shouldn't remove it. The same goes for the $y$. Hence, the result of removing all null quantifiers from $B$ is $B$ itself!

Finally, a hint for proving what you need to prove: use structural induction on the syntactical formation of $B$. Use the Null quantification Equivalence laws:

$(\forall x) \phi \Leftrightarrow \phi$

$(\exists x) \phi \Leftrightarrow \phi$

for any variable $x$ and formula $\phi$ that does not contain $x$ as a free variable.

and indeed use the replacement theorem as you already suspected.

• But in example $B$, for quantifier $\forall x$, the scope is $A(x,y)$ and it does not contain $x$ free, since $x$ is bounded by its quantifier. But if we read the sentence: by erasing all quantifiers whose scope does not contain $x$ free, then we should remove the quantifier right? And you say we shouldn't, since it isn't a null quantifier (which seems logical to me).. – Sven Mar 6 '17 at 22:11
• @SvenCornetsdeGroot Yes, the question is certainly confusing phrased that way. But I am sure it really is meant as: remove all null quantifiers. Otherwise it doesn't make sense, as your example shows. – Bram28 Mar 6 '17 at 23:08
• @SvenCornetsdeGroot Oh, I see now why they phrased it the way they do ... let me add a little bit to the beginning of my answer to explain ... give me a few minutes ... – Bram28 Mar 6 '17 at 23:16
• @SvenCornetsdeGroot OK, I explained in my answer what they mean by that phrase. – Bram28 Mar 6 '17 at 23:25
• now it makes sense to me too! thank you! – Sven Mar 6 '17 at 23:41