Wir sehen, dass sich die Aussagenlogik oder die Prädikatenlogik mit der Darstellung dynamischer Sachverhalte schwer tun. Das führt zur Definition modaler Logiken. Überlegungen zur Syntax werden begleitet von Überlegungen zur semantischen Modellierung, einmal durch Kripke-Modelle, dann durch Nachbarschaftsmodelle. Morphismen diesen zum Vergleich von Modellen, und Bisimulationen zeigen, wie ein Modell ein anderes simulieren kann. Der Zusammenhang von Gültigkeit und Beweisbarkeit wird studiert; hierzu konstruieren wir zunächst ein kanonisches Modell und gehen der Frage nach Vollständigkeit und Korrektheit nach. Wir beobachten, dass manche Formeln ganze Familien von Kripke-Modellen definieren und untersuchen Vollständigkeit und Korrektheit in diesem eingeschränkten Zusammenhang. Schließlich stellen wir die Semantik der Spiele-Logik durch Nachbarschaftsmodelle dar.