Logique intuitionniste - Définition

Interprétation de la logique intuitionniste

Approche intuitive

La logique intutionniste peut être vue comme une logique modale, munie de la modalité de nécessité, notée où l'implication intuitionniste est , quand est l'implication classique. Cela peut se lire nécessairement p implique q. L'idée des modèles de Kripke est de créer une hiérarchie qui donne de plus en plus de « nécessité» aux implications. Comme cela ne concerne que l'implication intuitionniste, il n'y a qu'elle qui sera concernée par cette hiérarchie.

La sémantique de la logique intuitionniste est fondée sur les modèles de Kripke. Ces modèles sont eux-mêmes fondés sur des mondes dans lesquels opèrent la sémantique classique (en 0 et 1 pour le calcul des propositions). Ces mondes peuvent être vus comme des contenus d'information de plus en plus riches. Ils sont donc hiérachisés par une relation d'ordre (la relation d'accessibilité). Si une proposition est « satisfaite » dans un monde, on dit que ce monde force la proposition. Un monde force une proposition , si tous les mondes qui le dominent hiérarchiquement forcent . Comme la nécessité ne va être appliquée qu'à l'implication, nous dirons qu'un monde force si pour tous les mondes m qui le dominent hiérarchiquement, on a m force ψ dès que m force .

On dira qu'un modèle de Kripke satisfait ou modèlise une proposition si tous les mondes qu'il contient forcent cette proposition.

Une proposition est valide, si elle est satisfaite par tous les modèles.

On peut montrer que la logique intuitionniste est correcte pour les modèles de Kripke, c'est-à-dire que toute proposition prouvable en logique intuitionniste est valide dans les modèles de Kripke.

Or on peut montrer que les propositions suivantes ne sont pas valides pour les modèles de Kripke:

• ,

• (loi de Peirce).

On en conclut que ces deux propositions, qui sont pourtant des tautologies classiques, ne sont pas prouvables en logique intuitionniste.

On montre que les modèles de Kripke sont complets pour la logique intuitionniste, c'est-à-dire que toute proposition valide est prouvable.

Approche formelle

Dans cet article nous ne considèrons que les modèles de la logique propositionnelle qui forment un exemple de sémantique de Kripke.

Un modèle est formé d'un triplet .

• est appelé l'univers et ses éléments notés m sont appelés des mondes,

• < est une relation d'ordre ,

Un cône est un ensemble C de mondes ( ) tels que et m < m' impliquent .

est une initialisation; c'est une application qui associe à chaque variable propositionnelle un cône de .

On définit une relation de réalisabilité ou de forçage entre un monde m et une proposition , que l'on écrit et que l'on lit m force . La relation de forçage est définie par induction sur la structure des formules.

• si φ est une variable x, alors si ,
• si φ est une proposition alors , si pour tout monde m' tel que on a si alors .

On peut démontrer (par induction sur la structure ou la taille de ) que pour chaque proposition , l'ensemble des m tels que est un cône.

On dit que est valide dans ou que modélise , noté , si pour , on a . On dit que est valide, si pour tout modèle , .

Correction de la logique intuitionniste

On peut montrer que la logique intuitionniste est correcte vis-à-vis des modèles de Kripke, c'est-à-dire que toute proposition démontrable est valide.

Formellement, implique .

On peut utiliser ce résultat pour montrer qu'une proposition n'est pas démontrable en logique intuitionniste. Si on considère le modèle avec m₀ < m₁ et et , on peut montrer que , donc et donc que . La loi de Peirce n'est pas valide vis-à-vis des modèles de Kripke, donc elle n'est pas démontrable en logique intuitionniste.

On peut aussi trouver un contre-modèle très simple de la proposition .

Complétude de la logique intuitionniste

On peut démontrer que toute proposition valide est démontrable.

Formellement, implique .

La démonstration se fait de la façon suivante: si n'est pas démontrable alors on peut construire un contre-modèle (infini) de c'est-à-dire un modèle tel que .