Logique intuitionniste

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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 Arend Heyting. Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique. Gerhard Gentzen en a formulé 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 faisant d'elle historiquement la première des logiques constructives. Des travaux la concernant, effectués par Gödel et Andreï Kolmogorov au sujet de la « non-non interprétation » (interprétation de la double négation) ont ouvert la porte de l’interprétation de la logique classique dans les termes de la logique intuitionniste. L'étude de la logique intuitionniste est la clé pour bien comprendre la logique classique et ses subtilités.

Approche informelle[modifier | modifier le code]

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 contre-intuitives. En fait, il refusait deux principes.

  • Le tiers exclu, qui consiste à dire qu'étant donnée une proposition P, soit on a P, soit on a \text{non}P, formellement P \vee \neg P. À titre d'exemple, il rejetait le raisonnement suivant[1],[2] :

« Il existe des nombres irrationnels a et b, tels que a^b est un nombre rationnel. En effet, on sait que la racine carrée de deux est irrationnelle, et 2 est évidemment rationnel. En notant \varphi la proposition « \sqrt2^\sqrt2 est rationnel », on pourrait alors dire :

si \varphi est vrai alors les irrationnels a = \sqrt{2} et b = \sqrt{2} conviennent,
si \varphi est faux alors les irrationnels a= \sqrt{2}^{\sqrt2} et b = \sqrt{2} conviennent (l'irrationalité de a étant l’hypothèse \neg\varphi), puisque a^b = (\sqrt{2}^{\sqrt2})^{\sqrt2} = \sqrt{2}^{\sqrt{2}\times\sqrt{2}} = \sqrt{2}^2 =2 est rationnel ».

La critique de cette démonstration est qu'elle n'est pas constructive : de par son utilisation du tiers exclu, elle n'exhibe pas une solution explicite, mais démontre seulement l'existence d'un couple-solution sans pouvoir préciser lequel (puisqu'on ne sait pas si \varphi est vrai ou faux). En fait, le théorème de Gelfond-Schneider permet de montrer que \sqrt{2}^{\sqrt2} est transcendant, donc irrationnel, et que c'est donc a= \sqrt{2}^{\sqrt2} 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 (\exists x)~P(x), il donne aussi un moyen de construire x qui satisfait P.

Brouwer a 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 en font 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[modifier | modifier le code]

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, \Rightarrow, l’absurde ⊥ 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 ainsi que pour l’absurde.

La logique implicative minimale[modifier | modifier le code]

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.

En déduction naturelle, \Gamma\vdash\varphi se lit « de l'ensemble de propositions \,\Gamma on déduit la proposition \varphi ».

Il y a alors deux règles (voir plus bas Lecture des 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 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 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 intuitionniste) 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[modifier | modifier le code]

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

L'absurde[modifier | modifier le code]

L'absurde est la proposition, notée ⊥, qui traduit une proposition essentiellement 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 Γ conduit à l'absurde, alors de cet ensemble de propositions Γ, je peux déduire n'importe quelle proposition \varphi.

Cette règle est aussi la règle d'élimination de l'absurde. Il n'existe (heureusement !) pas 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[modifier | modifier le code]

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[modifier | modifier le code]

On introduit un nouveau connecteur binaire \land, représentant la conjonction de deux formules. On lit A \land B : A et B. On lui associe deux règles d'élimination, \land E_1 et \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[modifier | modifier le code]

On introduit un nouveau connecteur binaire \vee, représentant 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).

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[modifier | modifier le code]

Le calcul des prédicats intuitionniste reprend toutes les règles du calcul propositionnel intuitionniste ci-dessus et lui adjoint de nouvelles règles pour les quantificateurs « quel que soit » et « il existe ». Son langage et son ensemble de formules demeurent les mêmes que ceux du calcul des prédicats classiques.

Remarque : Nous rappelons que A[t/x] signifie le remplacement de toutes les occurrences librement substituables de la variable x par le terme t ; voir calcul des prédicats pour les notions de « variable », « terme », « substitution » et de « librement substituable ».

