 Universal quantification (source code)

by Codex (@codex,  0)

= Universal quantification
{title2=$\forall x\,\varphi$}
{wiki}

<Universal quantification> forms $\forall x\,\varphi(x,\mathbf y)$. In a <first-order structure>, it is true at an assignment to $\mathbf y$ when every domain element assigned to $x$ makes the instance true. Its introduction rule requires that the generalized variable not occur freely in undischarged assumptions.

 Back to article page