Logique intuitionniste

L'intuitionnisme est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une alternative à l'approche dite classique. Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et A.Heyting. Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la Logique. Gerhard Gentzen en a formalisé les règles de déduction dans le cadre de la déduction naturelle.

Les travaux récents, notamment la correspondance de Curry-Howard, lui ont donné un statut central dans la logique et dans l'informatique, en en faisant historiquement la première des logiques constructives. L'étude de la logique intuitionniste est la clé pour bien comprendre la logique classique et ses subtilités.

Approche informelle

Brouwer a fondé l'intuitionnisme comme une position philosophique vis-à-vis des mathématiques ; cela l'a conduit à rejeter certaines formes du raisonnement mathématique traditionnel, qu'il jugeait contrintuitives. En fait, il refusait deux concepts.

• Le tiers exclu, qui consiste à dire qu'étant donnée une proposition $\backslash phi$, soit on a $\backslash phi$, soit on a $non(\backslash phi)$, formellement $\backslash varphi\; \backslash vee\; \backslash neg\backslash varphi$. A titre d'exemple, il rejetait la démonstration suivante de la proposition : «Il existe des nombres irrationnelss $a$ et $b$, tels que $a^b$ est un nombre rationnel» :

«Posons $b\; =\; \backslash sqrt\{2\}$, et maintenant si $\backslash sqrt\{2\}^\{\backslash sqrt2\}$ est rationnel prenons $a\; =\; \backslash sqrt\{2\}$, sinon prenons $a=\; \backslash sqrt\{2\}^\{\backslash sqrt2\}$ et nous avons $a^b\; =\; (\backslash sqrt\{2\}^\{\backslash sqrt2\})^\{\backslash sqrt2\}\; =\; \backslash sqrt\{2\}^\{\backslash sqrt\{2\}\backslash times\backslash sqrt\{2\}\}\; =\; \backslash sqrt\{2\}^2\; =2$ qui donne le résultat puisque $2$ est évidemment rationnel». La critique de cette démonstration est qu'elle utilise le tiers exclu et qu'elle ne dit pas quel $a$ fait marcher les choses. En fait, un théorème d'analyse affirme que $\backslash sqrt\{2\}^\{\backslash sqrt2\}$ est irrationnel et que c'est le $a$ qu'il faut choisir, mais la démonstration fondée sur le tiers exclu ne le dit pas.

• L'existentiel non constructif. Brouwer veut que quand un mathématicien affirme il existe $x$ tel que $x$ est $P$, que l'on écrirait formellement $(\backslash exists\; x)~P(x)$, il donne aussi un moyen de construire $x$ qui satisfait $P$.

Brouwer a donc prôné une mathématique qui rejetterait le tiers exclu et n'accepterait que l'existentiel constructif. Cette attitude a été assez violemment critiquée par des mathématiciens comme David Hilbert tandis que d'autres comme Hermann Weyl y ont souscrit. Une fois formalisée, trois faits font de la logique intuitionniste une logique à part entière : l'existence de modèles qui font d'elle un système complet de déduction, la découverte de son contenu calculatoire, connu sous le nom de correspondance de Curry-Howard, enfin le fait qu'elle est une logique modale. La logique intuitionniste n'a donc rien d'exotique. Allant plus loin, le logicien Jean-Yves Girard a proposé une logique plus faible que la logique intuitionniste, qu'il a appelée la logique linéaire, qui se trouve à la base de toute logique et qui permet de mieux comprendre la logique intuitionniste en particulier.

La logique intuitionniste revisite aussi le concept d'implication. L'implication $a\; \backslash Rightarrow\; b$ n'est plus l'implication matérielle $\backslash neg\; a\; \backslash vee\; b$. Quand un mathématicien intuitionniste affirme $a\; \backslash Rightarrow\; b$, il veut dire qu'il fournit un procédé de «construction» d'une démonstration de $\backslash \; b$ à partir d'une démonstration de $\backslash \; a$. Ceci est d'ailleurs la clé du contenu calculatoire de la logique intuitionniste.

Approche formelle

Nous venons de voir que l'implication et la disjonction ne sont plus liées. Mais en fait cela va plus loin: une des caractéristiques de la logique intuitionniste est le fait que chaque connecteur ($\backslash vee,\; \backslash wedge,\; \backslash bot$) et chaque quantificateur ($\backslash forall,\; \backslash exists$) doit être défini à partir de ses propres règles, autrement dit il n'y a pas de moyen de ramener la logique à un connecteur et à un quantificateur. C'est pourquoi nous allons donner des règles pour chaque connecteur.

La logique implicative minimale

Pour introduire la logique intuitionniste, le plus simple est de commencer par la déduction naturelle en logique implicative minimale, qui est la logique propositionnelle dans laquelle il n'y a qu'un connecteur, l'implication $\backslash Rightarrow$.

