Theory of proveit.logic.booleans.quantification.universality¶
Universal quantification is a general expression about everything (Forall: $\forall$).
The Forall Expression derives from proveit.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 $\forall_{x, y \in S~|~Q(x),~R(x, y)} P(x, y)$ means that $P(x, y)$ is TRUE for all occurrences of $x$ and $y$ in domain $S$ given that the conditions $Q(x)$ and $R(x, y)$ are satisfied. The conditions may be any Expressions involving the instance variables.
In [1]:
import proveit
%theory
