Le calcul des propositions dit ce qui est vrai. La logique modale lui ajoute deux opérateurs pour nuancer : la boîte $\Box$, « nécessairement », et le diamant $\Diamond$, « possiblement ».
Pour leur donner un sens, on ne raisonne plus dans un seul monde mais dans un graphe de mondes possibles : $\Box P$ est vraie ici si $P$ est vraie dans tous les mondes accessibles depuis ici, $\Diamond P$ si elle l’est dans au moins un. Selon ce qu’on fait dire à la boîte (c’est nécessaire, c’est obligatoire, je le sais, ce sera toujours vrai, c’est démontrable), la même machinerie modélise la nécessité, le devoir, la connaissance, le temps ou la prouvabilité.