 The treatment of quantifiers in models for substructural logics has proved to be quite difficult, but advances have been made in the early 2000s. The difficulty came in what seemed to be a mismatch between the proof theory and model theory for quantifiers. Appropriate axioms or rules for the quantifiers are relatively straightforward. The universal quantifier elimination axiom \[ \forall xA \rightarrow A[t/x] \] states that an instance follows (in the relevant sense) from its universal generalisation. The introduction rule \[ \cfrac{\vdash A\rightarrow B} {\vdash A\rightarrow \forall xB} \] (where the proviso that \(x\) is not free in \(A\) holds) tells us that if we can prove an instance of the generalisation \(\forall xB\), as a matter of logic, from some assumption which makes no particular claim about that instance, we can also prove the generalisation from that assumption. This axiom and rule seems to fit nicely with any interpretation of the first-order quantifiers in a range of substructural logics, from the weakest systems, to strong systems like \(\mathbf{R}\). 