# Understanding kQBF: changing order of quantification?

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:

1. 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)$?
2. 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:

1. There exists a village such that all villagers have shovels. Here we have two alternations ($\exists X~\forall Y~\exists Z$).
2. 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.

## 1 Answer

$\exists x\forall y \hspace{1mm}\varphi$ is not equivalent to $\forall y \exists x \hspace{1mm} \varphi$.

Consider for example the formula "for all $x$ there exists $y$ such that $y=x^2$". When evaluated over the reals, this is true (every real number has a square). However, if you switch the quantifiers you get the statement "there exists $y$ such that for all $x$ it holds that $y=x^2$". Note that this has an entirely different meaning, since now the statement reads "there exists a real number which is the square of all real numbers", and this is obviously false.

The order of quantifiers is important, so you can't trivially reduce $kQBF$ to $(k-1)QBF$.

• First formula says: "for all $x$ there exists $y$ such that $y=x^2$". Second says: "there exists $y$ for all $x$ such that $y=x^2$". Read carefully. What have you made think that they are unequal is that novices oftenly think that $\forall x~\exists y:\varphi(x,y)\Leftrightarrow\exists x~\forall y:\varphi(x,y)$. Also I don't think that this formula is in propositional logic: arithmetic hierarchy does not collapse = we can't move (in general) quantifiers in 1st order logic and higher. – rus9384 Aug 24 '17 at 23:43
• This (what you referred to as the "novices" confusion) is exactly what you asked in question one. I can't parse your second statement. – Ariel Aug 24 '17 at 23:52
• No, I have only moved order of assigning variables, not flipping quantifiers for corresponding variable. So, I yet can't understand why order is important. Assume $\varphi = (x\lor y\lor z)\land(\overline x\lor\overline y\lor\overline z)$ we have $\forall x~\exists y~\forall z:\varphi(x,y,z) = \forall x~\forall z~\exists y:\varphi$. And I can't understand what's wrong. – rus9384 Aug 24 '17 at 23:59
• Ah, well, simple example $x = y$ over binaries already gives an answer. – rus9384 Aug 25 '17 at 23:20