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

Sommaire

1 Approche informelle
2 Approche formelle
3 Interprétation de la logique intuitionniste
- 3.1 Approche intuitive
- 3.2 Approche formelle
  - 3.2.1 Correction de la logique intuitionniste
  - 3.2.2 Complétude de la logique intuitionniste
4 Relations avec la logique classique
5 Bibliographie
6 Références
7 Articles connexes
8 Liens externes

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 $ϕ$ , soit on a $ϕ$ , soit on a $n o n (ϕ)$ , formellement $\varphi \vee \neg\varphi$ . À titre d'exemple, il rejetait le raisonnement suivant^[1] :

« 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 $φ$ la proposition « $\sqrt2^\sqrt2$ est rationnel », on pourrait alors dire :

si $φ$ est vrai alors les irrationnels $a = \sqrt{2}$ et $b = \sqrt{2}$ conviennent,

si $φ$ 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 $φ$ est vrai ou faux). En fait, le théorème de Gelfond-Schneider permet de montrer que $\sqrt{2}^{\sqrt2}$ est 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 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, \Rightarrow$ , l’absurde $\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 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 $φ$ ».

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 $Γ$ je déduis $\varphi\Rightarrow\psi$ et si de plus de l'ensemble d'hypothèses $Γ$ je déduis $φ$ alors de l'ensemble d'hypothèses $Γ$ je déduis $ψ$ . 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 $Γ$ et de l'hypothèse $φ$ je déduis $ψ$ alors de l'ensemble d'hypothèses $Γ$ 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 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 $φ$ .

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

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^[2].

Négation

$\lnot A$

Interprétation : « Il est démontré que

A

est contradictoire » .

$\lnot A \Leftrightarrow \lnot \lnot \lnot A$

Attention : il ne faut pas en conclure que $A \Leftrightarrow \lnot \lnot A$ est vrai. Cela ne l’est strictement pas.

Double négation

$\lnot \lnot A$

Interprétation : « 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 » (et en particulier, surtout pas «

A

est vrai »).

$\lnot \lnot A \Leftarrow A$

C'est-à-dire $A \Rightarrow \lnot \lnot A$ .

Attention : la réciproque n’est pas vraie, on n'a pas $\lnot \lnot A \Rightarrow A$ , ce qui explique que nous n’ayons pas non plus $\lnot \lnot A \Leftrightarrow A$ .

L’expression $A \Rightarrow \lnot \lnot A$ peut s’interpréter comme « Si

A

est vraie, alors

A

n’est pas contradictoire ». La précédente remarque sur la non-validité de l’implication réciproque, s’interprète donc comme « Que

A

ne soit pas contradictoire, n’est encore pas assez pour nous permettre de construire une preuve que

A

est vraie »…

A

restant encore à démontrer.

Remarque : la non-contradiction de

A

, bien qu’insuffisante pour constituer une preuve de

A

, reste tout de même une condition nécessaire à cette démonstration.

Conjonction

$A \land B$

Interprétation : « Preuve que

A

et preuve que

B

» (comparable à ce qu’il en est en logique classique).

$\lnot (A \land B) \Leftarrow (\lnot A) \lor (\lnot B)$

C'est-à-dire $(\lnot A) \lor (\lnot B) \Rightarrow \lnot (A \land B)$ .

Contrairement à ce qu’il en serait en logique classique, $\lnot (A \land B)$ n’est seulement qu’une implication de $(\lnot A) \lor (\lnot B)$ , mais n’est pas équivalent à $(\lnot A) \lor (\lnot B)$ . En effet, l’équivalence nécessiterait d’accepter l’implication réciproque $\lnot (A \land B) \Rightarrow (\lnot A) \lor (\lnot B)$ , qui permettrait d’introduire un brouillage entre A et B (par la disjonction), dont il n’est possible de rien conclure selon le principe constructiviste, car $\lnot A$ et $\lnot B$ pourraient être simultanément vrais tout autant qu’un seul des deux, sans qu’il ne soit possible de déterminer ce qu’il en est concrètement.

Disjonction

$A \lor B$

Interprétation : « Preuve que

A

ou preuve que

B

» .

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

A et B s’excluent mutuellement et ne sont pas simultanément vrais.

Comparable à ce qu’il en serait dans la logique classique de Boole et Karnaugh.

Quantificateur existentiel

$\exists x A(x)$

Interprétation : « Nous savons comment créer un

