Logique intuitionniste 506728 31066154 2008-06-27T12:26:21Z JAnDbot 127921 robot Retire: [[zh:数学直觉主义]] L''''intuitionnisme''' est une position philosophique vis-à-vis des mathématiques proposée par le mathématicien [[Hollande|hollandais]] [[Luitzen Egbertus Jan Brouwer]] comme une alternative à l'approche dite [[logique classique|classique]]. Elle a été ensuite formalisée, sous le nom de '''logique intuitionniste''', par ses élèves [[V. Glivenko]] et [[Arend Heyting|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 [[démonstration constructive|logiques constructives]]. 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 contrintuitives. En fait, il refusait deux concepts. * Le ''tiers exclu'', qui consiste à dire qu'étant donnée une proposition <math>\phi</math>, soit on a <math>\phi</math>, soit on a <math>non(\phi)</math>, formellement <math>\varphi \vee \neg\varphi</math>. A titre d'exemple, il rejetait la démonstration suivante de la proposition : ''«Il existe des nombres [[Nombre rationnel|irrationnel]]s <math>a</math> et <math>b</math>, tels que <math>a^b</math> est un [[nombre rationnel]]»'' : ''«Posons <math>b = \sqrt{2}</math>, et maintenant si <math>\sqrt{2}^{\sqrt2}</math> est rationnel prenons <math>a = \sqrt{2}</math>, sinon prenons <math>a= \sqrt{2}^{\sqrt2}</math> et nous avons <math>a^b = (\sqrt{2}^{\sqrt2})^{\sqrt2} = \sqrt{2}^{\sqrt{2}\times\sqrt{2}} = \sqrt{2}^2 =2</math> qui donne le résultat puisque <math>2</math> est évidemment rationnel»''. La critique de cette démonstration est qu'elle utilise le tiers exclu et qu'elle ne dit pas quel <math>a</math> fait marcher les choses. En fait, un théorème d'analyse affirme que <math>\sqrt{2}^{\sqrt2}</math> est irrationnel et que c'est le <math>a</math> 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 <math>x</math> tel que <math>x</math> est <math>P</math>'', que l'on écrirait formellement <math>(\exists x)~P(x)</math>, il donne aussi un moyen de construire <math>x</math> qui satisfait <math>P</math>. Brouwer a donc 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 <math>a \Rightarrow b</math> n'est plus l'''implication matérielle'' <math>\neg a \vee b</math>. Quand un mathématicien intuitionniste affirme <math>a \Rightarrow b</math>, il veut dire qu'il fournit un procédé de «construction» d'une démonstration de <math>\ b</math> à partir d'une démonstration de <math>\ a</math>. 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 (<math>\vee, \wedge, \bot</math>) et chaque quantificateur (<math>\forall, \exists</math>) 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 minimale|logique implicative minimale]], qui est la logique propositionnelle dans laquelle il n'y a qu'un connecteur, l'implication <math>\Rightarrow</math>. Rappelons qu'en déduction naturelle <math>\Gamma\vdash\varphi</math> doit se lire ''«de l'ensemble de propositions <math>\,\Gamma</math> on déduit la proposition <math>\varphi</math>»''. Il y a alors deux règles (voir plus bas '''''Lecture des règles''''') : <center><math>\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)</math>.</center> 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 [[Raisonnement|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]] <math>((\varphi \Rightarrow\psi)\Rightarrow\varphi)\Rightarrow\varphi,</math> ni la proposition <math>((\varphi\Rightarrow \psi) \Rightarrow \rho)\Rightarrow((\psi\Rightarrow \varphi) \Rightarrow \rho)\Rightarrow \rho.</math> '''''Lecture des règles''''' La règle d'élimination de l'implication peut se lire comme suit : si de l'ensemble d'hypothèses <math>\Gamma</math> je déduis <math>\varphi\Rightarrow\psi</math> et si de plus de l'ensemble d'hypothèses <math>\Gamma</math> je déduis <math>\varphi</math> alors de l'ensemble d'hypothèses <math>\Gamma</math> je déduis <math>\psi</math>. 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 <math>\Gamma</math> et de l'hypothèse <math>\varphi</math> je déduis <math>\psi</math> alors de l'ensemble d'hypothèses <math>\Gamma</math> je déduis <math>\varphi \Rightarrow \psi</math>. ===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 <math>\bot</math>, qui traduit une proposition essentiellement fausse. Elle est régie par une règle: <center><math>\frac{\Gamma\vdash\bot}{\Gamma\vdash\varphi} \qquad (\bot E).</math></center> Cela signifie que si un ensemble de propositions <math>\Gamma</math> conduit à l'absurde, alors de cet ensemble de propositions <math>\Gamma</math>, je peux déduire n'importe quelle proposition <math>\varphi</math>. 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 <math>\neg\varphi</math> est en fait une abréviation pour <math>\varphi \Rightarrow \bot</math>. Il n'y a donc pas de règles spécifiques à la négation. ====La conjonction==== On introduit un nouveau connecteur binaire <math>\land</math>, representant la conjonction de deux formules. On lit <math>A \land B</math> : ''A et B''. On lui associe deux régles d'élimination, <math>\land E_1</math> et <math>\land E_2</math>, et une régle d'introduction. <center><math>\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)</math></center> ====La disjonction==== On introduit un nouveau connecteur binaire <math>\vee</math>, representant la disjonction de deux formules. Il est en quelque sorte symétrique du connecteur <math>\land</math>. Ainsi, on lui associe une régle d'élimination et deux régles d'introduction. <center><math>\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)</math></center> 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 <math>\Box</math> où l'implication intuitionniste est <math>\Box(p\rightarrow q)</math>, quand <math>p\rightarrow q</math> est l'implication classique. Cela peut se lire ''nécessairement p implique q''. L'idée des [[sémantique de Kripke|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 [[sémantique de Kripke|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 <math>\Box(\varphi)</math>, si tous les mondes qui le dominent hiérarchiquement forcent <math>\varphi</math>. Comme la nécessité ne va être appliquée qu'à l'implication, nous dirons qu'un monde force <math>\varphi\Rightarrow\psi</math> si pour tous les mondes ''m'' qui le dominent hiérarchiquement, on a ''m'' force <math>\psi</math> dès que ''m'' force <math>\varphi</math>. On dira qu'un modèle de Kripke ''satisfait'' ou ''modèlise'' une proposition si <u>tous</u> les mondes qu'il contient forcent cette proposition. Une proposition est ''valide'', si elle est <u>satisfaite par tous les modèles</u>. On peut montrer que la logique intuitionniste est [[logique mathématique#Système logique|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: *<math>((p\Rightarrow q)\Rightarrow r)\Rightarrow((q\Rightarrow p)\Rightarrow r)\Rightarrow r</math>, * <math>((p\Rightarrow q)\Rightarrow p)\Rightarrow p</math> ([[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 [[logique mathématique#Système logique|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 <math>\langle\mathcal{U}, <, \mathcal{I}\rangle</math>. * <math>\mathcal{U}</math> est appelé l'''univers'' et ses éléments notés <math>m</math> sont appelés des ''mondes'', * <math><</math> est une [[relation d'ordre]] , Un ''cône'' est un ensemble <math>C</math> de mondes (<math>C\subseteq\mathcal{U}</math>) tels que <math>m\in C</math> et <math>m<m'</math> impliquent <math>m'\in C</math>. <math>\mathcal{I}</math> est une ''initialisation''; c'est une application qui associe à chaque variable propositionnelle un cône de <math>\mathcal{U}</math>. On définit une relation <math>\Vdash</math> de ''réalisabilité'' ou de ''forçage'' entre un monde <math>m</math> et une proposition <math>\varphi</math>, que l'on écrit <math>m\Vdash \varphi</math> et que l'on lit ''<math>m</math> force <math>\varphi</math>''. La relation de ''forçage'' est définie par induction sur la structure des formules. * si <math>\phi</math> est une variable <math>x</math>, alors <math>m\Vdash x</math> si <math>m\in \mathcal{I}(x)</math>, * si <math>\phi</math> est une proposition <math>\psi\Rightarrow\theta</math> alors <math>m\Vdash \psi\Rightarrow\theta</math>, si pour tout monde <math>m'</math> tel que <math>m\le m'</math> on a si <math>m\Vdash \psi</math> alors <math>m\Vdash\theta</math>. On peut démontrer (par induction sur la structure ou la taille de <math>\varphi</math>) que pour chaque proposition <math>\varphi</math>, l'ensemble des <math>m</math> tels que <math>m\Vdash\varphi</math> est un cône. On dit que <math>\varphi</math> est valide dans <math>\mathcal{M}</math> ou que <math>\mathcal{M}</math> modélise <math>\varphi</math>, noté <math>\mathcal{M}\vDash\varphi</math>, si pour <math>m\in\mathcal{U}_\mathcal{M}</math>, on a <math>m\Vdash\varphi</math>. On dit que <math>\varphi</math> est ''valide'', si pour tout modèle <math>\mathcal{M}</math>, <math>\mathcal{M}\vDash\varphi</math>. ====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, <math>\vdash\varphi</math> implique <math>\vDash\varphi</math>. 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 <math>\mathcal{N}\equiv\langle\{m_1,m_0\}, <, \mathcal{I}\rangle</math> avec <math>m_0<m_1</math> et <math>\mathcal{I}(p) = \{m_1\}</math> et <math>\mathcal{I}(q) = \emptyset</math>, on peut montrer que <math>m_0\not\Vdash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p</math>, donc <math>\mathcal{N}\not\vDash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p</math> et donc que <math>\not\vDash ((p\Rightarrow q)\Rightarrow p)\Rightarrow p</math>. 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 <math>((p\Rightarrow q)\Rightarrow r)\Rightarrow((q\Rightarrow p)\Rightarrow r)\Rightarrow r</math>. ====Complétude de la logique intuitionniste==== On peut démontrer que toute proposition ''valide'' est ''démontrable''. Formellement, <math>\vDash\varphi</math> implique <math>\vdash\varphi</math>. La démonstration se fait de la façon suivante: si <math>\varphi</math> n'est pas démontrable alors on peut construire un contre-modèle (infini) de <math>\varphi</math> c'est-à-dire un modèle <math>\mathcal{M}</math> tel que <math>\mathcal{M}\not\vDash\varphi</math>. ==Voir aussi== * [[Analyse constructive]] * [[Constructivisme (mathématiques)]] * [[Sémantique de Kripke]] {{Portail|mathématiques|philosophie|logique}} [[Catégorie:logique]] [[Catégorie:logique mathématique]] [[Catégorie:Théorie des types]] [[cs:Intuicionistická logika]] [[en:Intuitionistic logic]] [[it:Logica intuizionista]] [[ja:直観論理]] [[pl:Logika intuicjonistyczna]]