Universal quantification ($\forall x\phi$)

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.

A universal formula has a block of universal quantifiers followed by a quantifier-free formula. Empty blocks are usually permitted. Truth transfers from a first-order structure to a substructure of a first-order structure for parameters in that substructure: every tuple in the smaller domain is available in the larger domain, and quantifier-free truth is preserved and reflected by the inclusion. This is the dual preservation direction to the forward preservation of an existential formula under a structure embedding.