Pour les articles homonymes, voir logique (homonymie).

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

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^[1].

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 « il existe ${\displaystyle x}$ tel que ${\displaystyle P(x)}$ », celui-ci donne aussi un moyen de construire ${\displaystyle x}$ qui satisfasse ${\displaystyle P(x)}$. 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 ${\displaystyle P}$, soit ${\displaystyle P}$ est vraie soit ${\displaystyle P}$ est fausse^[2] : Brouwer démontre qu'il n'est pas toujours possible de produire une construction prouvant que ${\displaystyle P}$ est vraie ou une construction prouvant que ${\displaystyle P}$ est fausse^[3].

Cette approche fut initialement vivement critiquée par des mathématiciens comme David Hilbert qui considérait que « enlever le principe du tiers exclu à un mathématicien équivaudrait à interdire l'usage du télescope à un astronome, ou celui de ses poings à un boxeur »^[4]. 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^[5].

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^[6]. Elle permet de dégager et d'étudier des règles de déduction valides pour les mathématiques intuitionnistes^[6]. Elle est formalisée et étudiée par Arend Heyting, élève de Brouwer, à partir de 1928^[6], mais aussi par Valery Glivenko^[7],[8]. 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^[9],[10]. Kurt Gödel contribue aussi à l'étude de la logique intuitionniste dans les années 1930^[11],[12].

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 « chaque théorème démontré par des méthodes idéalistes est un défi^[13] : il faut en trouver une version constructive et en donner une preuve constructive »^[14].

L'interprétation de Brouwer-Heyting-Kolmogorov ou simplement interprétation BHK met en évidence le caractère constructif de l'implication intuitionniste^[2] : quand un mathématicien intuitionniste affirme ${\displaystyle a\to b}$, il veut dire qu'il fournit un procédé de « construction » d'une démonstration de ${\displaystyle b}$ à partir d'une démonstration de ${\displaystyle a}$. Autrement dit, une preuve de ${\displaystyle a\to b}$ est une fonction qui transforme toute preuve de ${\displaystyle a}$ en preuve de ${\displaystyle b}$.

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 ${\displaystyle P}$ est assimilable à un (lambda-)terme de type ${\displaystyle P}$.

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^[15] ; 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és^[16].

Cette section a besoin d'être recyclée (confusion de concept).
Une réorganisation et une clarification du contenu sont nécessaires. Améliorez-la ou discutez des points à améliorer.

Par exemple, la démonstration d'une disjonction ${\displaystyle A\lor B}$ en logique intuitionniste est donnée soit par une démonstration de ${\displaystyle A}$, soit par une démonstration de ${\displaystyle B}$, en précisant de plus que c'est dans l'intention de démontrer ${\displaystyle A\lor B}$^[17]. Accepter la propriété de tiers exclu ${\displaystyle A\lor \lnot A}$ en logique intuitionniste aurait donc pour conséquence que pour tout énoncé ${\displaystyle A}$ des mathématiques intuitionnistes que développe Brouwer, on soit capable de fournir une démonstration de ${\displaystyle A}$ ou une démonstration de ${\displaystyle \lnot A}$. Or Brouwer a exhibé plusieurs contre exemples dans lesquels cette démonstration n'est pas produite^{[pas clair][18]} :

• contre exemple "faible"^[19]: 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"^[20] : l'affirmation « tout réel est rationnel ou irrationnel » 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 ${\displaystyle {\sqrt {2}}}$ est prouvable en logique intuitionniste.

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 (${\displaystyle \bot }$), négation (${\displaystyle \lnot }$), disjonction (${\displaystyle \lor }$), conjonction (${\displaystyle \land }$) et implication (${\displaystyle \Rightarrow }$) . Mais l'interprétation des propositions créées avec cette syntaxe est différente, comme le présente le tableau suivant^[1] :

