A possible-worlds semantics is defined that validates the main axioms of Kripke's original system for first-order modal logic over varying-domain structures. The novelty of this semantics is that it does not validate the commutative quantification schema ∀ x ∀ y φ→∀ y ∀ x φ, as we show by constructing a counter-model.