x

et pouvons prouver que

A (x)

» (et non pas « Il existe théoriquement un

x

vérifiant

A (x)

»)

$\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).

Comparable à ce qu’il en serait en logique classique.

Quantificateur universel

$\forall x A(x)$

Interprétation : « Preuve que pour chaque x appartenant à l’ensemble spécifié, nous pouvons toujours prouver A(x) » (comparable à ce qu’il en est en logique classique).

$\lnot (\forall x A(x)) \Leftarrow \exists x (\lnot A(x))$

C'est-à-dire $\exists x (\lnot A(x)) \Rightarrow \lnot (\forall x A(x))$ .

Contrairement à ce qu’il en serait en logique classique, $\lnot (\forall x A(x))$ n’est seulement qu’une implication de $\exists x (\lnot A(x))$ mais n’est pas équivalent à $\exists x (\lnot A(x))$ , car l’équivalence nécessiterait d’accepter l’implication réciproque $\lnot (\forall x A(x)) \Rightarrow \exists x (\lnot A(x))$ , qui présente un cas d’attention pour l’intuitionnisme. En effet, il requiert qu’en démontrant $\exists x (\lnot A(x))$ , on fournisse un moyen de montrer également un x qui vérifie cette affirmation positive de l’existence d’un x. Si cela est nécessaire, il faudra le prouver d’une autre manière, et il ne sera pas permis de l’assimiler à une conséquence de $\lnot (\forall x A(x))$ (ce qui ne « démontrerait » que son existence théorique). Cependant, l’implication présentée plus haut reste permise.

Tiers exclu

$A \lor \lnot A$

Cette relation n’est pas automatiquement valide, et elle n’en est pas plus automatiquement invalide. Elle est valide si nous pouvons prouver

A

ou prouver $\lnot A$ . Par exemple, dans $x \in \mathbb{N}, y \in \mathbb{N}, (x = y \lor x \neq y)$ , l’expression $(x = y \lor x \neq y)$ est valide, car nous pouvons toujours soit prouver

(x = y)

, soit prouver $(x \neq y)$ . Si nous prouvons

(x = y)

, alors $(x \neq y)$ est contradictoire ( $\lnot A$ ), ce qui est une interprétation valide. Et si nous pouvons prouver la contradiction de

(x = y)

, qui est $\lnot A$ , en prouvant $(x \neq y)$ , l’interprétation est valide de même. Par contre, l’expression ne serait plus valide avec $x \in \mathbb{R}, y \in \mathbb{R}$ , car l’égalité ou l’inégalité entre deux réels, peut être non-calculable, c'est-à-dire, non-décidable (hors arrondi, mais il ne s’agirait alors plus de véritables réels au sens mathématique du terme). Elle serait valide avec $x \in \mathbb{Q}, y \in \mathbb{Q}$ (sous réserves que ces rationnels ne soient pas représentés par des expressions de longueur infinie).

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 $V r a i$ et $F a u x$ , 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è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 $φ$ . 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 $ψ$ dès que m force $φ$ .

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

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

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

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