Construction	Lecture intuitive en logique classique	Lecture intuitive en logique intuitionniste
${\displaystyle A}$	${\displaystyle A}$ est vraie	${\displaystyle A}$ est prouvable : on dispose d'une preuve de ${\displaystyle A}$
${\displaystyle A\lor B}$	${\displaystyle A}$ est vraie ou ${\displaystyle B}$ est vraie	${\displaystyle A}$ est prouvable ou ${\displaystyle B}$ est prouvable : on dispose d'une preuve de ${\displaystyle A}$ ou d'une preuve de ${\displaystyle B}$
${\displaystyle A\land B}$	${\displaystyle A}$ est vraie et ${\displaystyle B}$ est vraie	${\displaystyle A}$ est prouvable et ${\displaystyle B}$ est prouvable : on dispose d'une preuve de ${\displaystyle A}$ et d'une preuve de ${\displaystyle B}$
${\displaystyle \bot }$	Faux, absurde	Faux, absurde
${\displaystyle A\to B}$	Si ${\displaystyle A}$ est vraie alors ${\displaystyle B}$ est vraie	Si ${\displaystyle A}$ est prouvable alors ${\displaystyle B}$ est prouvable : on peut démontrer que toute preuve de ${\displaystyle A}$ induit une preuve de ${\displaystyle B}$
${\displaystyle \lnot A}$ (abréviation de ${\displaystyle A\to \bot }$)	${\displaystyle A}$ est fausse	${\displaystyle A}$ est contradictoire

La négation peut se définir dans les deux logiques à partir de l'implication : ${\displaystyle \lnot A}$ se définit comme ${\displaystyle A\to \bot }$^[21]. 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 ${\displaystyle (A\lor B)}$ peut se définir comme un raccourci d'écriture pour ${\displaystyle \lnot (\lnot A\land \lnot B)}$^[22]. 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 .

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 (${\displaystyle \exists }$), et universel (${\displaystyle \forall }$). Mais l'interprétation des propositions utilisant ces quantificateurs est différente, comme l'indique le tableau ci-dessous^[1] :

Construction	Lecture intuitive en logique classique	Lecture intuitive en logique intuitionniste
${\displaystyle \exists xA(x)}$	il existe un élément ${\displaystyle x}$ tel que ${\displaystyle A(x)}$ est vraie	on peut construire un élément ${\displaystyle x}$ tel que ${\displaystyle A(x)}$ est prouvable
${\displaystyle \forall xA(x)}$	pour tout élément ${\displaystyle x}$, ${\displaystyle A(x)}$ est vraie	en prenant un élément quelconque ${\displaystyle x}$, ${\displaystyle A(x)}$ 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 ${\displaystyle \exists xA(x)}$ comme ${\displaystyle \lnot \forall x\lnot A(x)}$^[23].

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 ${\displaystyle a}$ et ${\displaystyle b}$ tels que ${\displaystyle a^{b}}$ soit rationnel ». La démonstration usuelle en logique classique est très courte. On considère d'abord le nombre ${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$ : s'il est rationnel, le théorème est prouvé en prenant ${\displaystyle a=b={\sqrt {2}}}$. Si ce nombre n'est pas rationnel, alors, comme ${\displaystyle ({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2}$, on peut prendre ${\displaystyle a={\sqrt {2}}^{\sqrt {2}}}$ (qui est supposé irrationnel) et ${\displaystyle b={\sqrt {2}}}$, 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 ${\displaystyle (a,b)}$ envisagés est tel que ${\displaystyle a^{b}}$ soit rationnel^[24]. (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 ${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$ est transcendant, donc irrationnel^[25] : le couple réalisant la propriété annoncée par le théorème est donc ${\displaystyle a={\sqrt {2}}^{\sqrt {2}}}$ et ${\displaystyle b={\sqrt {2}}}$).

Le tableau suivant donne quelques validités (et invalidités) implicatives en logique intuitionniste, dont la justification est détaillée ensuite^[26].

