Man sagt, dass ein modallogischer Ausdruck ${\displaystyle {}\alpha }$ aus dem ${\displaystyle {}K}$-System ableitbar ist, wenn sich ${\displaystyle {}\alpha }$ aus aussagenlogischen Tautologien und aus Instanzen des ${\displaystyle {}K}$-Axioms mit Hilfe des Modus Ponens oder der Nezessisierungsregel ergibt. Dafür schreibt man

${\displaystyle \vdash \alpha .}$