Logique intuitionniste

La logique intuitionniste est une logique qui diffère de la logique classique par le fait que la notion de vérité est remplacée par la notion de preuve constructive. Une proposition telle que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'Euler-Mascheroni n'est pas rationnelle » n'est pas démontrée de manière constructive (intuitionniste) dans le cadre de nos connaissances mathématiques actuelles, car la tautologie classique « P ou non P » (tiers exclu) n'appartient pas à la logique intuitionniste. La logique intuitionniste établit, entre autres, un distinguo entre « être vrai » et « ne pas être faux » (formulation plus faible) car ¬¬P → P n'est pas non plus démontrable en logique intuitionniste.

Histoire 
L'intuitionnisme a d'abord été une position philosophique vis-à-vis des mathématiques proposée par le mathématicien hollandais Luitzen Egbertus Jan Brouwer comme une possibilité différant de l'approche dite classique ; cela l'a conduit à ne pas inclure certaines formes du raisonnement mathématique traditionnel, qu'il jugeait contre-intuitives :
 Le tiers exclu, qui consiste à dire qu'étant donnée une proposition , on a soit  ou alors non  ;
 L'existentiel non constructif. Brouwer veut que quand un mathématicien affirme il existe  tel que , il donne aussi un moyen de construire  qui satisfait .
Brouwer a prôné une mathématique qui rejetterait le tiers exclu et n'accepterait que lexistentiel 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.

Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting, ainsi que par Kurt Gödel et Andreï Kolmogorov.
L'interprétation de Brouwer-Heyting-Kolmogorov ou simplement interprétation BHK est essentiellement la mise en évidence du caractère constructif de l'implication intuitionniste : Quand un mathématicien intuitionniste affirme , il veut dire qu'il fournit un procédé de « construction » d'une démonstration de  à partir d'une démonstration de . Autrement dit, une preuve de  est une fonction qui transforme une preuve de  en une preuve de .

Cette interprétation calculatoire trouvera son aboutissement dans un des plus importants résultats de l'informatique théorique : la correspondance de Curry-Howard dont le leitmotiv est « prouver, c'est programmer ». Il y a isomorphisme entre les règles de déduction de la logique intuitionniste et les règles de typage du lambda-calcul.
En conséquence, une preuve d'une proposition  est assimilable à un (lambda-)terme de type .

Dès lors, la logique intuitionniste (couplée à la théorie des types) acquiert un statut prépondérant en logique et en informatique théorique, en faisant d'elle historiquement la première des logiques constructives.
Ce résultat fondateur engendrera de multiples travaux dérivés ; notamment son extension à la logique d'ordre supérieur qui nécessite l'emploi de types dépendants (le calcul des constructions, par exemple, est la base théorique du logiciel Coq qui est donc, à la fois, un assistant de preuves (constructives), et un outil de création de programmes certifiés).

 Syntaxe du langage de la logique intuitionniste 
La syntaxe de la logique intuitionniste propositionnelle est la même que pour la logique propositionnelle classique. La syntaxe de la logique intuitionniste du premier ordre est la même que la syntaxe de la logique classique du premier ordre.

 Syntaxe de la logique intuitionniste propositionnelle 

 Syntaxe de la logique intuitionniste du premier ordre 

 Non-interdéfinissabilité des opérateurs 
La négation peut se définir à partir de l'implication :  se définit comme . En logique propositionnelle classique, on peut définir la disjonction (le « ou ») à partir du « et » et de la négation grâce aux lois de Morgan. Par exemple,  peut se définir comme un raccourci d'écriture pour . En logique propositionnelle intuitionniste, ce n'est plus le cas et chaque opérateur a une interprétation spécifique (cf. tableau ci-dessus). De même, on ne peut pas définir  comme .

 Règles de déduction naturelle 

En logique intuitionniste, les connecteurs ne sont pas inter-définissables. C'est pourquoi nous allons donner des règles pour chaque connecteur binaire, pour le connecteur unaire qu'est la négation et pour le symbole ⊥ représentant le faux ou absurde. Nous donnons une (ou des) règle(s) d'élimination  et une (ou des) règle(s) d'introduction  pour chaque connecteur, typique de la déduction naturelle classique. En déduction naturelle,  se lit « de l'ensemble de propositions  on déduit la proposition  ».

 La logique implicative 