Validités en logique intuitionniste	Explications pour ${\displaystyle \Rightarrow }$	Explications pour ${\displaystyle \Leftarrow }$
${\displaystyle A\Rightarrow \lnot \lnot A}$	✔ Si ${\displaystyle A}$ est prouvable, alors il est prouvé que ${\displaystyle A}$ n'est pas contradictoire.	✗ Par exemple, il est prouvé que « il pleut » n'est pas contradictoire (on n'obtient pas de contradiction en supposant « il pleut »). Pourtant, « il pleut » n'est pas prouvable, sauf si on sort et qu'on se fait mouiller.
${\displaystyle \lnot A\Leftrightarrow \lnot \lnot \lnot A}$	✔ Si ${\displaystyle A}$ est contradictoire, alors une preuve que ${\displaystyle A}$ n’est pas contradictoire donne une contradiction.	✔ Si on a une preuve que ${\displaystyle A}$ n’est pas contradictoire donne une contradiction, alors ${\displaystyle A}$ est contradictoire.
${\displaystyle (\lnot A)\lor (\lnot B)\Rightarrow \lnot (A\land B)}$	✔ Si ${\displaystyle A}$ est contradictoire ou ${\displaystyle B}$ est contradictoire, alors « ${\displaystyle A}$ et ${\displaystyle B}$ » est contradictoire.	✗ 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.
${\displaystyle \lnot (A\lor B)\Leftrightarrow (\lnot A)\land (\lnot B)}$	✔ Si on obtient une contradiction d'une preuve de ${\displaystyle A}$ ou d'une preuve de ${\displaystyle B}$, alors ${\displaystyle A}$ est contradictoire et ${\displaystyle B}$ est contradictoire.	✔ Si ${\displaystyle A}$ est contradictoire et ${\displaystyle B}$ est contradictoire, alors d'une preuve de ${\displaystyle A}$ ou d'une preuve de ${\displaystyle B}$, on obtient une contradiction.
${\displaystyle ((\lnot A)\lor B)\Rightarrow (A\Rightarrow B)}$	✔ Si ${\displaystyle A}$ est contradictoire ou alors ${\displaystyle B}$ est prouvable, alors si j'ai une preuve de ${\displaystyle A}$ (ce qui n'existe pas !), j'ai une preuve de ${\displaystyle B}$.	✗ Par exemple, je construis une preuve de « x>0 » qui utilise une preuve « x>1 ». Pourtant, « x>1 » n'est pas contradictoire et « x>0 » n'est pas prouvable.
${\displaystyle \lnot (\exists xA(x))\Leftrightarrow \forall x(\lnot A(x))}$	✔ Si « il existe ${\displaystyle x}$ tel que ${\displaystyle A(x)}$ » est contradictoire, alors pour tout ${\displaystyle x}$, ${\displaystyle A(x)}$ est contradictoire.	✔ Si pour tout ${\displaystyle x}$, ${\displaystyle A(x)}$ est contradictoire, alors « il existe ${\displaystyle x}$ tel que ${\displaystyle A(x)}$ » est contradictoire.
${\displaystyle \exists x(\lnot A(x))\Rightarrow \lnot (\forall xA(x))}$	✔ Si je peux construire un ${\displaystyle x}$ tel que ${\displaystyle A(x)}$ donne une contradiction, alors « pour tout ${\displaystyle x}$, ${\displaystyle A(x)}$ » est contradictoire.	✗ Par exemple, « pour tout ${\displaystyle x}$, ${\displaystyle x}$ est pauvre » est contradictoire (car je vois qu'il existe des richesses). Pourtant, je ne peux pas trouver un individu ${\displaystyle x}$ (riche) tel que ${\displaystyle x}$ est pauvre soit contradictoire.

En logique classique, les formules obtenues en remplaçant les implications par des équivalences sont toutes valides.

La négation de la proposition ${\displaystyle A}$, notée ${\displaystyle \lnot A}$, s'interprète en logique intuitionniste comme : « Il est démontré que ${\displaystyle A}$ est contradictoire ».

On dispose en logique intuitionniste du théorème suivant : ${\displaystyle \lnot A\Leftrightarrow \lnot \lnot \lnot A}$

Cependant, on ne peut pas, contrairement à ce qui est possible en logique classique, en conclure que ${\displaystyle A\Leftrightarrow \lnot \lnot A}$ (voir la double négation ci‑dessous).

On peut interpréter ${\displaystyle \lnot \lnot A}$ comme : « Il est démontré qu’il est contradictoire d’affirmer que ${\displaystyle A}$ est contradictoire », c'est-à-dire « Il est démontré que ${\displaystyle A}$ n’est pas contradictoire ». Mais on ne peut pas en déduire que « ${\displaystyle A}$ est démontrable ».

On dispose en logique intuitionniste du théorème suivant : ${\displaystyle A\Rightarrow \lnot \lnot A}$

Mais la réciproque (${\displaystyle \lnot \lnot A\Rightarrow A}$) n'est pas démontrable^[27]. L’expression ${\displaystyle A\Rightarrow \lnot \lnot A}$ peut s’interpréter comme « d'une démonstration de ${\displaystyle A}$, on peut construire une démonstration de ${\displaystyle \neg \neg A}$ ». Mais le fait que ${\displaystyle A}$ ne soit pas contradictoire n’est pas suffisant pour établir une démonstration de ${\displaystyle A}$.

À titre d'exemple, soit ${\displaystyle x}$ un réel et ${\displaystyle A}$ la proposition "${\displaystyle x}$ est rationnel". Démontrer ${\displaystyle A}$, c'est donner deux entiers ${\displaystyle a}$ et ${\displaystyle b}$ tels que ${\displaystyle x=a/b}$. Si ${\displaystyle A}$ est contradictoire (et donc si on a ${\displaystyle \lnot A}$), c'est que ${\displaystyle x}$ est non rationnel, ou irrationnel. Dire que l'on a ${\displaystyle \lnot \lnot A}$, c'est dire que supposer "${\displaystyle x}$ est irrationnel" conduit à une contradiction, et donc conclure que ${\displaystyle x}$ n'est pas irrationnel. Mais ce n'est pas suffisant pour établir l'existence effective de deux entiers ${\displaystyle a}$ et ${\displaystyle b}$ tels que ${\displaystyle 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.

L'interprétation de ${\displaystyle A\land B}$ est : on dispose d'une preuve de ${\displaystyle A}$ et d'une preuve de ${\displaystyle B}$ (comparable à ce qu’il en est en logique classique).

En logique intuitionniste, la proposition suivante est un théorème : ${\displaystyle (\lnot A)\lor (\lnot B)\Rightarrow \lnot (A\land B)}$

Mais contrairement à ce qu’il en serait en logique classique, ${\displaystyle \lnot (A\land B)}$ n’est qu’une conséquence de ${\displaystyle (\lnot A)\lor (\lnot B)}$, et la réciproque n'est pas démontrable. En effet, supposer que ${\displaystyle A\land B}$ est contradictoire est généralement insuffisant pour conclure si ${\displaystyle A}$ seul l'est ou ${\displaystyle B}$ seul ou s'ils le sont tous les deux : or la logique intuitionniste impose d'obtenir cette précision. 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.

L'interprétation de ${\displaystyle A\lor B}$ est : on a une preuve de ${\displaystyle A}$ ou une preuve de ${\displaystyle B}$.

On dispose en logique intuitionniste du théorème suivant :

• ${\displaystyle \lnot (A\lor B)\Leftrightarrow (\lnot A)\land (\lnot B)}$

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 :

• ${\displaystyle ((\lnot A)\lor B)\Rightarrow (A\Rightarrow B)}$

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.

L'interprétation de ${\displaystyle \exists xA(x)}$ est : nous pouvons créer un objet ${\displaystyle x}$ et prouver que ${\displaystyle A(x)}$. L'existence de ${\displaystyle x}$ est ici effective ou constructive. Il ne s'agit pas d'une existence théorique d'un élément ${\displaystyle x}$ vérifiant ${\displaystyle A(x)}$.

On dispose du théorème suivant :

• ${\displaystyle \lnot (\exists xA(x))\Leftrightarrow \forall x(\lnot A(x))}$

S’il n’existe pas de ${\displaystyle x}$ qui vérifie ${\displaystyle A(x)}$ alors pour tous les ${\displaystyle x}$ on ne vérifie pas ${\displaystyle 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.

L'interprétation de ${\displaystyle \forall xA(x)}$ est : on a une preuve que pour chaque ${\displaystyle x}$ appartenant à l’ensemble spécifié, on peut prouver ${\displaystyle A(x)}$ (comparable à ce qu’il en est en logique classique).

On dispose en logique intuitionniste du théorème suivant :

• ${\displaystyle \exists x(\lnot A(x))\Rightarrow \lnot (\forall xA(x))}$

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é ${\displaystyle A(x)}$, on soit capable d'exhiber explicitement un objet ${\displaystyle x}$ invalidant ${\displaystyle A(x)}$, ce qui est rarement possible.

On peut aussi dire que, en logique intuitionniste, l'affirmation de ${\displaystyle \exists xA(x)}$ est l'affirmation de l'existence effective et constructible d'un objet ${\displaystyle x}$ validant ${\displaystyle A(x)}$, alors que ${\displaystyle \lnot (\forall x\lnot A(x))}$ n'en est que l'existence théorique, exprimant seulement qu'il est contradictoire que ${\displaystyle A(x)}$ 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.

La proposition suivante

• ${\displaystyle A\lor \lnot A}$

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 ${\displaystyle A}$ ou prouver ${\displaystyle \lnot A}$, ce qui n'est pas toujours possible.

Par exemple, dans l'arithmétique dans le cadre de la logique intuitionniste (dite arithmétique de Heyting), l’expression ${\displaystyle (x=y\lor x\neq y)}$ 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 ${\displaystyle x=y}$ ou de prouver que ${\displaystyle x\neq y}$. 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.

En logique intuitionniste, les connecteurs ne sont pas inter-définissables^[28],[22]. C'est pourquoi il faut 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. Cette section donne les règles d'élimination ${\displaystyle (E)}$ et d'introduction ${\displaystyle (I)}$ pour chaque connecteur, typique de la déduction naturelle classique. En déduction naturelle, ${\displaystyle \Gamma \vdash \varphi }$ se lit « de l'ensemble de propositions ${\displaystyle \,\Gamma }$ on déduit la proposition ${\displaystyle \varphi }$ ».

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

${\displaystyle {\frac {}{\Gamma ,\varphi \vdash \varphi }}\quad ({\text{axiome}})}$

sont :

${\displaystyle {\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)}$

où la lettre ${\displaystyle \Gamma }$ désigne un ensemble fini de formules, et la notation ${\displaystyle \Gamma ,\varphi }$ désigne ${\displaystyle \Gamma \cup \{\varphi \}}$, où ${\displaystyle \varphi }$ peut être ou non présent dans ${\displaystyle \Gamma }$.

La règle ${\displaystyle (\Rightarrow E)}$ s'appelle la règle d'élimination de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses ${\displaystyle \Gamma }$ on déduit ${\displaystyle \varphi \Rightarrow \psi }$ et si de plus de l'ensemble d'hypothèses ${\displaystyle \Gamma }$ on déduit ${\displaystyle \varphi }$ alors de l'ensemble d'hypothèses ${\displaystyle \Gamma }$ on déduit ${\displaystyle \psi }$. L'élimination de l'implication est aussi appelée modus ponens.

La règle ${\displaystyle (\Rightarrow I)}$ s'appelle la règle d'introduction de l'implication. Elle se lit comme suit : si de l'ensemble d'hypothèses ${\displaystyle \Gamma }$ et de l'hypothèse ${\displaystyle \varphi }$ on déduit ${\displaystyle \psi }$ alors de l'ensemble d'hypothèses ${\displaystyle \Gamma }$ on déduit ${\displaystyle \varphi \Rightarrow \psi }$ (${\displaystyle \varphi }$ peut appartenir ou ne pas appartenir à ${\displaystyle \Gamma }$).

La loi de Peirce ${\displaystyle ((\varphi \Rightarrow \psi )\Rightarrow \varphi )\Rightarrow \varphi }$ ou la proposition ${\displaystyle ((\varphi \Rightarrow \psi )\Rightarrow \rho )\Rightarrow ((\psi \Rightarrow \varphi )\Rightarrow \rho )\Rightarrow \rho }$, 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, autrement dit en créant un nouvel axiome

${\displaystyle {\frac {}{\Gamma \vdash ((\varphi \Rightarrow \psi )\Rightarrow \varphi )\Rightarrow \varphi }}\quad ({\text{Peirce}})}$

on obtient un système qui démontre toutes les théorèmes purement implicationnels de la logique classique (voir Calcul propositionnel implicationnel (en)).

La logique intuitionniste comporte les règles de la logique minimale et en outre les règles ci-dessous régissant les autres connecteurs.

Le faux ou absurde, ⊥, est un connecteur d'arité nulle, c'est-à-dire qui n'a pas de proposition en argument. Il est régi par la règle :

${\displaystyle {\frac {\Gamma \vdash \bot }{\Gamma \vdash \varphi }}\qquad (\bot E)}$.

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 ${\displaystyle \varphi }$. Il n'y a pas de règle d'introduction correspondante.

Le vrai, ${\displaystyle \top }$, est également un connecteur d'arité nulle. Il n'a pas de règle d'élimination, mais vient avec la règle d'introduction suivante :

${\displaystyle {\frac {}{\Gamma \vdash \top }}\qquad (\top I)}$.

Traditionnellement, on considère la négation ${\displaystyle \neg \varphi }$ comme l'abréviation ${\displaystyle \varphi \Rightarrow \bot }$ 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 :

${\displaystyle {\frac {\Gamma \vdash \neg \varphi \quad \Gamma \vdash \varphi }{\Gamma \vdash \bot }}~(\neg E)\qquad \qquad {\frac {\Gamma ,\varphi \vdash \bot }{\Gamma \vdash \neg \varphi }}~(\neg I)}$.

Il est à noter que ces règles pour la négation intuitionnistes sont plus faibles que celles de la négation classique, car par exemple on ne peut pas déduire ${\displaystyle \varphi }$ de ${\displaystyle \neg \neg \varphi }$.

Au connecteur ${\displaystyle \land }$ (conjonction), on associe deux règles d'élimination, ${\displaystyle \land E_{1}}$ et ${\displaystyle \land E_{2}}$, et une règle d'introduction.

${\displaystyle {\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)}$.

Au connecteur ${\displaystyle \vee }$ (disjonction), on associe une règle d'élimination et deux règles d'introduction :

${\displaystyle {\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 : elle a trois prémisses.

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

Remarque : rappelons que ${\displaystyle A[t/x]}$ signifie le remplacement de toutes les occurrences librement substituables de la variable ${\displaystyle x}$ par le terme ${\displaystyle t}$ ; voir calcul des prédicats pour les notions de « variable », « terme », « substitution » et de « librement substituable ».

${\displaystyle {\frac {\Gamma ,A[t/x]\vdash B}{\Gamma ,\forall xA\vdash B}}(\forall E)}$ ${\displaystyle {\frac {\Gamma \vdash A}{\Gamma \vdash \forall xA}}(\forall I)}$

${\displaystyle {\frac {\Gamma \vdash A[t/x]}{\Gamma \vdash \exists xA}}(\exists E)}$ ${\displaystyle {\frac {\Gamma ,A\vdash B}{\Gamma ,\exists xA\vdash B}}(\exists I)}$

On peut donner une sémantique à la logique intuitionniste qui est une sémantique de Kripke. Un modèle de Kripke ${\displaystyle {\mathcal {M}}}$ est un graphe orienté où^[29] :

• les nœuds sont des mondes possibles. Selon Kripke, ces mondes représentent des contenus d'information fondés sur des preuves (evidential situations). 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^[30] ;
• 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)^[31].

La sémantique d'une formule est donnée par rapport à un modèle de Kripke ${\displaystyle {\mathcal {M}}}$ et un monde désigné comme le monde courant ${\displaystyle m}$. On parle alors de modèle de Kripke pointé ${\displaystyle ({\mathcal {M}},m)}$. Dans certains ouvrages, on écrit alors ${\displaystyle m\models _{\mathcal {M}}\varphi }$ pour dire que la formule ${\displaystyle \varphi }$ est vraie dans ${\displaystyle ({\mathcal {M}},m)}$. On dit aussi que ${\displaystyle ({\mathcal {M}},m)}$ satisfait formule ${\displaystyle \varphi }$. Plus simplement, comme le modèle de Kripke ${\displaystyle {\mathcal {M}}}$ est fixé, on dit qu'un monde ${\displaystyle m}$ satisfait une formule ${\displaystyle \varphi }$, ou que le monde ${\displaystyle m}$ force une formule ${\displaystyle \varphi }$^[29],[30]. La relation forçage de (ou de réalisabilité) est définie par induction structurelle par :

• le monde ${\displaystyle m}$ force une variable propositionnelle ${\displaystyle p}$ si ${\displaystyle p}$ est vraie dans le monde ${\displaystyle m}$ ;
• le monde ${\displaystyle m}$ force ${\displaystyle (\varphi \land \psi )}$ si ${\displaystyle m}$ force ${\displaystyle \varphi }$ et ${\displaystyle m}$ force ${\displaystyle \psi }$ ;
• le monde ${\displaystyle m}$ force ${\displaystyle (\varphi \lor \psi )}$ si ${\displaystyle m}$ force ${\displaystyle \varphi }$ ou ${\displaystyle m}$ force ${\displaystyle \psi }$ ;
• le monde ${\displaystyle m}$ force ${\displaystyle (\varphi \Rightarrow \psi )}$ si pour tout monde ${\displaystyle m'}$ accessible depuis ${\displaystyle m}$, si ${\displaystyle m'}$ force ${\displaystyle \varphi }$ alors ${\displaystyle m'}$ force ${\displaystyle \psi }$ ;
• le monde ${\displaystyle m}$ force ${\displaystyle \neg \varphi }$ (il s'agit de l'abréviation ${\displaystyle \varphi \Rightarrow \bot }$) si pour tout monde ${\displaystyle m'}$ accessible depuis ${\displaystyle m}$, ${\displaystyle m'}$ ne force pas ${\displaystyle \varphi }$.

Une formule ${\displaystyle \varphi }$ est valide si pour tout monde ${\displaystyle m}$ de tout modèle ${\displaystyle {\mathcal {M}}}$, ${\displaystyle m}$ force ${\displaystyle \varphi }$.

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

Le monde de gauche est le monde pointé ou monde initial. Il ne satisfait pas le tiers exclu ${\displaystyle (p\lor \lnot p)}$. En effet :

• d'une part, le monde initial ne force pas ${\displaystyle p}$ (intuitivement, ${\displaystyle p}$ n'est pas prouvé car ${\displaystyle p}$ est fausse donc cela signifie que l'on n'a pas encore assez d'informations)
• d'autre part, le monde initial ne force pas ${\displaystyle \lnot p}$. En effet, le monde de droite est accessible depuis le monde initial mais malheureusement il force ${\displaystyle p}$. 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 ${\displaystyle p}$.

Aussi :

• ${\displaystyle ((p\Rightarrow q)\Rightarrow p)\Rightarrow p}$ (loi de Peirce) n'est pas valide : le monde de gauche du modèle de Kripke à droite ne force pas ${\displaystyle ((p\Rightarrow q)\Rightarrow p)\Rightarrow p}$ ;
• ${\displaystyle ((p\Rightarrow q)\Rightarrow r)\Rightarrow ((q\Rightarrow p)\Rightarrow r)\Rightarrow r}$ n'est pas valide.

La logique intuitionniste est correcte vis-à-vis des modèles de Kripke^[32], 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 ${\displaystyle (p\lor \lnot p)}$ ou la loi de Peirce ${\displaystyle ((p\Rightarrow q)\Rightarrow p)\Rightarrow p}$ ne sont pas valides, elles ne sont pas démontrables.

Toute formule valide est démontrable^[33]. La démonstration se fait de la façon suivante : si ${\displaystyle \varphi }$ n'est pas démontrable alors on peut construire un contre-modèle (infini) de ${\displaystyle \varphi }$ c'est-à-dire un modèle ${\displaystyle {\mathcal {M}}}$ contenant un monde qui ne force pas ${\displaystyle \varphi }$.

Kurt Gödel a proposé une traduction de la logique classique dans la logique intuitionniste : la « non-non traduction (en) », 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 ${\displaystyle f}$ de l'ensemble des formules dans l'ensemble des formules définie par :

• ${\displaystyle f(\bot )=\bot }$ ;
• ${\displaystyle f(A)=\neg \neg A}$, pour une formule atomique ${\displaystyle A}$ différente de ⊥ ;
• ${\displaystyle f(A\land B)=f(A)\land f(B)}$ ;
• ${\displaystyle f(A\lor B)=\neg \left(\neg f(A)\land \neg f(B)\right)}$ ;
• ${\displaystyle f(A\Rightarrow B)=f(A)\Rightarrow f(B)}$ ;
• ${\displaystyle f(\forall xP(x))=\forall xf(P(x))}$ ;
• ${\displaystyle f(\exists xP(x))=\neg (\forall x\neg f(P(x))}$ ;

où ${\displaystyle A}$ et ${\displaystyle B}$ sont des formules quelconques et ${\displaystyle P}$ est une formule ayant ${\displaystyle x}$ comme paramètre.

Alors on a le théorème suivant :

${\displaystyle \Gamma \vdash _{c}A\Leftrightarrow f(\Gamma )\vdash _{i}f(A)}$.

Où ${\displaystyle \vdash _{c}}$ est la déduction classique et ${\displaystyle \vdash _{i}}$ est la déduction intuitionniste.

La logique intuitionniste peut être traduite dans la logique modale classique S4^[34] munie d'une modalité ${\displaystyle \Box }$. La construction ${\displaystyle \Box A}$ se lit « ${\displaystyle A}$ est prouvable »^[35]. La traduction est définie par :

• ${\displaystyle T(p)=\Box p}$ pour toute variable propositionnelle ${\displaystyle p}$ ;
• ${\displaystyle T(\bot _{i})=\bot _{c}}$ ;
• ${\displaystyle T(A\land _{i}B)=T(A)\land _{c}T(B)}$ ;
• ${\displaystyle T(A\lor _{i}B)=T(A)\lor _{c}T(B)}$ ;
• ${\displaystyle T(A\to _{i}B)=\Box (T(A)\to _{c}T(B))}$.

Une formule ${\displaystyle A}$ est valide en logique intuitionniste si et seulement si ${\displaystyle T(A)}$ est valide dans la logique modale S4 classique (c'est-à-dire valide sur les modèles de Kripke réflexifs et transitifs).

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^[36]. D'ailleurs, ils demeurent PSPACE-complets même si on restreint les formules à deux variables^[37].

• René David, Karim Nour et Christophe Raffalli, Introduction à la logique : Théorie de la démonstration, cours et exercices corrigés, Paris, Dunod, 2001, 332 p. (ISBN 978-2-100-04892-2). 
• Jean-Yves Girard, Le point aveugle, Tome I, Hermann, 2007.
• Arend Heyting Les fondements des mathématiques, intuitionnisme, théorie de la démonstration, Gauthier-Villars, Nauwelaerts, 1955, 91 pages.
• Arend Heyting, « La conception intuitionniste de la logique », Les études philosophiques, PUF, vol. 11, n^o 2,‎ 1956, p. 226-233 (lire en ligne [PDF]). 
• Jean Largeault, Intuitionisme et théorie de la démonstration, Paris, J. Vrin, 1992, 566 p. (ISBN 2-7116-1059-4, présentation en ligne)
  Textes de Bernays, Brouwer, Gentzen, Gödel, Hilbert, Kreisel et Weyl réunis, traduits et présentés par Jean Largeault.
• Jean Largeault, L'Intuitionisme, Paris, Presses universitaires de France, 1992.

• (en) Errett Bishop, Foundations of constructive analysis, New York, Mc Graw-Hill, 1967, 392 p. (lire en ligne)
• (en) A. G. Dragalin (trad. Ben Silver), Mathematical Intuitionism : Introduction to Proof Theory, vol. 67, Rhode Island, American Mathematical Society, coll. « Translations of Mathematical Monographs », 1988, 244 p. (ISBN 0-8218-4520-9, lire en ligne). 
• (en) Michael Dummett, Elements of Intuitionism, Oxford, Clarendon Press, 1977, 488 p. (ISBN 0198531583, lire en ligne)
• (en) S. A. Kripke, « Semantical Analysis of Intuitionistic Logic I », Studies in Logic, Amsterdam, North-Holland Publishing « Formal Systems and Recursive Functions »,‎ 1965, p. 92-130 (lire en ligne, consulté le 15 juin 2025). 
• (en) Dirk Van Dalen, Logic and Structure : fourth edition, Berlin, Springer, 2008, 275 p. (ISBN 978-3-540-20879-2, lire en ligne). 
• (en) Jean van Heijenoort, From Frege to Gödel : A Source Book in Mathematical Logic 1879-1931, Massachussets, Harvard University Press, 1967, 680 p. (lire en ligne). 

• Richard Moot et Christian Retoré, « La "non-non" traduction de Gödel-Kolmogorov », Université Bordeaux-I, 2007 ou sur arXiv https://arxiv.org/abs/1602.07608
• Étienne Lozes, « TD non non traduction », Laboratoire Spécification et Vérification — ENS Cachan, 2009
• Alexandre Miquel, « Réalisabilité et extraction de programmes », Laboratoire Preuves, Programmes et Systèmes (PPS) de Jussieu, 2005 (sur la logique intuitionniste et l’interprétation de Brouwer-Heyting-Kolmogorov — interprétation BHK)
• Michel Lévy Preuve en logique intuitionniste propositionnelle

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

• Portail de la philosophie
• Portail de la logique