Theory of proveit.logic.booleans.quantification¶
Logical quantification is a general expression about everything (Forall: $\forall$), something (Exists: $\exists$), or nothing (NotExists: $\nexists$). These quantify over instance variables (instance_vars) with an instance expression (instance_expr) and may be restricted to a domain and have zero or more conditions. For example $\forall_{x \in S~|~Q(x)} P(x)$ means that $P(x)$ is TRUE for all occurrences of $x$ in domain $S$ given that the condition $Q(x)$ is satisfied. $\exists_{x \in S~|~Q(x)} P(x)$ means that there exists a value for $x$ in domain $S$ with $Q(x)$ satisfied such that $P(x)$ is TRUE. $\forall$ is the universal quantifier. $\exists$ is the existential quantifier. $\nexists$ is the negation of the existential quantifier.
