There is an exercise in Mendelson's Introduction to Mathematical Logic, 6th edition:
If $\mathscr C$ is obtained from $\mathscr B$ by erasing all quantifiers $(\forall x)$ or $(\exists x)$ whose scope does not contain $x$ free, prove that $\vdash \mathscr B \longleftrightarrow \mathscr C$.
I have searched the site for similar questions, and I stumped upon this: Proving a biconditional relation between wfs $B$ and $C$, where $C$ is obtained by erasing all quantifiers from $B$
The asker supposed that he will use the Replacement Theorem for his final conclusion, and the answerer agrees with him. Supposing that it is absolutely necessary for proving this theorem, why my proof attempt would be incorrect?
My proof attempt:
We suppose that it holds for $r<q$ number of quantifiers. Clearly, $\vdash A \leftrightarrow A$, so the base case holds. If $\mathscr B$ is $(\forall x) \mathscr E$, then, by rule A4, $\vdash \mathscr B \rightarrow \mathscr E$. Since $x$ is not free in $\mathscr E$, by $\vdash \mathscr E \rightarrow \mathscr E$, Gen, A5 and MP, we have $\vdash \mathscr E \rightarrow \mathscr B$. Now, by biconditional introduction, $\vdash \mathscr B \longleftrightarrow \mathscr E$. If $\mathscr B$ is $(\exists x) \mathscr E$, then, by rule E4, $\vdash \mathscr E \rightarrow \mathscr B$. Since $x$ is not free in $\mathscr E$, by Ex. 2.32 (b) we have $\vdash \mathscr B \rightarrow \mathscr E$. Again, $\vdash \mathscr B \longleftrightarrow \mathscr E$. In both cases, by inductive hypothesis, we can erase null quantifiers in $\mathscr E$ to obtain $\mathscr C$ and have $\vdash \mathscr E \longleftrightarrow \mathscr C$, so $\vdash \mathscr B \longleftrightarrow \mathscr C$
Clarification on used abbreviations:
- A4: rule to eliminate universal quantifier.
- E4: rule to introduce existential quantifier.
- A5: axiom $(\forall x)(\mathscr B \rightarrow \mathscr C) \rightarrow (\mathscr B \rightarrow (\forall x) \mathscr C)$, if $x$ is not free in $\mathscr B$.
- Ex. 2.32 (b): $\vdash (\exists x) \mathscr B \rightarrow \mathscr B$, if $x$ is not free in $\mathscr B$.