logo

Context: proveit.logic.boolean.quantification.existential

Existential quantification is a general expression about something (Exists: $\exists$).
The Exists Expression derives from proveit._generic_.operation_over_instances.OperationOverInstances. As such, it has instance variables (instanceVars) with an instance expression (instanceExpr) 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
%context