Zweig der Logik, der mit Hilfe logischer Kalküle die Grundmodalitäten „möglich, notwendig, unmöglich, nicht notwendig“ und durch deren Zusammensetzung entstehende kompliziertere Modalitäten untersucht und präzisiert, und dabei Beziehungen zu den klassischen Aussageverknüpfungen „nicht, und, oder, wenn–so, genau dann–wenn“ (evtl. auch zu den Quantoren „es gibt ein, für jedes“) herstellt.

Zu den Grundzeichen des Aussagen- bzw. des Prädikatenkalküls kommen die beiden weiteren Funktoren ⋄ und □ für die Modalitäten „möglich“ und „notwendig“ hinzu.

Beispiele für Axiome im Rahmen der Modallogik sind:

□φ ↔ ¬⋄¬φ (φ ist notwendig ⇔ es ist nicht möglich, daß φ nicht gilt).

⋄φ ↔ ¬□¬φ (φ ist möglich ⇔ es ist nicht notwendig, daß φ nicht gilt).