La logique minimale implicative a pour seul connecteur l'implication  . En déduction naturelle, ses règles, outre la règle axiome :

sont : 

où la lettre  désigne un ensemble fini de formules, et la notation  désigne , où  peut être ou non présent dans .

La règle  s'appelle la règle d'élimination de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses  on déduit  et si de plus de l'ensemble d'hypothèses  on déduit  alors de l'ensemble d'hypothèses  on déduit . L'élimination de l'implication est aussi appelée modus ponens.

La règle  s'appelle la règle d'introduction de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses  et de l'hypothèse  on déduit  alors de l'ensemble d'hypothèses  on déduit  ( peut appartenir ou ne pas appartenir à ).

La loi de Peirce  ou la proposition , qui sont des tautologies de la logique classique, ne sont pas démontrables dans ce système de déduction.
En lui ajoutant, par exemple la loi de Peirce, on obtient un système déductivement complet au sens de la logique classique pour les formules purement implicationnelles (voir ).

 La logique propositionnelle intuitionniste 
La logique intuitionniste comporte les règles de l'implication, de la logique minimale, plus les règles ci-dessous régissant les autres connecteurs. 
 L'absurde 
Le faux ou absurde, ⊥, est un connecteur zéro-aire, c'est-à-dire qui n'a pas de proposition en argument, il est régi par la règle : 

Cette règle est nommée principe d'explosion, ou en latin, ex falso quodlibet. Le principe d'explosion signifie que si un ensemble de propositions  conduit à l'absurde ⊥, alors de , on peut déduire n'importe quelle proposition .

 La négation 
Traditionnellement, on considère la négation  comme l'abréviation  et on ne donne donc pas habituellement de règles correspondant à la négation. Cependant on pourrait en donner, pour simplifier des démonstrations et elles seraient :

 

Il est à noter que ces règles pour la négation intuitionnistes sont plus faibles que celles de la négation classique, car pour exemple on ne peut pas y déduire  de .

 La conjonction 
Au connecteur  (conjonction), on associe deux règles d'élimination,  et , et une règle d'introduction.

où  se lit « A et B ».

 La disjonction 
Au connecteur  (disjonction), on associe une règle d'élimination et deux règles d'introduction :

.

