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
