Logique Intuitionniste

Logique Intuitionniste: Logique intuitionniste

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

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

Sommaire

1 Approche informelle

2 Approche formelle

2.1 La logique implicative minimale

2.2 La logique propositionnelle intuitionniste

2.2.1 L'absurde

2.2.2 La négation

2.2.3 La conjonction

2.2.4 La disjonction

2.3 Le calcul des prédicats intuitionniste

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

4.1 Références

4.2 Articles connexes

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

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$ . A titre d'exemple, il rejetait la démonstration suivante de la proposition : « Il existe des nombres irrationnels $a$ et $b$ , tels que $a b$ est un nombre rationnel» :

« Si $\sqrt{2}^{\sqrt2}$ est rationnel, $a = \sqrt{2}$ et $b = \sqrt{2}$ conviennent. Sinon, prenons $a= \sqrt{2}^{\sqrt2}$ et $b= \sqrt{2}$ . Nous avons $a^b = (\sqrt{2}^{\sqrt2})^{\sqrt2} = \sqrt{2}^{\sqrt{2}\times\sqrt{2}} = \sqrt{2}^2 =2$ qui donne le résultat puisque $2$ est évidemment rationnel ». La critique de cette démonstration est qu'elle utilise le tiers exclu et qu'elle n'exhibe pas un couple particulier qui serait solution. En fait, un théorème d'analyse affirme que $\sqrt{2}^{\sqrt2}$ est irrationnel et que c'est le $a$ qu'il faut choisir, mais la démonstration fondée sur le tiers exclu ne le dit pas.

L'existentiel non constructif. Brouwer veut que quand un mathématicien affirme il existe $x$ tel que $x$ est $P$ , que l'on écrirait formellement $(\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, \bot$ ) et chaque quantificateur ( $\forall, \exists$ ) doit être défini à partir de ses propres règles, autrement dit il n'y a pas de moyen de ramener la logique à un connecteur et à un quantificateur. C'est pourquoi nous allons donner des règles pour chaque connecteur.

La logique implicative minimale

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

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

Il y 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 ni la loi de Peirce $((\varphi \Rightarrow\psi)\Rightarrow\varphi)\Rightarrow\varphi,$ ni la proposition $((\varphi\Rightarrow \psi) \Rightarrow \rho)\Rightarrow((\psi\Rightarrow \varphi) \Rightarrow \rho)\Rightarrow \rho.$

Lecture des règles

La règle d'élimination de l'implication peut se lire comme suit : si de l'ensemble d'hypothèses $Γ$ je déduis $\varphi\Rightarrow\psi$ et si de plus de l'ensemble d'hypothèses $Γ$ je déduis $\varphi$ 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 $\varphi$ 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 $\varphi$ .

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

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

La négation

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

La conjonction

On introduit un nouveau connecteur binaire $\land$ , representant la conjonction de deux formules. On lit $A \land B$ : A et B. On lui associe deux régles d'élimination, $\land E_1$ 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$ , representant la disjonction de deux formules. Il est en quelque sorte symétrique du connecteur $\land$ . Ainsi, on lui associe une régle d'élimination et deux régles d'introduction.
$\frac{\Gamma \vdash A \vee B\quad\Gamma, A \vdash C\quad\Gamma, B \vdash C}{\Gamma \vdash C}\quad (\vee E)\qquad\qquad\qquad\frac{\Gamma \vdash A_i}{\Gamma \vdash A_1 \vee A_2}\quad(\vee I_i)$
On remarque que la règle d'élimination de la disjonction est une règle tryadique, c'est-à-dire qu'elle a trois prémisses.

Le calcul des prédicats intuitionniste

Interprétation de la logique intuitionniste

Approche intuitive

La logique intutionniste peut être vue comme une logique modale, munie de la modalité de nécessité, notée $\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 $\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 $ψ$ 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 d'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 $φ$ 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 $\varphi$ ) que pour chaque proposition $\varphi$ , l'ensemble des $m$ tels que $m\Vdash\varphi$ est un cône.

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

Correction de la logique intuitionniste

On peut montrer que la logique intuitionniste est correcte vis-à-vis des modèles de Kripke, c'est-à-dire que toute proposition démontrable est valide.

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

On peut utiliser ce résultat pour montrer qu'une proposition n'est pas démontrable en logique intuitionniste. Si on considère le modèle $\mathcal{N}\equiv\langle\{m_1,m_0\}, <, \mathcal{I}\rangle$ avec $m 0 < 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$ .

Voir aussi

Références

Articles connexes

Analyse constructive

Constructivisme (mathématiques)

Sémantique de Kripke

Portail des mathématiques

Portail de la philosophie

Portail de la logique

Ce document provient de « Logique intuitionniste ».

Catégories : Logique | Logique mathématique | Théorie des types | Théorie de la démonstration

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

Игры ⚽ Поможем решить контрольную работу

Regardez d'autres dictionnaires:

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

Mark and share
Search through all dictionaries
Translate…
Search Internet

Share the article and excerpts