Le quantificateur universel[modifier | modifier le code]

  • Règle d'introduction :\frac{\Gamma \vdash A}{\Gamma \vdash \forall x A}
  • Règle d'élimination :\frac{\Gamma , A[t/x] \vdash B}{\Gamma, \forall x A\vdash B}

Le quantificateur existentiel[modifier | modifier le code]

  • Règle d'introduction :\frac{\Gamma \vdash A[t/x]}{\Gamma \vdash \exists x A}
  • Règle d'élimination :\frac{\Gamma, A \vdash B}{\Gamma, \exists x A \vdash B }

Exemples de différences avec la logique classique[modifier | modifier le code]

Les opérations ne sont pas définies l’une par rapport à l’autre (voir plus loin), et ne sont définies qu’en elles-mêmes. Elles sont définies par l’interprétation qui doit en être faite. Pour cette raison, en plus des règles de calcul, sont données les interprétations qui doivent être faites des expressions de chaque opérateur[3].

Négation[modifier | modifier le code]

On peut interpréter \lnot A comme : « Il est démontré que A est contradictoire ».

On dispose en logique intuitionniste du théorème suivant :

  • \lnot A \Leftrightarrow \lnot \lnot \lnot A

Mais on ne peut pas en conclure que A \Leftrightarrow \lnot \lnot A est vrai. En effet, cette dernière équivalence ne peut être prouvée en logique intuitionniste.

Double négation[modifier | modifier le code]

On peut interpréter \lnot \lnot A comme : « Il est prouvé qu’il est contradictoire d’affirmer que A est contradictoire », c'est-à-dire « Il est prouvé que A n’est pas contradictoire ». Mais on ne peut pas en déduire que « A est vrai ».

On dispose en logique intuitionniste du théorème suivant :

  • A \Rightarrow \lnot \lnot A

Mais la réciproque n’est pas vraie. On n'a pas \lnot \lnot A \Rightarrow A. L’expression A \Rightarrow \lnot \lnot A peut s’interpréter comme « Si A est vraie, alors A n’est pas contradictoire ». Mais le fait que A ne soit pas contradictoire n’est pas suffisant pour établir une preuve que « A est vraie ».

À titre d'exemple, soit x un réel et A la proposition x est rationnel. Prouver A, c'est donner deux entiers a et b tels que x = a/b. Si A est contradictoire (et donc si on a \lnot A), c'est que x est non rationnel, ou irrationnel. Dire que l'on a \lnot \lnot A, c'est dire que supposer x irrationnel conduit à une contradiction, et donc conclure que x n'est pas irrationnel. Mais ce n'est pas suffisant pour établir l'existence effective de deux entiers a et b tels que x = a/b. Ainsi, en logique intuitionniste, ne pas être irrationnel est une propriété différente et plus faible que celle d'être rationnel.

Conjonction[modifier | modifier le code]

L'interprétation de A \land B est : on dispose d'une preuve de A et d'une preuve de B (comparable à ce qu’il en est en logique classique).

En logique intuitionniste, la proposition suivante est un théorème :

  • (\lnot A) \lor (\lnot B) \Rightarrow \lnot (A \land B)

Mais contrairement à ce qu’il en serait en logique classique, \lnot (A \land B) n’est seulement qu’une conséquence de (\lnot A) \lor (\lnot B), la réciproque étant fausse. En effet, supposer que A \land B est contradictoire, est insuffisant en logique intuitionniste pour conclure si A seul l'est ou B seul ou s'ils le sont tous les deux. Par exemple, supposer qu'un nombre est à la fois rationnel et irrationnel est contradictoire, mais insuffisant pour conclure si ce nombre est irrationnel ou non.

Disjonction[modifier | modifier le code]

L'interprétation de A \lor B est : on a une preuve de A ou une preuve de B.

On dispose en logique intuitionniste du théorème suivant :

  • \lnot (A \lor B) \Leftrightarrow (\lnot A) \land (\lnot B)

A et B s’excluent mutuellement et ne sont pas simultanément vrais. Cette situation est comparable à ce qu’il en serait dans la logique classique de Boole et Karnaugh.

