Universal quantification ($\forall$)

Universal quantification forms $\forall x\phi (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: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.

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 Frank Pfenning, First-Order Logic and Type Theory, section 4.1.