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?

  • $\begingroup$ In a formula $\forall x \phi$ the scope of the leading quantifier $\forall x$ is $\phi$. $\endgroup$ – Mauro ALLEGRANZA Mar 6 '17 at 16:17
  • $\begingroup$ The formal syntax licenses formulas $\forall x \phi$ with $x$ not occurring in $\phi$. Example: $\forall x (0=1)$ is formally correct. $\endgroup$ – Mauro ALLEGRANZA Mar 6 '17 at 16:17
  • $\begingroup$ 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. $\endgroup$ – 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'.

In your example:

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

  • $\begingroup$ 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).. $\endgroup$ – Sven Mar 6 '17 at 22:11
  • $\begingroup$ @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. $\endgroup$ – Bram28 Mar 6 '17 at 23:08
  • 1
    $\begingroup$ @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 ... $\endgroup$ – Bram28 Mar 6 '17 at 23:16
  • $\begingroup$ @SvenCornetsdeGroot OK, I explained in my answer what they mean by that phrase. $\endgroup$ – Bram28 Mar 6 '17 at 23:25
  • $\begingroup$ now it makes sense to me too! thank you! $\endgroup$ – Sven Mar 6 '17 at 23:41

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.