Par contre, le théorème suivant :

  • ((\lnot A) \lor B) \Rightarrow (A \Rightarrow B)

est valide en logique intuitionniste, mais pas sa réciproque. En effet, si x est un nombre réel, on sait que s'il est rationnel alors il n'est pas irrationnel, mais on n'est pas pour autant capable de conclure si ce nombre est irrationnel ou non.

Quantificateur existentiel[modifier | modifier le code]

L'interprétation de \exists x A(x) est : nous pouvons créer un objet x et prouver que A(x). L'existence de x est ici effective ou constructive. Il ne s'agit pas d'une existence théorique d'un élément x vérifiant A(x).

On dispose du théorème suivant :

  • \lnot (\exists x A(x)) \Leftrightarrow \forall x (\lnot A(x))

S’il n’existe pas de x qui vérifie A(x) alors pour tous les x on ne vérifie pas A(x), d’où l’équivalence (qui correspond à l’intuition et se formule naturellement). Cette propriété est comparable à ce qu’il en serait en logique classique.

Quantificateur universel[modifier | modifier le code]

L'interprétation de \forall x A(x) est : on a une preuve que pour chaque x appartenant à l’ensemble spécifié, on peut prouver A(x) (comparable à ce qu’il en est en logique classique).

On dispose en logique intuitionniste du théorème suivant :

  • \exists x (\lnot A(x)) \Rightarrow \lnot (\forall x A(x))

Mais contrairement à ce qu’il en serait en logique classique, la réciproque est fausse. En effet, cette réciproque exigerait que, en supposant contradictoire l'universalité de la propriété A(x), on soit capable d'exhiber explicitement un objet x invalidant A(x), ce qui n'est rarement possible.

On peut aussi dire que, en logique intuitionniste, l'affirmation de \exists x A(x) est l'affirmation de l'existence effective et constructible d'un objet x validant A(x), alors que \lnot (\forall x \lnot A(x)) n'en est que l'existence théorique, exprimant seulement qu'il est contradictoire que A(x) soit universellement contradictoire. La logique classique ne fait aucune distinction entre ces deux existences, alors que la logique intuitionniste considère la deuxième comme plus faible que la première.

Tiers exclu[modifier | modifier le code]

La proposition suivante

  • A \lor \lnot A

est un théorème de la logique classique, mais pas de la logique intuitionniste. Dans cette dernière, elle signifierait que nous pouvons prouver A ou prouver \lnot A, ce qui n'est pas toujours possible.

Par exemple, en arithmétique munie de la logique intuitionniste (dite arithmétique de Heyting), l’expression (x = y \lor x \neq y) est valide, car pour tout couple d'entiers, on peut prouver qu'ils sont égaux, ou on peut prouver qu'ils sont différents. Il en est de même pour deux rationnels. Mais pour deux réels en analyse constructive, on ne dispose pas de méthode générale permettant de prouver que x = y ou de prouver que x \neq y. Cette situation correspond bien aux situations qu'on rencontre en algorithmique, où l’égalité ou l’inégalité entre deux réels peut être non calculable, c'est-à-dire, non décidable.

Relations entre les règles[modifier | modifier le code]

Pour mieux comprendre, on remarquera dans ce qui précède, que contrairement à ce qu’il en est dans la logique de Boole, la conjonction \land ne peut pas être reformulée en termes de disjonction \lor et que le quantificateur existentiel \exists ne peut pas être reformulé en termes de quantificateur universel \forall ; ceci en vertu du principe du constructivisme. Dit d’une autre manière et dans des termes peut-être plus proches de l’informatique : il n’est pas permis de réduire les contraintes d’une expression.

Concernant la disjonction \lor et le quantificateur universel \forall, seules leurs expressions sous formes négatives peuvent être reformulées en termes de, respectivement, conjonction \land et quantificateur existentiel \exists. Cependant, une remarque : il n’est pas possible de contourner cette exigence par l’usage de doubles négations, car (et justement pour cette raison) en logique intuitionniste, \lnot \lnot A n’est pas équivalent à A.

