Brouwer-Heyting-Kolmogorovinterpretatie

In de wiskundige logica is de Brouwer-Heyting-Kolmogorovinterpretatie of BHK-interpretatie een theorie die de wiskundige stroming van het intuïtionisme onderbouwde. De BHK-interpretatie is opgesteld door L.E.J. Brouwer, Arend Heyting en Andrej Kolmogorov en wordt ook wel de realiseerbaarheidsinterpretatie genoemd, omdat de theorie sterk tegen de realiseerbaarheidstheorie van de Amerikaanse wiskundige Stephen Kleene aanleunt.

Interpretatie

De interpretatie geeft een bewijs van een gegeven logische formule. Dit wordt gespecifieerd door de structuurinductie van die formule:

• Een bewijs van $P\wedge Q$ is een paar $\langle a,b\rangle$ met $a$ een bewijs van $P$ en $b$ een bewijs van $Q$.
• Een bewijs van $P\vee Q$ is een paar $\langle a,b\rangle$ met $a$ gelijk aan 0 en $b$ een bewijs van $P$, ofwel is $a$ gelijk aan 1 en $b$ een bewijs van $Q$.
• Een bewijs van $P\to Q$ is een functie die een bewijs van $P$ omvormt naar een bewijs van $Q$.
• Een bewijs van $\exists x\in S:\phi (x)$ is een paar $\langle a,b\rangle$ met $a$ een element van $S$, en $b$ een bewijs van $\phi (a)$.
• Een bewijs van $\forall x\in S:\phi (x)$ is een functie f die een element $a$ van $S$ omzet naar een bewijs van $\phi (a)$.
• De formule $\neg P$ is gedefinieerd als $P\to \bot$. Bijgevolg is een bewijs ervan een functie die een bewijs van $P$ omzet naar een bewijs van $\bot$.
• Er bestaat geen bewijs van $\bot$ (het absurde).

Het wordt aangenomen dat de interpretatie van de primitieve proposities door de context bekend is. In de rekenkunde is de interpretatie van de formule $s=t$ bijvoorbeeld een berekening die beide kanten tot hetzelfde getal omrekent.

Kolmogorov volgde dezelfde hoofdlijnen maar formuleerde zijn interpretatie in de vorm van problemen en oplossingen. Een formule geldig maken staat dan gelijk aan beweren dat er een oplossing voor het probleem bekend is, die de formule representeert. Zo is $P\to Q$ het probleem van het reduceren van $Q$ tot $P$. Om dit op te lossen, is een methode nodig die een probleem $Q$ kan oplossen wanneer een oplossing voor het probleem $P$ is gegeven.

Voorbeelden

De identiteitsfunctie is steeds een bewijs van de formule $P\to P$, wat $P$ ook is.

De wet van de non-contradictie $\neg (P\wedge \neg P)$ wordt uitgebreid tot $(P\wedge (P\to \bot ))\to \bot$:

• Een bewijs van $(P\wedge (P\to \bot ))\to \bot$ is een functie die een bewijs van $(P\wedge (P\to \bot ))$ omzet naar een bewijs van $\bot$.
• Een bewijs van $(P\wedge (P\to \bot ))$ is een paar van bewijzen $\langle a,b\rangle$, met $a$ een bewijs van $P$ en $b$ een bewijs van $P\to \bot$.
• Een bewijs van $P\to \bot$ is een functie die een bewijs van $P$ omzet naar een bewijs van $\bot$.

Samengevat is een bewijs van $(P\wedge (P\to \bot ))\to \bot$ een functie $f$ die een paar $\langle a,b\rangle$ (waarbij $a$ een bewijs van $P$ en $b$ een functie die een bewijs van $P$ omzet naar een bewijs van $\bot$) omzet naar een bewijs van $\bot$. De functie $f(\langle a,b\rangle )=b(a)$ past hierin en bewijst de wet van de non-contradictie, wat $P$ ook is.

Tegenover deze wet staat de wet van de uitgesloten derde die $P\vee \neg P$ uitbreidt naar $P\vee (P\to \bot )$ en geen algemeen bewijs heeft. Volgens de interpretatie is een bewijs van $P\vee \neg P$ een paar $\langle a,b\rangle$ met $a$ gelijk aan 0 en $b$ een bewijs van $P$, of $a$ gelijk aan 1 en $b$ een bewijs van $P\to \bot$. Als dus $P$ noch $P\to \bot$ bewijsbaar zijn, dan is $P\vee \neg P$ dat ook niet. Hieruit volgt dat als $P$ noch $P\to \bot$ bewijsbaar is, hetzelfde geldt voor $P\vee \neg P$.