In classical logic we tend to make the assumption the domain of quantification is non-empty. This isn't (too) problematic because classical mathematicians assume a language/mind/proof independent ...
Rule modus ponens: $ p, p \to q \vdash q $ Axioms A1 $ p \to (q \to p) $ A2 $ (p \to (q \to r)) \to ((p \to q) \to (p \to r)) $ A3 $ (p \land q) \to p $ A4 $ (p \land q) \to q $ A5 $ p \to ...
Prove that: Two finite rooted frames are isomorphic iff they validate the same formulas. (This is an exercise in the book "Modal Logic" by A.Chagrov and M.Zakharyaschev)