Les interprétations des expressions ne se font pas dans le sens de Vrai et Faux, mais dans le sens de Prouvable et Contradictoire. C’est ce qui explique que nous ne disposons pas de tables de calcul, comme avec l’algèbre de Boole, ce qui ensuite, explique pourquoi les opérations ne puissent pas être redéfinies dans les termes d’une autre.

Interprétation de la logique intuitionniste[modifier | modifier le code]

Approche intuitive[modifier | modifier le code]

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. 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ère 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,

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[modifier | modifier le code]

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 \langle\mathcal{U}, <, \mathcal{I}\rangle.

  • \mathcal{U} est appelé l'univers et ses éléments notés m sont appelés des mondes ;

Un cône est un ensemble C de mondes (C\subseteq\mathcal{U}) tels que m\in C et m<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.

Pour des compléments brefs de cette section, on peut consulter le paragraphe 4.4 du livre « Introduction à la logique de David, Nour, Raffali », cité dans la bibliographie ci-dessous.

Correction de la logique intuitionniste[modifier | modifier le code]

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<m_1 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[modifier | modifier le code]

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.

Relations avec la logique classique[modifier | modifier le code]

Inclusion de la logique classique dans la logique intuitionniste[modifier | modifier le code]

Si l’on admet la démonstration faite par Kurt Gödel, que l’insertion de double-négations placées selon des règles définies, nommée « non-non traduction de Gödel-Kolmogorov » (voir ci-après), permet de rendre démontrable en logique intuitionniste toute formule démontrable en logique classique ; et si l’on considère qu’en logique intuitionniste, \lnot \lnot A est une forme affaiblie de A, alors il est possible d’assimiler la logique classique à une forme affaiblie de la logique intuitionniste et de voir la logique classique comme incluse dans la logique intuitionniste. Remarque : si l’on admet cela, on peut également faire remarquer que la logique intuitionniste n’est pas « moins capable » que la logique classique (voir les exposés qui suivent).

