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.

In [1]:

```
import proveit
%theory
```