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.Heything. 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.

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.

Approche informelle

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

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

«Posons $b = \sqrt{2}$ , et maintenant si $\sqrt{2}^{\sqrt2}$ est rationnel prenons $a = \sqrt{2}$ , sinon prenons $a= \sqrt{2}^{\sqrt2}$ et nous avons $a^b = (\sqrt{2}^{\sqrt2})^{\sqrt2} = \sqrt{2}^{\sqrt{2}\times\sqrt{2}} = \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 exclus et qu'elle ne dit pas quel

a

fait marcher les choses. En fait, un théorème d'analyse affirme que

\sqrt{2}^{\sqrt2}

est en fait irrationnel et que c'est le

a

qu'il faut choisir, mais la démonstration fondée sur le tiers exclus 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 $(\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 exclus et n'accepterait que l'existentiel constructif. Cette attitude a été assez violemment critiquée par des mathématiciens comme David Hilbert et 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 \Rightarrow b$ n'est plus l'implication matérielle $\neg a \vee b$ . Quand un mathématicien intuitionniste affirme $a \Rightarrow b$ , il veut dire qu'il fournit un procédé de «construction» d'une démonstration de $b$ à partir d'une démonstration de $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 (

\vee, \wedge, \bot

) et chaque quantificateur (

\forall, \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

\Rightarrow

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

Il y alors deux règles:

\frac{\Gamma\vdash\varphi\Rightarrow\psi\quad\Gamma\vdash\varphi}{\Gamma\vdash\psi}\quad(\Rightarrow E)\qquad\qquad\qquad \frac{\Gamma,\varphi\vdash\psi}{\Gamma\vdash\varphi\Rightarrow\psi}\quad (\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 la flèche 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 le 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 $((\varphi \Rightarrow\psi)\Rightarrow\varphi)\Rightarrow\varphi,$ ni la proposition $((\varphi\Rightarrow \psi) \Rightarrow \rho)\Rightarrow((\psi\Rightarrow \varphi) \Rightarrow \rho)\Rightarrow \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 $\Gamma$ je déduis $\varphi\Rightarrow\psi$ et si de plus de l'ensemble d'hypothèses $\Gamma$ je déduis $\varphi$ alors de l'ensemble d'hypothèses $\Gamma$ je déduis $\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 $\Gamma$ et de l'hypothèse $\varphi$ je déduis $\psi$ alors de l'ensemble d'hypothèses $\Gamma$ je déduis $\varphi \Rightarrow \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

\bot

, qui traduit une proposition essentiellemment fausse. Elle est régie par une règle:

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

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

Cette règle est aussi la règle d'élimination de l'absurde. Il n'y 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 exclus et n'est pas constructif.

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

La négation

Traditionnellement, on considère la négation comme une abréviation. Plus précisément on dit que

\neg\varphi

est en fait une abréviation pour

\varphi \Rightarrow \bot

. Il n'y a donc pas de règles spécifiques à la négation.

La conjonction

On introduit un nouveau connecteur binaire

\land

, representant la conjonction de deux formules. On lit

A \land B

: A et B. On lui associe deux régles d'élimination,

\land E_1

\land E_2

, et une régle d'introduction.

\frac{\Gamma \vdash A_1 \land A_2}{\Gamma \vdash A_i}\quad(\land E_i)\qquad\qquad\qquad\frac{\Gamma \vdash A\quad\Gamma \vdash B}{\Gamma \vdash A \land B}\quad(\land I)

La disjonction

On introduit un nouveau connecteur binaire

\vee

, representant la disjonction de deux formules. Il est en quelque sorte symétrique du connecteur

\land

. Ainsi, on lui associe une régle d'élimination et deux régles d'introduction.

\frac{\Gamma \vdash A \vee B\quad\Gamma, A \vdash C\quad\Gamma, B \vdash C}{\Gamma \vdash C}\quad (\vee E)\qquad\qquad\qquad\frac{\Gamma \vdash A_i}{\Gamma \vdash A_1 \vee A_2}\quad(\vee I_i)

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

$((p\Rightarrow q)\Rightarrow p)\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.

Un modèle est formé d'un triplet $\langle\mathcal{U}, <, \mathcal{I}\rangle$ .

$\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\subseteq\mathcal{U}$ ) tels que $m\in C$ et $m impliquent m'\in C .$

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

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

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

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

On dit que $\varphi$ est valide dans $\mathcal{M}$ ou que $\mathcal{M}$ modélise $\varphi$ , noté $\mathcal{M}\vDash\varphi$ , si pour $m\in\mathcal{U}_\mathcal{M}$ , on a $m\Vdash\varphi$ . On dit que $\varphi$ est valide, si pour tout modèle $\mathcal{M}$ , $\mathcal{M}\vDash\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, $\vdash\varphi$ implique $\vDash\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 $\mathcal{N}\equiv\langle\{m_1,m_0\}, <, \mathcal{I}\rangle$ avec $m_0 et \mathcal{I}(p) = \{m_1\} et \mathcal{I}(q) = \emptyset, on peut montrer que m_0\not\Vdash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p, donc \mathcal{N}\not\vDash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p et donc que \not\vDash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p . 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 $((p\Rightarrow q)\Rightarrow r)\Rightarrow((q\Rightarrow p)\Rightarrow r)\Rightarrow r$ .

Complétude de la logique intuitionniste

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

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

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

logique | logique mathématique

Gourt Home::Gourt :: Logique intuitionniste

Approche informelle

Approche formelle

La logique implicative minimale

La logique propositionnelle intuitionniste

L'absurde

La négation

La conjonction

La disjonction

Le calcul des prédicats intuitionniste

Interprétation de la logique intuitionniste

Approche intuitive

Approche formelle

Correction de la logique intuitionniste

Complétude de la logique intuitionniste