Les logiques modales considèrent les propositions non seulement comme vraies ou fausses, mais encore comme nécessaires, contingentes, possibles, impossibles (modalités aléthiques). D’autres systèmes prennent en considération des modalités comme « il faut que », « il est permis de » (modalités déontiques).

Conditions initiales

En tant que système formel, une logique modale introduira un certain nombre de signes qu’il s’agira ensuite d’interpréter. Pour qu’une telle interprétation rende compte de certains aspects des notions intuitives de nécessité, de possibilité, etc., il convient tout d’abord d’expliciter ces dernières.

Ajoutons aux symboles de la logique classique (v. calcul des propositions) les deux opérateurs suivants : □, qui sera interprété comme l’opérateur de nécessité, de sorte que □p s’interprétera par « p est nécessaire », et ⃟, qui sera interprété comme l’opérateur de possibilité et permettra d’interpréter ⃟p par « p est possible ». Il est alors naturel de requérir au moins les conditions suivantes :
(1) ⊢ □p ⊃ p, si une proposition est nécessaire, elle est vraie.
(2) ⊢ p ⊃ ⃟p, si une proposition est vraie, elle est possible.
(3) Les réciproques de (1) et (2) ne doivent pas être valides. En effet, admettre, par exemple, que p ⊃ □p, reviendrait à poser l’équivalence entre p et □p et donc à supprimer toute distinction entre vrai et nécessaire.
(4) En revanche, l’idée de nécessité est généralement liée à celle de loi logique.
On posera donc que si P est un théorème logique, P est une proposition nécessaire : si ⊢ P, alors ⊢ □P. On notera qu’il s’agit d’une règle (la future règle N) et non d’une formule des calculs.
(5) ⊢ □p ≡ ~ ⃟ ~ p, dire que p est nécessaire équivaut à dire que non-p est impossible.
(6) ⊢ ⃟p ≡ ~ □ ~ p, dire que p est possible équivaut à dire que non-p n’est pas nécessaire.
(7) Enfin, la plupart des systèmes modaux se construisent comme une extension de la logique bivalente classique. Cela signifie que tout théorème de la logique des propositions vraies/fausses est aussi un théorème de la logique modale, sans que naturellement [v. (3)] la réciproque soit vraie.

Il est possible de satisfaire aux sept conditions ci-dessus de multiples façons. Nous allons en envisager quelques-unes en partant d’un système appelé t, dû à Feys (1937) et reconstruit autrement par von Wright (1951) sous le nom de système m.

Le système T

La condition (7) ci-dessus permet de considérer t comme une extension du calcul des propositions. Donnons-nous donc ce qui suit :

Symboles primitifs

Variables de propositions : p, q, m, ...,

Opérateurs unaires : ~, □ ;

Opérateur binaire : ⊃.

Nous introduirons des parenthèses en les utilisant de manière intuitive.

Expressions bien formées (ebf)

Il suffit d’ajouter, aux clauses inductives du calcul des propositions, la clause :

(2′) Si P est une ebf, □ P est une ebf.

Cela signifie que ~ p, □ ~ p, □ (p ⊃ q), par exemple, sont des ebf.

Définitions abréviatives

Outre celles de ⋀, ⋁ et ≡, nous poserons :

⃟ P = df ~ □ ~ P, conformément à la condition (6), et P ≺ Q = df □ (P ⊃ Q).

Le signe ≺ est celui de la conditionnelle stricte. Il signifie que l’on a non seulement « si P alors Q », mais « nécessairement : si P alors Q ».

Axiomes

Un système d’axiomes pour le calcul des propositions est par exemple :
a₁ p ⊃ (q ⊃ p) ;
a₂ (p ⊃ (q ⊃ m)) ⊃ ((p ⊃ q) ⊃ (p ⊃ m)) ;
a₃ (~ p ⊃ ~ q) ⊃ (q ⊃ p) ;
auquel on adjoindra les deux axiomes suivants :
a₄ □ p ⊃ p, conformément à la condition (1) ;
a₅ □ (p ⊃ q) ⊃ (□ p ⊃ □ q).
L’axiome a₅ pourrait aussi s’écrire (p ≺ q) ⊃ (□ p ⊃ □ q).
Il signifie que, en présence de la conditionnelle stricte entre p et q, si p est nécessaire, q l’est aussi.

Règles de déduction

• Règle de substitution. Dans un théorème, la substitution d’une ebf à chaque mention d’une variable de proposition fournit un théorème.

• Règle du « modus ponens ». Si P et P ⊃ Q sont des théorèmes, Q est un théorème.

• Règle de la nécessité N. Si P est un théorème, □ P est un théorème.

Les deux premières règles appartiennent au calcul classique des propositions, la troisième, proprement modale, correspond à la condition (4).

Les théorèmes de t seront toutes les ebf déductibles des axiomes par ces trois règles.

Exemple. ⊢ p ⊃ ⃟ p

Il existe une analogie formelle entre les propriétés de □ et ⃟ d’une part et celles de ∀ et ∃ de l’autre (v. calcul des prédicats). Ainsi a-t-on par exemple dans t :

On a de même :

Ces lois montrent bien que la nécessité dont il est ici question est de nature logique. Ce serait un autre problème que de chercher à rendre compte de la nécessité que l’on attribue parfois aux lois de la nature ou de celle dont on fait usage dans des formules comme « il faut que je m’en aille ».