Rappelons qu'en déduction naturelle $\backslash Gamma\backslash vdash\backslash varphi$ doit se lire «de l'ensemble de propositions $\backslash ,\backslash Gamma$ on déduit la proposition $\backslash varphi$».

Il y a alors deux règles (voir plus bas Lecture des règles) :

$\backslash frac\{\backslash Gamma\backslash vdash\backslash varphi\backslash Rightarrow\backslash psi\backslash quad\backslash Gamma\backslash vdash\backslash varphi\}\{\backslash Gamma\backslash vdash\backslash psi\}\backslash quad(\backslash Rightarrow\; E)\backslash qquad\backslash qquad\backslash qquad\; \backslash frac\{\backslash Gamma,\backslash varphi\backslash vdash\backslash psi\}\{\backslash Gamma\backslash vdash\backslash varphi\backslash Rightarrow\backslash psi\}\backslash quad\; (\backslash Rightarrow\; I)$.

La première régle s'appelle la règle d'élimination de l'implication, tandis que la seconde règle s'appelle la règle d'introduction de l'implication. On remarque que l'élimination de l'implication est aussi le modus ponens bien connu. La méthode qui consiste à avoir pour chaque connecteur une (ou des) règle(s) d'élimination et une (ou des) règle(s) d'introduction est typique de la déduction naturelle et nous allons la retrouver par la suite.

Ce système de déduction est très simple (rasoir d'Ockham), mais il est moins puissant que la logique classique, car on ne peut y démontrer ni la loi de Peirce $((\backslash varphi\; \backslash Rightarrow\backslash psi)\backslash Rightarrow\backslash varphi)\backslash Rightarrow\backslash varphi,$ ni la proposition $((\backslash varphi\backslash Rightarrow\; \backslash psi)\; \backslash Rightarrow\; \backslash rho)\backslash Rightarrow((\backslash psi\backslash Rightarrow\; \backslash varphi)\; \backslash Rightarrow\; \backslash rho)\backslash Rightarrow\; \backslash rho.$

Lecture des règles

La règle d'élimination de l'implication peut se lire comme suit : si de l'ensemble d'hypothèses $\backslash Gamma$ je déduis $\backslash varphi\backslash Rightarrow\backslash psi$ et si de plus de l'ensemble d'hypothèses $\backslash Gamma$ je déduis $\backslash varphi$ alors de l'ensemble d'hypothèses $\backslash Gamma$ je déduis $\backslash psi$. Nous verrons (section interprétation de la logique intuinonniste) que l'expression «je déduis» prend un sens plus fort en logique intuitionniste qu'en logique classique. La règle d'introduction de l'implication, quant à elle, peut se lire comme suit : si de l'ensemble d'hypothèses $\backslash Gamma$ et de l'hypothèse $\backslash varphi$ je déduis $\backslash psi$ alors de l'ensemble d'hypothèses $\backslash Gamma$ je déduis $\backslash varphi\; \backslash Rightarrow\; \backslash psi$.

La logique propositionnelle intuitionniste

On conserve les règles de la logique implicative minimale concernant l'implication.

L'absurde

L'absurde est la proposition, notée $\backslash bot$, qui traduit une proposition essentiellement fausse. Elle est régie par une règle:

$\backslash frac\{\backslash Gamma\backslash vdash\backslash bot\}\{\backslash Gamma\backslash vdash\backslash varphi\}\; \backslash qquad\; (\backslash bot\; E).$

Cela signifie que si un ensemble de propositions $\backslash Gamma$ conduit à l'absurde, alors de cet ensemble de propositions $\backslash Gamma$, je peux déduire n'importe quelle proposition $\backslash varphi$.

Cette règle est aussi la règle d'élimination de l'absurde. Il n'y a pas (heureusement!) de règle d'introduction de l'absurde. Le nom de cette règle ne doit pas la faire confondre avec la règle de raisonnement par l'absurde (reductio ad absurdum) qui n'existe pas en logique intuitionniste. En effet le raisonnement par l'absurde est étroitement lié au tiers exclu et n'est pas constructif.

Remarque: en logique classique cette règle n'est pas utile, car elle est une conséquence du raisonnement par l'absurde.

La négation

Traditionnellement, on considère la négation comme une abréviation. Plus précisément on dit que $\backslash neg\backslash varphi$ est en fait une abréviation pour $\backslash varphi\; \backslash Rightarrow\; \backslash bot$. Il n'y a donc pas de règles spécifiques à la négation.

La conjonction

On introduit un nouveau connecteur binaire $\backslash land$, representant la conjonction de deux formules. On lit $A\; \backslash land\; B$ : A et B. On lui associe deux régles d'élimination, $\backslash land\; E\_1$ et $\backslash land\; E\_2$, et une régle d'introduction.

$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\_1\; \backslash land\; A\_2\}\{\backslash Gamma\; \backslash vdash\; A\_i\}\backslash quad(\backslash land\; E\_i)\backslash qquad\backslash qquad\backslash qquad\backslash frac\{\backslash Gamma\; \backslash vdash\; A\backslash quad\backslash Gamma\; \backslash vdash\; B\}\{\backslash Gamma\; \backslash vdash\; A\; \backslash land\; B\}\backslash quad(\backslash land\; I)$

