= 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.
Over the <natural numbers>, reversing the preceding <existential quantification> and <universal quantification> gives a true <first-order sentence>:
$$
\forall n\in\mathbb N\,\exists m\in\mathbb N\;(m>n).
$$
Choose $m=n+1$. The computed witnesses for $n=0,1,2,3$ are $m=1,2,3,4$. The choice may depend on the previously given $n$. The formula states that every <natural number> has a larger <natural number>; the reversed formula demands one larger than all of them.
\Image[/quantifier-order-witnesses.png]
{title=<Universal quantification> followed by <existential quantification> permits a different witness for each input}
The diagram displays a finite window, while the rules $m=n+1$ and $n=m$ settle the two statements for every <natural number>. This dependence is why quantifier order matters in precise specifications. Choosing one $m$ that works for every $n$ would also provide a witness for each $n$; the reverse inference fails here.
To introduce <universal quantification> in <natural deduction>, reason with an arbitrary input, without assuming a special property of it. The construction $m=n+1$ does exactly this and also gives a proof in <intuitionistic first-order logic>. The introduction and elimination rules for both quantifiers are developed in https://www.cs.cmu.edu/~fp/courses/15317-f08/lectures/06-quant.pdf[Frank Pfenning, First-Order Logic and Type Theory, section 4.1].
Back to article page
