Brouwer-Heyting-Kolmogorovinterpretatie

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

In de wiskundige logica is de Brouwer-Heyting-Kolmogorovinterpretatie of BHK-interpretatie een logische 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 hij sterk aanleunt bij de realiseerbaarheidstheorie van de Amerikaanse wiskundige Stephen Kleene.

De interpretatie[bewerken]

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).

Van de interpretatie van primitieve proposities wordt verondersteld vanuit de context gekend te zijn. In de context van de rekenkunde is een bewijs van de forume een computatie die beide termen 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 men een oplossing kent voor het probleem dat 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 gegeven is.

Voorbeelden[bewerken]

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 .