# Boolean quantification

Hello

Please may explain in simple word what is the idea for existential quantification? I studied on lecture video and also tried to find on previous exam but i am not sure what I understood is the right one.

My understanding is: "based on given variables e, we must try to see either in left or right branch of ϕ, after passing variables e, being true". Kindly elaborate on it? Thank you.

edited

Formally, exists x. phi is defined as the disjunction of the co-factors, i.e., phi[x<-0] | phi[x<-1]. In simply words, we ask whether there is a value for x such that phi becomes true. Since there are only values 0 and 1 for x, this is the disjunction phi[x<-0] | phi[x<-1]. Hence, we need to find a variable assignment that satisfies phi[x<-0] or phi[x<-1], so that the models of exists x.phi are the models of phi where we just omit the assignment to x.

In contrast, forall x. phi is defined as the conjunction of the co-factors, i.e., phi[x<-0] & phi[x<-1]. Hence, we ask whether phi can become true for all values of x, i.e., we need to find a variable assignment that satisfies both phi[x<-0] and phi[x<-1]. Thus, we take the intersection of models of phi[x<-0] and phi[x<-1] as the models of forall x. phi.

Examples:

• exists x. x = true
• exists x. !x = true
• exists x. x&y = y
• exists x. x|y = true
• exists x. x->y = true
• exists x. x<->y = true
Feel free to make more examples using https://es.cs.uni-kl.de/tools/teaching/BDDAlgorithms.html with the Exists and Forall algorithm on the BDDs.
by (91.8k points)