Generalisation

Generalisation

Suppose $\phi$ is a formula of $\mathcal{L}$, then from $\phi$ infer $\forall v\phi$

Remark

A consequence of the Generalisation Rule is that we can put universal quantifiers in front of the propositional and identity axioms. This accords with how we should think of free variables in the axioms — the axioms should hold in any structure independently of how the free variables are interpreted. It also accords with standard mathematical practice: if we can prove a result $\phi (v)$ about a variable $v$ without any particular assumptions on $v$, we can deduce $\forall v\phi (v)$.