\begin{frame}
  \frametitle{Modal Validity}

  Modal validity is semantic implication with zero premises.
  
  \begin{goal}{Modal validity: \;\;$\models \; \psi $\;\; as}
    In every world $w$ in every Kripke model $\mathcal{M}$ holds $\mathcal{M},w \models \psi$.
  \end{goal}
  \smallskip
  \pause
  
  \begin{exampleblock}{}
    \begin{malign}
      &\mpause[1]{\models\; \all (\phi \to\psi)\to(\all \phi \to\all\psi) } \\
      &\mpause{\models\; \neg \all \phi   \to  \some\neg \phi } \\ 
      &\mpause{\models\; \all \phi  \vee \neg \all \phi }
    \end{malign}
  \end{exampleblock}
\end{frame}