 A formula \(\varphi\) is globally true in a model \(\mathcal{A}\) if it is satisfied at all worlds in \(\mathcal{A}\) (\(\mathcal{A}\models \varphi\)). A formula \(\varphi\) is valid if it is globally true at all models (\(\models \varphi\)). The set of validities in the whole class of Kripke models (when no restrictions are imposed to the accessibility relation) are the validities of the basic modal logic, also called minimal modal logic or System K.[12]