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  is een paar  met  een bewijs van  en  een bewijs van .
 Een bewijs van  is een paar  met  gelijk aan 0 en  een bewijs van , ofwel is  gelijk aan 1 en  een bewijs van .
 Een bewijs van  is een functie die een bewijs van  omvormt naar een bewijs van .
 Een bewijs van  is een paar  met  een element van , en  een bewijs van .
 Een bewijs van  is een functie f die een element  van  omzet naar een bewijs van .
 De formule  is gedefinieerd als . Bijgevolg is een bewijs ervan een functie die een bewijs van  omzet naar een bewijs van .
 Er bestaat geen bewijs van  (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  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  het probleem van het reduceren van  tot . Om dit op te lossen, is een methode nodig die een probleem  kan oplossen wanneer een oplossing voor het probleem  is gegeven.

Voorbeelden 
De identiteitsfunctie is steeds een bewijs van de formule , wat  ook is. 

De wet van de non-contradictie  wordt uitgebreid tot : 
 Een bewijs van  is een functie die een bewijs van  omzet naar een bewijs van .
 Een bewijs van  is een paar van bewijzen , met  een bewijs van  en  een bewijs van .
 Een bewijs van  is een functie die een bewijs van  omzet naar een bewijs van . 

Samengevat is een bewijs van  een functie  die een paar  (waarbij  een bewijs van  en  een functie die een bewijs van  omzet naar een bewijs van ) omzet naar een bewijs van . De functie  past hierin en bewijst de wet van de non-contradictie, wat  ook is. 

Tegenover deze wet staat de wet van de uitgesloten derde die  uitbreidt naar  en geen algemeen bewijs heeft. Volgens de interpretatie is een bewijs van  een paar  met  gelijk aan 0 en  een bewijs van , of  gelijk aan 1 en  een bewijs van . Als dus  noch  bewijsbaar zijn, dan is  dat ook niet. Hieruit volgt dat als  noch  bewijsbaar is, hetzelfde geldt voor . 

Wiskundige logica