De manière plus économe que la saturation des formules et sous-formules par des doubles négations, Gödel a remarqué que si on considère une fonction f de l'ensemble des formules dans l'ensemble des formules définie par :

  1. f (\bot)  =  \bot
  2. f (A) =\neg(\neg A ), pour une formule atomique A différente de ⊥
  3. f ( A \and B)  =  f (A) \and f(B)
  4. f (A \or B)  =  \neg \left[ \neg f (A) \and  \neg f (B) \right]
  5. f (A \Rightarrow B)  =  f(A) \Rightarrow  f(B)
  6. f ( \forall x P(x) )  =  \forall x f ( P(x) )
  7. f ( \exists x P(x) ) = \neg ( \forall x \neg f ( P(x) )

A et B sont des formules quelconques et P est une formule ayant x comme paramètre.

Alors on a le théorème suivant :

  • \Gamma \vdash_c A \Leftrightarrow f (\Gamma) \vdash_i f (A).

\vdash_c est la déduction classique et \vdash_i est la déduction intuitionniste.

La Non-non traduction[modifier | modifier le code]

Ce qui amena Brouwer à concevoir l’intuitionnisme étant une remise en cause de la qualité des preuves de la logique classique[4], une question peut venir : quelle est donc la valeur d’une preuve de la logique classique du point de vue de la logique intuitionniste ? Dans le cas de la preuve de l’hypothèse qu’il existe des a et b irrationnels tels que ab soit rationnel (voir plus haut), la preuve de cette affirmation par le tiers-exclus est-elle fausse ? Il serait contradictoire de l’affirmer, puisque le théorème de Gelfond-Schneider indique que effectivement, l’une des deux hypothèses utilisées est concrètement vraie, et qu’il existe des solutions qui permettent d’en donner des exemples à l’œuvre. Cependant, comme vu précédemment, elle apporte une réponse… incomplète (elle ne réalise pas de solution). On pourra dire assez honnêtement, que la preuve par le tiers-exclus, montre au moins que l’affirmation de l’hypothèse qu’elle « démontre », n’est pas une contradiction. La preuve de la non-contradiction d’une hypothèse A selon la logique intuitionniste étant la preuve de \lnot \lnot A, c’est finalement la preuve de \lnot \lnot A (qui signifie que A peut éventuellement être démontré) qu’a effectuée la démonstration par la logique classique. Cette constatation est le fondement de la non-non traduction, qui permet d’exprimer une formule de la logique classique en logique intuitionniste (voir Liens externes). Ce principe a été formalisé par Kurt Gödel et Andreï Kolmogorov.

Attention : la non-non traduction est une traduction dans un seul sens. Bien qu’elle permette de traduire une expression de la logique classique en termes de la logique intuitionniste, elle ne garantit par l’inverse (mais l’inverse reste possible dans certains cas, comme il peut l’être trivialement pour une formule traduite de la logique classique). De plus et ne serait-ce que pour la raison que, par exemple en logique classique \lnot \lnot A \Leftrightarrow A ou encore qu’en logique classique les opérateurs peuvent être exprimés les uns par rapport aux autres, la non-non traduction ne peut pas être bijective : plusieurs expressions de la logique classique peuvent correspondre à une même expression de la logique intuitionniste.

La question des preuves non constructives[modifier | modifier le code]

Bien que le principe de la logique intuitionniste soit la preuve constructive, nous avons vu qu’il est possible de traduire une expression de la logique classique en logique intuitionniste. Cela amène à se poser la question des expressions de la logique intuitionniste, qui correspondraient à des expressions de la logique classique (suite à une traduction ou non). Nous avons vu que ces expressions peuvent faire usage de \lnot \lnot A qui signifie que A n’est pas contradictoire. Les preuves faites sur de telles expressions ne traiteront pas de choses concrètes, mais de potentialités (contradictoire ou non contradictoire) ; ce qui n’amène pas à exposer une solution au sens propre du terme, puisque l’objet, est la proposition. La logique intuitionniste, peut donc également faire des démonstrations non constructives ; mais ces démonstrations sont alors identifiées comme telles, et ne disent rien de plus que « cela est contradictoire » ou « cela n’est pas contradictoire ». La logique intuitionniste peut donc produire des preuves ayant sens pour la logique classique. Une interprétation de cette remarque, est que la logique intuitionniste, éclaire ce que fait la logique classique, en donnant une interprétation de ce que sont les preuves classiques.

La question du tiers-exclu[modifier | modifier le code]

La négation \lnot n’ayant pas le même sens en logique intuitionniste qu’en logique classique, explique que A \lor \lnot A ne soit pas toujours valide en logique intuitionniste (après tout, des similitudes syntaxiques n’indiquent pas nécessairement des similitudes sémantiques). Cependant, il existe une formulation du tiers-exclu de la logique classique, qui est (en termes intuitionnistes) \lnot \lnot (A \lor \lnot A). Cette expression reste toujours valide, même si A n’est pas décidable (c’est une conséquence de la signification du \lnot \lnot, qui a été présenté plus haut). Cette interprétation, « même si A n’est pas décidable \lnot \lnot (A \lor \lnot A) est toujours démontrable », est une autre mise en lumière de la raison pour laquelle le tiers-exclu classique ne peut pas fonder une preuve intuitionniste : son interprétabilité est faible.

Bibliographie[modifier | modifier le code]

Références[modifier | modifier le code]

  1. Alexandre Miquel, « L’intuitionnisme : où l’on construit une preuve », Pour la Science, no 49 « Argumentation et preuve »,‎ Octobre-Décembre 2005, p. 33, cadre B (lire en ligne).
  2. (en) Dirk van Dalen (de), Logic and structure, Springer, 1991, p. 155.
  3. Joseph Vidal-Rosset, « Intuitionnisme », Université de Nancy 2,‎ 2006 (sur l’interprétation des expressions et la philosophie).
  4. Franck Wynen, « La logique intuitionniste », CNAM,‎ 2000-2001 (sur l’épistémologie et l’histoire de la logique intuitionniste de Platon au XXe siècle).

Articles connexes[modifier | modifier le code]

Liens externes[modifier | modifier le code]