logo

Context: proveit.logic.boolean.quantification

Logical quantification is a general expression about everything (Forall: $\forall$), something (Exists: $\exists$), or nothing (NotExists: $\nexists$). These quantify over instance variables (instanceVars) with an instance expression (instanceExpr) 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.

In [1]:
import proveit
%context