Theory of proveit.logic.booleans.quantification.existence¶
Existential quantification is a general expression about something (Exists: $\exists$).
The Exists Expression derives from OperationOverInstances. As such, it has 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 $\exists_{x, y \in S~|~Q(x, y),~R(y)} P(x, y)$ means that $P(x, y)$ is TRUE for some occurrence of $x$ and $y$ in domain $S$ for which the conditions $Q(x, y)$ and $R(y)$ are satisfied. The conditions may be any Expressions involving the instance variables.
The negation of the existential quantification is compactly expressed as $\nexists$, represented by the NotExists Expression type.
In [1]:
import proveit
%theory