$((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 $φ$ , que l'on écrit $m\Vdash \varphi$ et que l'on lit $m$ force $φ$ . La relation de forçage est définie par induction sur la structure des formules.

si $ϕ$ est une variable $x$ , alors $m\Vdash x$ si $m\in \mathcal{I}(x)$ ,
si $ϕ$ 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 $φ$ ) que pour chaque proposition $φ$ , l'ensemble des $m$ tels que $m\Vdash\varphi$ est un cône.

On dit que $φ$ est valide dans $\mathcal{M}$ ou que $\mathcal{M}$ modélise $φ$ , noté $\mathcal{M}\vDash\varphi$ , si pour $m\in\mathcal{U}_\mathcal{M}$ , on a $m\Vdash\varphi$ . On dit que $φ$ 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 $φ$ n'est pas démontrable alors on peut construire un contre-modèle (infini) de $φ$ 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 $\bot$
$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

Ce qui amena Brouwer à concevoir l’intuitionnisme étant une remise en cause de la qualité des preuves de la logique classique^[3], 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-exclus

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-exclus de la logique classique, qui est (en termes intuitionniste) $\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 la raison pour laquelle le tiers-exclus classique ne peut pas fonder une preuve intuitionniste : son interprétabilité est faible.

Bibliographie

Dirk van Dalen, Logic and structure, Springer-Verlag, 1991.
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, Vrin, 1992.
René David, Karim Nour, Christophe Raffali, Introduction à la logique, Dunod, 2001.

Références

↑ Alexandre Miquel, « L’intuitionnisme : où l’on construit une preuve », dans Pour la Science, n^o 49 « Argumentation et preuve », Octobre-Décembre 2005, p. 33, cadre B [texte intégral]
↑ . (fr) [PDF] Joseph Vidal-Rosset, « Intuitionnisme (sur l’interprétation des expressions et la philosophie) », Université de Nancy 2, 2006. Consulté le Vendredi 11 juin 2010
↑ (fr) [PDF] Franck Wynen, « La logique intuitionniste (sur l’épistémologie et l’histoire de la logique intuitionniste de Platon au XX^e siècle) », Conservatoire National des Arts & Métiers (CNAM), 2000-2001. Consulté le Mardi 8 juin 2010

Liens externes

(fr) [PDF] Richard Moot & Christian Retoré, « La Non-non traduction de Gödel-Kolmogorov », Université Bordeaux I, 2007. Consulté le Mercredi 9 juin 2010

(fr) [PDF] Etienne Lozes, « TD Non-non traduction », Laboratoire Spécification et Vérification — CNS Cachan, 2009. Consulté le Vendredi 11 juin 2010

(fr) [PDF] Alexandre Miquel, « Réalisabilité et extraction de programmes (sur la logique intuitionniste et l’interprétation de Brouwer-Heyting-Kolmogorov — interprétation BHK) », Laboratoire Preuves, Programmes et Systèmes (PPS) de Jussieu, 2005. Consulté le Mercredi 9 juin 2010

Catégories :

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Logique intuitionniste de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

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… … Wikipédia en Français
Logique intuitionniste — ● Logique intuitionniste logique qui présente de notables différences par rapport à la logique classique. (La loi de la double négation : non non p → p (¬ ¬ p → p), en particulier, n y est pas admise.) … Encyclopédie Universelle
Logique Minimale — La logique minimale est, comme la logique intuitionniste, une variante de la logique classique. Les trois logiques diffèrent sur la façon de traiter la négation et la contradiction dans le calcul des propositions ou le calcul des prédicats. Dans… … Wikipédia en Français
Logique Classique — La logique classique est l ensemble des principes de raisonnements usuellement utilisés en mathématiques, tels qu ils ont été formalisés au début du XXe siècle. C est l apparition d autres systèmes logiques, notamment la logique… … Wikipédia en Français
Logique Linéaire — La logique linéaire (LL), inventée par le logicien Jean Yves Girard en 1986, est un produit de la théorie de la démonstration moderne. Elle résulte d une analyse du comportement des preuves des logiques classique et intuitionniste au travers de… … Wikipédia en Français
Logique lineaire — Logique linéaire La logique linéaire (LL), inventée par le logicien Jean Yves Girard en 1986, est un produit de la théorie de la démonstration moderne. Elle résulte d une analyse du comportement des preuves des logiques classique et… … Wikipédia en Français
Logique (mathématiques) — Logique mathématique La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme. Ses débuts furent marqués par la rencontre entre deux idées nouvelles : la volonté chez Frege, Russell, Peano et… … Wikipédia en Français
Logique Mathématique — La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme. Ses débuts furent marqués par la rencontre entre deux idées nouvelles : la volonté chez Frege, Russell, Peano et Hilbert de donner une … Wikipédia en Français
Logique mathematique — Logique mathématique La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme. Ses débuts furent marqués par la rencontre entre deux idées nouvelles : la volonté chez Frege, Russell, Peano et… … Wikipédia en Français
Logique Combinatoire — Pour les articles homonymes, voir combinatoire (homonymie). Avertissement: Cet article traite de la logique combinatoire, au sens qu a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu avec ce que l on… … Wikipédia en Français

Dictionnaires et Encyclopédies sur 'Academic'

Logique intuitionniste

Sommaire

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

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

Bibliographie

Références

Articles connexes

Liens externes

Regardez d'autres dictionnaires:

Share the article and excerpts

Dictionnaires et Encyclopédies sur 'Academic'

Wikipédia en Français

Logique intuitionniste

Sommaire

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

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

Bibliographie

Références

Articles connexes

Liens externes

Regardez d'autres dictionnaires:

Share the article and excerpts

Direct link