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