2QBF is a problem of determining whether formula $\exists X~\forall Y:\varphi(X,Y)$ is valid. $X$ and $Y$ here are sets of variables. Next, 3QBF asks if formula $\exists X~\forall Y~\exists Z:\varphi(X,Y,Z)$ is valid. But what I can't understand is following:
- Can't we change order of quantification? E.g. isn't following true $\exists X~\forall Y:\varphi(X,Y) = \forall Y~\exists X:\varphi(X,Y)$?
- If we can, what prevents us from doing this in the second case and reducing 3QBF to 2QBF? E.g. $\exists X~\forall Y~\exists Z:\varphi(X,Y,Z) = \exists \{X, Z\}~\forall Y:\varphi(X,Y,Z)$.
The main idea is to reduce the number of alternations to one.
What I thought:
Let we have a formula $\forall x_1~\exists y_1...\forall x_k~\exists y_k:\varphi(x_1,y_1...x_k,y_k)$. Then we can construct a truth-table (theoretically) where columns will be sorted this way:
x_1 x_2 ... x_k y_1 ... y_k ф
0 0 ... 0 0 ... 0 _
0 0 ... 0 0 ... 1 _
. . ... . . ... . .
. . ... . . ... . .
1 1 ... 1 1 ... 1 _
Then we can divide table (no row/column moving) in $2^k$ parts each containing $2^k$ rows. If each of that part has satisfiying assignment, formula is valid. But that means that there is no difference at all in which order we should assign variables, since truth-table of formula is independent on the quantifiers.
In other words following must be true: $\forall x_1~\exists y_1...\forall x_k~\exists y_k:\varphi(x_1,y_1...x_k,y_k) = \forall x_1~\forall x_2...\forall x_k~\exists y_1...\exists y_k:\varphi(x_1,y_1...x_k,y_k)$
It seems that we can change order of quantification in first order logic. Compare following sentences:
- There exists a village such that all villagers have shovels. Here we have two alternations ($\exists X~\forall Y~\exists Z$).
- Every villager has a shovel in some village. This is logically equivalent, but has only one alternation ($\forall Y~\exists Z~\exists X$).
There are 4 another ways to move quantifiers and all of them will produce equal statements. Yet I do not have any reasons to think we can't change order of quantification in logic.
Ability to change order of quantification $\Leftrightarrow \mathsf{NP = PSPACE}$. This problem is open for decades and logic rules I used are not something really new. So, this is strange... like I am missing something.