In formal logic, a quantifier that ranges over propositions and binds atomic variables. For example, $\forall p\left(p\to p\right)$ is read as ‘for all propositions $p$, $p\to p$ is true’.