vignette|Le rejet du tiers exclu en logique intuitionniste : prouver qu'il est contradictoire d'affirmer que la proposition A est contradictoire ne suffit pas à prouver A. La logique intuitionniste est une logique qui diffère de la logique classique par le fait que toute affirmation doit être démontrable par une preuve constructive. Cette logique rejette le principe classique de tiers exclu, selon lequel « P ou non P » est toujours vrai, ainsi que les démonstrations par l'absurde. La logique intuitionniste considère notamment que la proposition « ne pas être faux » n'est pas équivalente à la proposition « être vrai » et, d'autre part, elle n'accepte une preuve d'existence d'un objet mathématique satisfaisant une propriété que si elle fournit une méthode effective de construction de l'objet en question. Certaines affirmations et démonstrations, valides en logique classique ne le sont donc pas en logique intuitionniste. Par exemple, la proposition « tout nombre réel est soit rationnel, soit irrationnel », trivialement vraie en logique classique, n'est pas prouvable en logique intuitionniste.
Développée à partir de la fin des années 1910 par les mathématiciens néerlandais Luitzen Egbertus Jan Brouwer et Arend Heyting, la logique intuitionniste a eu une influence importante sur le développement des logiques constructives puis de l'informatique théorique.
Histoire
L'intuitionnisme en mathématique est issu d'une position philosophique vis-à-vis des mathématiques proposée par le mathématicien néerlandais Luitzen Egbertus Jan Brouwer comme une critique de l'approche dite classique. vignette|256x256px|Luitzen Egbertus Jan Brouwer en 1932. Brouwer rejette la notion d'infini actuel, et n'accepte que celle d'infini potentiel. Il rejette également la notion d'existentiel non constructif : il exige que quand un mathématicien affirme , celui-ci donne aussi un moyen de construire qui satisfasse . Cela l'a conduit à rejeter certaines formes du raisonnement mathématique traditionnel, notamment celles posant en axiome le principe du tiers exclu, qui consiste à dire qu'étant donnée une proposition , soit est vraie soit est fausse : Brouwer démontre qu'il n'est pas toujours possible de produire une construction prouvant que est vraie ou une construction prouvant que est fausse.
Cette approche fut initialement vivement critiquée par des mathématiciens comme David Hilbert qui considérait que . Hilbert s'inquiétait notamment des dégâts que pourrait causer cette approche aux fondements mêmes des mathématiques, alors qu'elle n'avait produit que très peu de résultats et restait incomplète. D'autres mathématiciens, en particulier Hermann Weyl, élève et disciple de Hilbert, y ont souscrit dès les années 1920.
Pour Brouwer, la logique n'est pas première vis-à-vis des mathématiques, la logique intuitionniste résulte de l'application des principes de l'intuitionnisme et des mathématiques intuitionnistes au langage, préambule.. Elle permet de dégager et d'étudier des règles de déduction valides pour les mathématiques intuitionnistes. Elle est formalisée et étudiée par Arend Heyting, élève de Brouwer, à partir de 1928, mais aussi par Valery Glivenko, 4.3 Glivenko 1928 and 1929.Glivenko, V., 1928, « Sur la logique de M. Brouwer », Académie Royale de Belgique, Bulletin de la classe des sciences, 14: 225–228.. Andreï Kolmogorov avait déjà entamé cette formalisation dès 1925, mais son travail était alors resté largement ignoré hors de l'Union Soviétique, Kolmogorov 1925.. Kurt Gödel contribue aussi à l'étude de la logique intuitionniste dans les années 1930, 4.5.1 Some early results.Kurt Godel, , Vol. III, (1995)..
Parmi les compléments ayant progressivement enrichi l'intuitionnisme, on peut noter la reconstruction formelle des nombres (entiers, relatifs puis réels), et la reformulation ainsi que la démonstration constructive de nombreux théorèmes de la logique classique. Bishop considérait d'ailleurs que pour tout mathématicien intuitionniste .
L'interprétation de Brouwer-Heyting-Kolmogorov ou simplement interprétation BHK met en évidence le 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 toute preuve de en 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 Rocq qui est donc, à la fois, un assistant de preuves (constructives), et un outil de création de programmes certifiésIl faut comprendre par là, que lorsque le programmeur construit une fonction dont il aura spécifié le type des arguments et du résultat, il s'astreint à respecter cette spécification puisqu'il doit fournir un objet correctement typé. Les types dépendants offrent une typage plus puissant que la plupart des langages, et permettent la spécification complète d'un programme..
Notion de preuve et refus de l'axiome du tiers exclu
Par exemple, la démonstration d'une disjonction en logique intuitionniste est donnée soit par une démonstration de , soit par une démonstration de , en précisant de plus que c'est dans l'intention de démontrer . Accepter la propriété de tiers exclu en logique intuitionniste aurait donc pour conséquence que pour tout énoncé des mathématiques intuitionnistes que développe Brouwer, on soit capable de fournir une démonstration de ou une démonstration de . :
contre exemple "faible": dans l'état actuel des connaissances mathématiques, on ne sait pas si la conjecture de Goldbach, selon laquelle tout nombre pair égal ou supérieur à 4 est la somme de deux nombres premiers, est vraie ou fausse. Ceci ne veut pas dire qu'on ne pourra jamais savoir si cette conjecture est vraie ou fausse, mais qu'on ne peut, à ce jour, rien affirmer à ce sujet ; contre exemple "fort" : l'affirmation ne peut être prouvée en logique intuitionniste. Dans ce cas, on sait qu'il ne sera jamais possible de trouver un processus opératoire permettant de démontrer, pour un nombre réel quelconque, qu'il est rationnel ou qu'il est irrationnel. Ceci ne veut pas dire que cette démonstration n'existe pas pour certains réels : ainsi, par exemple, l'irrationnalité de est prouvable en logique intuitionniste.
La logique intuitionniste à la base des circuits synchrones La conception de circuits synchrones cycliques corrects (c'est-à-dire qui se stabilisent et n'oscillent pas) correspond exactement à ceux qui sont prouvés par la logique intuitionniste, comme l'explique Gérard Berry dans son cours au Collège de France et qu'il résume par la formule
La stabilité électrique avec délais est équivalente à la preuve intuitionniste des circuits sans délais.
Syntaxe du langage de la logique intuitionniste Syntaxe de la logique intuitionniste propositionnelle La syntaxe de la logique intuitionniste propositionnelle est la même que celle de la logique propositionnelle classique. La logique intuitionniste utilise notamment les mêmes connecteurs logiques que la logique classique : faux/absurde (), négation (), disjonction (), conjonction () et implication () . Mais l'interprétation des propositions créées avec cette syntaxe est différente, comme le présente le tableau suivant : ConstructionLecture intuitive en logique classiqueLecture intuitive en logique intuitionniste est vraie est prouvable : on dispose d'une preuve de est vraie ou est vraie est prouvable ou est prouvable : on dispose d'une preuve de ou d'une preuve de est vraie et est vraie est prouvable et est prouvable : on dispose d'une preuve de et d'une preuve de Faux, absurdeFaux, absurdeSi est vraie alors est vraieSi est prouvable alors est prouvable : on peut démontrer que toute preuve de induit une preuve de (abréviation de ) est fausse est contradictoire La négation peut se définir dans les deux logiques à partir de l'implication : se définit comme . En outre, en logique propositionnelle classique, la disjonction (le « ou ») peut être définie à partir du « et » et de la négation grâce aux lois de 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 : on dit que ces opérateurs ne sont pas inter-définissables .
Syntaxe de la logique intuitionniste du premier ordre La syntaxe de la logique intuitionniste du premier ordre est la même que celle de la logique classique du premier ordre. La logique intuitionniste utilise notamment les deux mêmes quantificateurs : existentiel (), et universel (). Mais l'interprétation des propositions utilisant ces quantificateurs est différente, comme l'indique le tableau ci-dessous : ConstructionLecture intuitive en logique classiqueLecture intuitive en logique intuitionnisteil existe un élément tel que est vraieon peut construire un élément tel que est prouvablepour tout élément , est vraieen prenant un élément quelconque , est prouvable Ces deux quantificateurs n'ont en outre pas la même relation qu'en logique classique. Par exemple, en logique intuitionniste, on ne peut pas définir comme , Exercice 29 ..
Un exemple est fréquemment cité dans les ouvrages spécialisés pour illustrer la différence de la notion d'existence entre logique classique et logique intuitionniste. Il s'agit de la démonstration du théorème suivant : « il existe deux réels irrationnels et tels que soit rationnel ». La démonstration usuelle en logique classique est très courte. On considère d'abord le nombre : s'il est rationnel, le théorème est prouvé en prenant . Si ce nombre n'est pas rationnel, alors, comme , on peut prendre (qui est supposé irrationnel) et , et le théorème est démontré en logique classique. Mais il ne l'est pas en logique intuitionniste car cette démonstration ne permet pas de désigner celui des deux couples de réels envisagés est tel que soit rationnel. (En fait, il existe bien une démonstration qui, faisant appel au théorème de Gelfond-Schneider et acceptable en logique intuitionniste, montre que est transcendant, donc irrationnel : le couple réalisant la propriété annoncée par le théorème est donc et ).
Exemples de différences avec la logique classique
Validité de certaines implications Le tableau suivant donne quelques validités (et invalidités) implicatives en logique intuitionniste, dont la justification est détaillée ensuite.