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

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

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

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

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

Ex falso quodlibet

En logique intuitionniste, comme en logique classique, est acceptée la règle suivante :

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

Cette règle est nommée principe d'explosion, ou en latin, ex falso quodlibet. ⊥ est la notation de L'absurde, c'est-à-dire d'une proposition fausse pour toutes les interprétations. Le principe d'explosion 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$ .

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$ , 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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. 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érarchisé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 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 $\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 de pré-ordre ,

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

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

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

Inclusion de la logique classique dans la logique intuitionniste

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 :

$f (\bot) = \bot$
$f (A) =\neg(\neg A )$ , pour une formule atomique $A$ différente de ⊥
$f ( A \and B) = f (A) \and f(B)$
$f (A \or B) = \neg \left[ \neg f (A) \and \neg f (B) \right]$
$f (A \Rightarrow B) = f(A) \Rightarrow f(B)$
$f ( \forall x P(x) ) = \forall x f ( P(x) )$
$f ( \exists x P(x) ) = \neg ( \forall x \neg f ( P(x) )$

Où $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)$ .

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

La Non-non traduction

Cette section semble contenir un travail inédit ou des déclarations non vérifiées.

Vous pouvez aider en ajoutant des références. Voir la page de discussion pour plus de détails.

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 a^b 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

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

Le fait que la négation $\lnot$ n’ait 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.

Références

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

Annexes

Bibliographie

Ouvrages

Jean-Yves Girard, Le point aveugle, Tome I, Hermann, 2007.
Jean Largeault, L'Intuitionisme, Paris, Presses universitaires de France, 1992.
Jean Largeault, Intuitionisme et théorie de la démonstration, Paris, J. Vrin,‎ 1992, 566 p. (ISBN 2-7116-10594, présentation en ligne)
Textes de Bernays, Brouwer, Gentzen…[et al.] réunis, traduits et présentés par Jean Largeault.
René David, Karim Nour et Christophe Raffali, Introduction à la logique, Dunod, 2001.

Liens externes

Richard Moot et Christian Retoré, « La "non-non" traduction de Gödel-Kolmogorov », Université Bordeaux I,‎ 2007
Étienne Lozes, « TD non non traduction », Laboratoire Spécification et Vérification — ENS Cachan,‎ 2009
Alexandre Miquel, « Réalisabilité et extraction de programmes », Laboratoire Preuves, Programmes et Systèmes (PPS) de Jussieu,‎ 2005 (sur la logique intuitionniste et l’interprétation de Brouwer-Heyting-Kolmogorov — interprétation BHK)

Articles connexes

Algèbre de Heyting (en)
Analyse constructive
Constructivisme (mathématiques)
Sémantique de Kripke

Portail de la philosophie
Portail de la logique

This article is issued from Wikipédia - version of the Thursday, June 18, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.

Logique intuitionniste

Approche informelle

Approche formelle

La logique implicative minimale

La logique propositionnelle intuitionniste

Ex falso quodlibet

La négation

La conjonction

La disjonction

Le calcul des prédicats intuitionniste

Le quantificateur universel

Le quantificateur existentiel

Exemples de différences avec la logique classique

Négation

Double négation

Conjonction

Disjonction

Quantificateur existentiel

Quantificateur universel

Tiers exclu

Relations entre les règles

Interprétation de la logique intuitionniste

Approche intuitive

Approche formelle

Correction de la logique intuitionniste

Complétude de la logique intuitionniste

Relations avec la logique classique

Inclusion de la logique classique dans la logique intuitionniste

La Non-non traduction

La question des preuves non constructives

La question du tiers-exclu

Références

Annexes

Bibliographie

Ouvrages

Liens externes

Articles connexes

Medical Encyclopedia