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 P \wedge Q is een paar <ab> met a een bewijs van P en b een bewijs van Q.
  • Een bewijs van P \vee Q is een paar <a, b> 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 f die een bewijs van P omvormt naar een bewijs van Q.
  • Een bewijs van \exists x \in S : \phi(x) is een paar <a, b> met a een element van S, en b een bewijs van φ(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 φ(a).
  • De formule \neg P is gedefinieerd als P \to \bot. Bijgevolg is een bewijs ervan een functie f die een bewijs van P omzet naar een bewijs van \bot.
  • Er bestaat geen bewijs van \bot (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 s=t een computatie die beide termen tot hetzelfde getal.

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 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 gegeven is.

Voorbeelden[bewerken]

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 f 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 <a,b>, 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 <a,b> - met 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 <ab> met a gelijk aan 0 en b een bewijs van P, ofa gelijk aan 1 en b een bewijs van P \to \bot. Thus if neither P nor P \to \bot is provable then neither is P \vee (\neg P). Hieruit volgt dat als P noch P \to \bot bewijsbaar is, hetzelfde geldt voor P \vee (\neg P).

Bronnen, noten en/of referenties

Dit artikel of een eerdere versie ervan is (gedeeltelijk) vertaald vanaf de Engelstalige Wikipedia, die onder de licentie Creative Commons Naamsvermelding/Gelijk delen valt. Zie de bewerkingsgeschiedenis aldaar.