I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e ..." lines denoting which variables are to be existentially quantified and which variables are to be universally quantified.
For instance, a simple QDIMACS input such as:
p cnf 2 3
a 1 0
e 2 0
1 2 0
-1 0
-2 0
...would be correspond to the formula $\forall x \exists y \ (x \lor y) \land \neg x \land \neg y$ where $x$ and $y$ range over $\{T, F\}$. SAT is an instance of QBF where all the variables are existential.
The above is an example of 2QBF, where we have two layers of quantifiers. A more complex QDIMACS problem with alternating quantifiers might be:
p cnf 2316 15282
e 1 17 2 18 3 19 4 ... 0
a 1598 1599 1600 1601 1602 1603 0
e 65 81 66 82 67 83 68 ... 0
a 1610 1611 1612 1613 1614 1615 0
e 193 209 194 210 195 211 196 ... 0
a 1616 1617 1618 1619 1620 1621 0
-2 -18 0
-3 -19 0
-4 -20 0
-5 -21 0
-6 -22 0
-7 -23 0
...
Anyways, on to my question. I don't understand why 2QBF != QBF. It seems to me for any formula $F$ and variables $x$, $y$ ranging over the booleans that $\forall x \exists y \ F$ is equivalent to $\exists y \forall x \ F$.
To demonstrate my thinking, I will consider the Shannon expansion of the universal quantifier.
\begin{align} \forall x \exists y \ F \iff& (\exists y \ F[x \to T]) \land (\exists y \ F[x \to F]) \\\\ \exists y \forall x \ F \iff& \exists y \ (F[x \to T] \land F[x \to F]) \end{align}
Suppose $\exists y \ (F[x \to T] \land F[x \to F])$ is satisfiable. Then the same assignment would extend to both $\exists y \ F[x \to T]$ and $\exists y \ F[x \to F]$.
Suppose $\exists y \ (F[x \to T] \land F[x \to F])$ is unsatisfiable. Then at least one of $\exists y \ F[x \to T]$ or $\exists y \ F[x \to F]$ is also unsatisfiable.
Thus $\forall x \exists y \ F \iff \forall y \exists x \ F$.
A similar question has been asked before here, but there appears to be ambiguity over the domain of the quantifiers. They should range only over true or false and not over other mathematical objects or propositional variables. This is in correspondence to the standard interpretation of the SAT problem.
For instance, $\forall x \exists y \ x \leftrightarrow y$ would not be true since setting $y$ to $x$ is not valid.
Is my interpretation of QBF correct? Is there a counterexample I'm missing?