On remarque que la règle d'''élimination de la disjonction est une règle tryadique : elle a trois prémisses.

 Le calcul des prédicats intuitionniste 
En plus des règles du calcul propositionnel intuitionniste, le calcul des prédicats intuitionniste contient de nouvelles règles d'introduction et d'élimination pour les quantificateurs « quel que soit » et « il existe ».

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 
 

 Le quantificateur existentiel 
 

 Sémantique de la logique intuitionniste 

 Modèles de Kripke 

On peut donner une sémantique à la logique intuitionniste qui est une sémantique de Kripke. Un modèle de Kripke  est un graphe où :
 les nœuds sont des mondes possibles. Selon Kripke, ces mondes représentent des contenus d'information fondés sur des preuves (). Chaque monde est muni d'une valuation classique : intuitivement, pour chaque variable propositionnelle p, p est vraie dans un monde si on a assez d'information pour prouver p et p est fausse sinon ;
 une relation d'accessibilité de préordre sur les mondes : une relation réflexive et transitive hiérarchise les mondes. Pour Kripke, un arc m → m' signifie que m' est dans le « futur » de m ;
 la valuation est telle que si une variable propositionnelle p est vraie dans m et que m' est dans le « futur » de m, p est aussi vraie dans m' (on ne perd pas d'information et donc on peut toujours prouver p).
La sémantique d'une formule est donné par rapport à un modèle de Kripke  et un monde désigné comme le monde courant . On parle alors de modèle de Kripke pointé . Dans certains ouvrages, on écrit alors  pour dire que la formule  est vraie dans . On dit aussi que  satisfait formule . Plus simplement, comme le modèle de Kripke  est fixé, on dit qu'un monde  satisfait une formule , ou que le monde  force une formule . La relation forçage de (ou de réalisabilité) est définie par induction structurelle par :
 le monde  force une variable propositionnelle  si  est vraie dans le monde m ;
 le monde  force  si  force  et  force  ;
 le monde  force  si  force  ou  force  ;
 le monde  force  si pour tout monde  accessible depuis , si  force  alors  force  (certains auteurs appellent l'ensemble des mondes accessibles depuis un monde un cône) ;
 le monde   force   (il s'agit de l'abréviation ) si pour tout monde   accessible depuis ,  ne force pas .
Une formule  est valide si pour tout monde  de tout modèle ,  force .

 Exemple 

Le tiers-exclu  n'est pas valide. Pour le voir, donnons un modèle de Kripke pointé qui ne satisfait pas . Considérons le modèle de Kripke dans la figure à droite. Ce modèle contient deux mondes possibles : l'un (celui de gauche) où  est faux, l'autre (celui de droite) où  est vrai.

Le monde de gauche est le monde pointé ou monde initial. Il ne satisfait pas le tiers exclu . En effet :

 d'une part, le monde initial ne force pas  (intuitivement,  n'est pas prouvé car  est fausse donc cela signifie que l'on n'a pas encore assez d'informations)
 d'autre part, le monde initial ne force pas . En effet, le monde de droite est accessible depuis le monde initial mais malheureusement il force . Cette situation signifie intuitivement qu'en fournissant un peu plus d'effort, on peut « gagner plus d'informations » et arriver dans le monde de droite et prouver .

Aussi :
  (loi de Peirce) n'est pas valide : le monde de gauche du modèle de Kripke à droite ne force pas  ;
  n'est pas valide.

 Correction de la logique intuitionniste 
La logique intuitionniste est correcte vis-à-vis des modèles de Kripke, c'est-à-dire que toute formule démontrable (par exemple avec les règles de déduction naturelle de la section précédente) est valide. On peut utiliser ce résultat pour montrer qu'une formule n'est pas démontrable en logique intuitionniste. Par exemple, comme le tiers-exclu  ou la loi de Peirce  ne sont pas valides, elles ne sont pas démontrables.

 Complétude de la logique intuitionniste 
Toute formule valide est démontrable. 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  contenant un monde qui ne force pas .

 Relations avec la logique classique 
 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.

 Quelques validités 
Le tableau suivant donne quelques validités de la logique intuitionniste.

En logique classique, les formules obtenues en remplaçant les implications par des équivalences sont des validités (le tableau contiendrait que des ✔).

 Négation 
On peut interpréter  comme : « Il est démontré que  est contradictoire ».

On dispose en logique intuitionniste du théorème suivant :
 
Cependant, on ne peut pas en conclure , car cette équivalence ne peut pas être prouvée en logique intuitionniste.

 Double négation 
On peut interpréter  comme : « Il est démontré qu’il est contradictoire d’affirmer que  est contradictoire », c'est-à-dire « Il est démontré que  n’est pas contradictoire ». Mais on ne peut pas en déduire que «  est démontrable ».

Le théorème :
 
peut être démontré en logique intuitionniste.
Mais la réciproque ne peut pas l'être. On n'a pas . L’expression  peut s’interpréter comme « d'une démonstration de , on peut construire une démonstration de  ». Mais le fait que  ne soit pas contradictoire n’est pas suffisant pour établir une démonstration de «  ».

À titre d'exemple, soit x un réel et  la proposition x est rationnel. Démontrer , c'est donner deux entiers a et b tels que x = a/b. Si  est contradictoire (et donc si on a ), c'est que x est non rationnel, ou irrationnel. Dire que l'on 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  est : on dispose d'une preuve de  et d'une preuve de  (comparable à ce qu’il en est en logique classique).

En logique intuitionniste, la proposition suivante est un théorème :
 
Mais contrairement à ce qu’il en serait en logique classique,  n’est seulement qu’une conséquence de , la réciproque étant fausse. En effet, supposer que  est contradictoire, est insuffisant en logique intuitionniste pour conclure si  seul l'est ou  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  est : on a une preuve de  ou une preuve de .

On dispose en logique intuitionniste du théorème suivant :
 
A et B s’excluent mutuellement et ne sont pas simultanément démontrables. Cette situation est comparable à ce qu’il en serait dans la logique classique de Boole et Karnaugh.

Par contre, le théorème suivant :
 
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  est : nous pouvons créer un objet  et prouver que . L'existence de x est ici effective ou constructive. Il ne s'agit pas d'une existence théorique d'un élément  vérifiant .

On dispose du théorème suivant :
 
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  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 :
 
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é , on soit capable d'exhiber explicitement un objet x invalidant , ce qui est rarement possible.

On peut aussi dire que, en logique intuitionniste, l'affirmation de  est l'affirmation de l'existence effective et constructible d'un objet x validant , alors que  n'en est que l'existence théorique, exprimant seulement qu'il est contradictoire que  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
 
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  ou prouver , ce qui n'est pas toujours possible.

Par exemple, en arithmétique munie de la logique intuitionniste (dite arithmétique de Heyting), l’expression  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  ou de prouver que . Cette situation correspond bien à ce 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  ne peut pas être reformulée en termes de disjonction  et que le quantificateur existentiel  ne peut pas être reformulé en termes de quantificateur universel  ; 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.

Les interprétations des expressions ne se font pas à l'aide de  et , mais grâce aux concepts Prouvable et Contradictoire.

 Plongement de la logique classique dans la logique intuitionniste 
Kurt Gödel a proposé une traduction de la logique classique dans la logique intuitionniste : la «  », qui  rend démontrable en logique intuitionniste toute formule démontrable en logique classique. Ainsi, en ce sens précis, la logique intuitionniste ne démontre pas moins que la logique classique.

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  de l'ensemble des formules dans l'ensemble des formules définie par :
 
 , pour une formule atomique  différente de ⊥
 
 
 
 
  ;

où  et  sont des formules quelconques et  est une formule ayant  comme paramètre ;

alors on a le théorème suivant :
 .
Où  est la déduction classique et  est la déduction intuitionniste.

 Traduction en logique modale classique 
La logique intuitionniste peut être traduite dans la logique modale classique S4 munie d'une modalité . La construction  se lit «  est prouvable ». La traduction est définie par :
  pour toute variable propositionnelle  ;
  ;
  ;
  ;
 .
Une formule  est valide en logique intuitionniste si et seulement si  est valide dans la logique modale S4' classique (c'est-à-dire valide sur les modèles de Kripke réflexifs et transitifs).

 Complexité algorithmique des problèmes de décision en logique intuitionniste 
Le problème de la décision de la satisfiabilité et le problème de la décision de la validité en logique propositionnelle intuitionniste sont PSPACE-complets. D'ailleurs, ils demeurent PSPACE-complets même si on restreint les formules à deux variables.

 Références 

 Annexes 
 Bibliographie 
 Ouvrages 
  
 Arend Heyting Les fondements des mathématiques, intuitionnisme, théorie de la démonstration, Gauthier-Villars, Nauwelaerts, 1955, 91 pages.
 Jean Largeault, L'Intuitionisme, Paris, Presses universitaires de France, 1992.
 René David, Karim Nour et Christophe Raffali, Introduction à la logique, Dunod, 2001.
 Jean-Yves Girard, Le point aveugle'', Tome I, Hermann, 2007.

Liens externes 
  ou sur arXiv https://arxiv.org/abs/1602.07608
 
  (sur la logique intuitionniste et l’interprétation de Brouwer-Heyting-Kolmogorov — interprétation BHK)
 Michel Lévy Preuve en logique intuitionniste propositionnelle

Articles connexes 
 Algèbre de Heyting
 Analyse constructive
 Constructivisme (mathématiques)
 Logique classique
 Logique de la prouvabilité
 Logique minimale
 Sémantique de Kripke

Intuitionnisme
Logique
Logique mathématique
Théorie des types
Théorie de la démonstration
Logique non classique