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.