# Negating a Quantified Boolean Formula (QBF)

You should also verify that the negation of the formula $$Q_1x_1\cdot\cdot\cdot Q_nx_n \phi(x_1, ..., x_n)$$ is the same as $$Q^{\prime}_1x_1\cdot\cdot\cdot Q_n^{\prime}x_n \neg\phi(x_1, ..., x_n)$$, where $$Q^{\prime}_i$$ is $$\exists$$ if $$Q_i$$ is $$\forall$$ and vice-versa.

I know the identity $$\neg\forall\phi(x) = \exists x\neg\phi(x)$$. Also, it seems like $$\neg$$ is, in some cases, distributive.

However, I haven't had any luck in using those two things to verify that statement.

Any idea?

Thanks!

You're right in that the identity you need is essentially $$\neg \forall X. \phi = \exists X. \neg \phi$$ and (symmetrically) $$\neg \exists X. \phi = \forall X. \neg \phi$$.

One can proceed via proof by induction.

Base case: It is obvious that $$\neg Q_1 x_1. \phi(x_1)= Q_1' x_1. \neg \phi(x_1)$$ via the properties above.

Inductive case: Assume the statement is true for $$n-1$$, i.e. $$Q_1 x_1. Q_2 x_2., ..., Q_{n-1} x_{n-1}. \phi(x_1,...,x_{n-1}) = Q'_1 x_1... Q'_{n-1} x_{n-1}. \neg\phi(x_1,...,x_{n-1})$$. Then

$$Q_1 x_1,..., Q_n x_n. \phi_n (x_1,...,x_n)= Q_1x_1,...,Q_{n-1}x_{n-1} (Q_n x_n.\phi(x_1,...,x_n)) \\ = Q'_1 x_1...Q'_{n-1}x_{n-1}.\neg(Q_nx_n.\phi(x_1,...,x_n)) \text{ by ind.hyp.} \\ = Q'_1 x_1,...,Q'_nx_n.\neg\phi(x_1,...,x_n)\text{ by negation properties above.}$$

• The reasoning is OK, however you are missing negations before the original quantifiers: $\lnot Q \phi = Q' \lnot \phi$. Also, the base case can even be where $n=0$, so without quantifiers. (The inductive case also works for $n=1$.) Commented May 31 at 21:44
• @HendrikJan I corrected the typo in the base case. Thanks for pointing it out. Commented Jun 2 at 1:15
• Sorry that I was not really explicit, but also the inductive case at the start needs a negation before the sequence of original quantifiers. Commented Jun 2 at 12:08