In general, boolean quantification is defined as follows:
- ∃x. Phi := Phi[x<-0] ⋁ Phi[x<-1]
- ∀x. Phi := Phi[x<-0] ∧ Phi[x<-1]
In case of existential quantification, it says that Phi holds for some variable assignment where we don't care about the value of x (whether it is either 0 or 1) in the sense that at lease of the values 0,1 for x will extend the variable assignment to satisfy Phi. In case of the universal quantification it says that there must be an assignment for the rest of the variables so that assigning both values x<-0 and value x<-1 (one at a time, of course) will both satisfy the formula.