La disjonction

On introduit un nouveau connecteur binaire $\backslash vee$, representant la disjonction de deux formules. Il est en quelque sorte symétrique du connecteur $\backslash land$. Ainsi, on lui associe une régle d'élimination et deux régles d'introduction.

$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; \backslash vee\; B\backslash quad\backslash Gamma,\; A\; \backslash vdash\; C\backslash quad\backslash Gamma,\; B\; \backslash vdash\; C\}\{\backslash Gamma\; \backslash vdash\; C\}\backslash quad\; (\backslash vee\; E)\backslash qquad\backslash qquad\backslash qquad\backslash frac\{\backslash Gamma\; \backslash vdash\; A\_i\}\{\backslash Gamma\; \backslash vdash\; A\_1\; \backslash vee\; A\_2\}\backslash quad(\backslash vee\; I\_i)$

On remarque que la règle d'élimination de la disjonction est une règle tryadique, c'est-à-dire qu'elle a trois prémisses.

Le calcul des prédicats intuitionniste

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 $\backslash Box$ où l'implication intuitionniste est $\backslash Box(p\backslash rightarrow\; q)$, quand $p\backslash rightarrow\; q$ 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. Notons que 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 $\backslash Box(\backslash varphi)$, si tous les mondes qui le dominent hiérarchiquement forcent $\backslash varphi$. Comme la nécessité ne va être appliquée qu'à l'implication, nous dirons qu'un monde force $\backslash varphi\backslash Rightarrow\backslash psi$ si pour tous les mondes m qui le dominent hiérarchiquement, on a m force $\backslash psi$ dès que m force $\backslash varphi$.

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:

• $((p\backslash Rightarrow\; q)\backslash Rightarrow\; r)\backslash Rightarrow((q\backslash Rightarrow\; p)\backslash Rightarrow\; r)\backslash Rightarrow\; r$,

• $((p\backslash Rightarrow\; q)\backslash Rightarrow\; p)\backslash Rightarrow\; p$ (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 intuinionniste, 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 .

• $\backslash mathcal\{U\}$ 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 ($C\backslash subseteq\backslash mathcal\{U\}$) tels que $m\backslash in\; C$ et

$\backslash mathcal\{I\}$ est une initialisation; c'est une application qui associe à chaque variable propositionnelle un cône de $\backslash mathcal\{U\}$.

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

• si $\backslash phi$ est une variable $x$, alors $m\backslash Vdash\; x$ si $m\backslash in\; \backslash mathcal\{I\}(x)$,
• si $\backslash phi$ est une proposition $\backslash psi\backslash Rightarrow\backslash theta$ alors $m\backslash Vdash\; \backslash psi\backslash Rightarrow\backslash theta$, si pour tout monde $m\text{'}$ tel que $m\backslash le\; m\text{'}$ on a si $m\backslash Vdash\; \backslash psi$ alors $m\backslash Vdash\backslash theta$.

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

On dit que $\backslash varphi$ est valide dans $\backslash mathcal\{M\}$ ou que $\backslash mathcal\{M\}$ modélise $\backslash varphi$, noté $\backslash mathcal\{M\}\backslash vDash\backslash varphi$, si pour $m\backslash in\backslash mathcal\{U\}\_\backslash mathcal\{M\}$, on a $m\backslash Vdash\backslash varphi$. On dit que $\backslash varphi$ est valide, si pour tout modèle $\backslash mathcal\{M\}$, $\backslash mathcal\{M\}\backslash vDash\backslash varphi$.

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, $\backslash vdash\backslash varphi$ implique $\backslash vDash\backslash varphi$.

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

On peut aussi trouver un contre-modèle très simple de la proposition $((p\backslash Rightarrow\; q)\backslash Rightarrow\; r)\backslash Rightarrow((q\backslash Rightarrow\; p)\backslash Rightarrow\; r)\backslash Rightarrow\; r$.

Complétude de la logique intuitionniste

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

Formellement, $\backslash vDash\backslash varphi$ implique $\backslash vdash\backslash varphi$.

La démonstration se fait de la façon suivante: si $\backslash varphi$ n'est pas démontrable alors on peut construire un contre-modèle (infini) de $\backslash varphi$ c'est-à-dire un modèle $\backslash mathcal\{M\}$ tel que $\backslash mathcal\{M\}\backslash not\backslash vDash\backslash varphi$.

Voir aussi

• Sémantique de Kripke