BHKinterpretasjonen

BHK-interprettasjonen, eller Brouwer–Heyting–Kolmogorov-tolkningen, er en forklaring av hva det betyr at en påstand i intuitionistisk logikk er sann. Den gir en konstruktiv mening til logiske forbindelser og kvantifikatorer, og bygger på ideen om at sannhet avhenger av å kunne gi et konstruktivt bevis, ikke bare av en sannhetsverdi som holdes av en meta-logisk regel.

Ifølge BHK-tolkningen er bevis for de enkelte konstruksjonene: P ∧ Q er bevis ved å presentere et bevis for P og et bevis for Q; P ∨ Q er bevis ved å gi et bevis av enten P eller Q, sammen med en indikasjon av hvilken disjunkt og hvilket bevis som er gitt; P → Q er bevis ved å gi en måte som konverterer hvert bevis for P til et bevis for Q; ¬P er definert som P → ⊥, hvor ⊥ representerer en motsetning eller absurde konsekvens; universell kvantifisering ∀x P(x) bevises ved å gi en metode som, for alle verdier a, gir et bevis av P(a); eksistensiell kvantifisering ∃x P(x) bevises ved å gi et konkret vitne a og et bevis av P(a).

BHK har hatt stor innflytelse på konstruktiv matematikk og logikk. Den ligger til grunn for Curry–Howard-korrespondansen mellom bevis og programmer, og den påvirker hvordan intuitionistisk logikk blir modellert i ulike formelle rammer, blant annet gjennom Kripke-semantikk og topos-teori. Litteraturen anerkjenner også at BHK er en intuitiv forklaringsmetode; formaliserte semantikker gir presisitet, men koblingen mellom bevis og mening forblir en kjerneidé i feltet.