Interprétation de Brouwer-Heyting-Kolmogorov

L'interprétation définit exactement ce qui est attendu d'une preuve d'une formule logique. Elle est spécifiée par induction sur la structure d'une formule donnée:

• Une preuve de ${\displaystyle P\wedge Q}$ est une paire <a, b> dans laquelle a est une preuve de P et b est une preuve de Q.
• Une preuve de ${\displaystyle P\vee Q}$ est une paire <a, b> où a est 0 et b est une preuve de P, ou alors a est 1 et b est une preuve de Q.
• Une preuve de ${\displaystyle P\to Q}$ est une fonction f qui transforme une preuve de P en une preuve de Q.
• Une preuve de ${\displaystyle \exists x\in S:\phi (x)}$ est une paire <a, b> où a est un élément de S, et b est une preuve de φ(a).
• Une preuve de ${\displaystyle \forall x\in S:\phi (x)}$ est une fonction f qui transforme un élément a de S en une preuve de φ(a).
• La formule ${\displaystyle \neg P}$ est définie comme ${\displaystyle P\to \bot }$, donc une de ses preuves est une fonction f qui transforme une preuve de P en une preuve de ${\displaystyle \bot }$.
• Il n'existe pas de preuve de ${\displaystyle \bot }$ (l'absurdité).

L'interprétation d'une formule élémentaire est supposée donnée par le contexte. Par exemple dans le contexte de l'arithmétique, une preuve de la formule s=t est le calcul réduisant les deux termes à un nombre identique.

Kolmogorov a suivi la même idée, mais en formulant son interprétation en termes de problème et de solutions. Affirmer la vérité d'une formule est affirmer connaître une solution du problème posé par cette formule. Par exemple ${\displaystyle P\to Q}$ est dans cette formulation le problème de réduire la résolution de P à la résolution de Q; le résoudre nécessite de trouver une méthode (ou un algorithme) permettant de trouver une solution au problème Q à partir d'une solution du problème P. C'est une démarche analogue à la réduction de la théorie de la complexité des algorithmes.

La fonction identité est une preuve de la formule ${\displaystyle P\to P}$, quel que soit P.

Le principe de non-contradiction ${\displaystyle \neg (P\wedge \neg P)}$ s'étend en ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$:

• Une preuve de ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ est une fonction f qui transforme une preuve de ${\displaystyle (P\wedge (P\to \bot ))}$ en une preuve de ${\displaystyle \bot }$.
• Une preuve de ${\displaystyle (P\wedge (P\to \bot ))}$ est une paire de preuves <a,b>, où a est une preuve de P, et b est une preuve de ${\displaystyle P\to \bot }$.
• Une preuve de ${\displaystyle P\to \bot }$ est une fonction qui transforme une preuve de P en une preuve de ${\displaystyle \bot }$.

Une preuve de ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ est donc une fonction f qui transforme une paire <a,b> – où a est une preuve de P, et b est une fonction qui transforme une preuve de P en une preuve de ${\displaystyle \bot }$ – en une preuve de ${\displaystyle \bot }$. La fonction ${\displaystyle f(\langle a,b\rangle )=b(a)}$ remplit ce contrat, et constitue donc une preuve de la loi de non contradiction quelle que soit la formule P.

Ce n'est pas le cas pour le principe du tiers exclu ${\displaystyle P\vee (\neg P)}$ formulée ${\displaystyle P\vee (P\to \bot )}$, qui ne peut pas se prouver dans le cas général. Selon l'interprétation, une preuve de ${\displaystyle P\vee (\neg P)}$ est une paire <a, b> où a est 0 et b est une preuve de P, ou où a est 1 et b est une preuve de ${\displaystyle P\to \bot }$. Par conséquent si ni P ni ${\displaystyle P\to \bot }$ ne sont prouvables, alors ${\displaystyle P\vee (\neg P)}$ ne le sera pas non plus.

Il n'est pas possible pour un système formel « suffisamment puissant », d'avoir un opérateur de négation tel qu'il y ait une preuve de ${\displaystyle \neg P}$ à chaque fois qu'il n'existe pas de preuve de ${\displaystyle P}$ ; voir le théorème d'incomplétude de Gödel. L'interprétation BHK en tient compte et définit ${\displaystyle \neg P}$ par ${\displaystyle P}$ entraîne l'absurdité, notée ${\displaystyle \bot }$. Une preuve de ${\displaystyle \neg P}$ est ainsi une fonction qui transforme une preuve de ${\displaystyle P}$ en une preuve de l'absurdité.

Supposons une absurdité arithmétique comme 0 = 1, et procédons par récurrence : 0 = 0 par l'axiome d'égalité. Si 0 était égal à un nombre naturel n, alors 1 serait égal à n+1, (par l'axiome de Peano, : Sm = Sn si et seulement si m = n), mais comme 0=1, 0 serait aussi égal à n + 1. Par récurrence, 0 est égal à tous les nombres, et par conséquent n'importe quelle paire de nombre deviennent égaux.

Par conséquent il existe une manière de passer d'une preuve de 0=1 à une preuve de n'importe quelle égalité arithmétique simple, et donc une preuve de n'importe quelle proposition arithmétique complexe. De plus, il n'a pas été nécessaire de prendre en compte l'axiome de Peano statuant que 0 n'est le successeur d'aucun nombre naturel. On peut donc choisir 0=1 comme formule ${\displaystyle \bot }$ dans l'arithmétique de Heyting - l'axiome de Peano s'exprimant alors 0 = Sn → 0 = S0. Cette utilisation de la formule 0 = 1 est compatible avec le principe d'explosion.

L'interprétation BHK dépend de la définition que l'on choisit pour la fonction qui transforme une preuve en une autre preuve, ou un élément d'un domaine en une preuve. Il en découle plusieurs variantes du constructivisme qui divergent sur ce point.

La théorie de la réalisabilité de Kleene identifie ces fonctions comme les fonctions calculables. Elle permet de donner une interprétation à l'arithmétique de Heyting (en), dans laquelle le domaine de quantification est l'ensemble des entiers naturels et les propositions élémentaires sont de la forme ${\displaystyle x=y}$. Une preuve de ${\displaystyle x=y}$ est simplement l'algorithme trivial qui vérifie si x et y s'évaluent au même nombre, dans le cas contraire il n'y a pas de preuve. Les autres preuves sont construites par induction sur ces algorithmes triviaux pour construire des algorithmes plus complexes.

Si on choisit le lambda calcul comme définition pour les fonctions, alors l'interprétation BHK décrit la correspondance de Curry-Howard entre la déduction naturelle et les fonctions.

• (en) Anne Sjerp Troelstra (en), « History of Constructivism in the Twentieth Century », sur http://staff.science.uva.nl/~anne/, 1991
• (en) Anne Sjerp Troelstra (en), « Constructivism and Proof Theory », sur http://staff.science.uva.nl/~anne/, 2003
• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Brouwer–Heyting–Kolmogorov interpretation » (voir la liste des auteurs).