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