Brouwerova–Heytingova–Kolmogorovova interpretace

Brouwerova-Heytingova-Kolmogorovova interpretace nebo BHK interpretace je v matematické logice interpretace intuicionistické logiky, kterou navrhli Luitzen Egbertus Jan Brouwer a Arend Heyting, a nezávisle na nich Andrej Nikolajevič Kolmogorov. Díky spojení s teorií realizovatelnosti Stephena Kleeneho se někdy nazývá interpretace realizovatelnosti.

Interpretace

Interpretace stanovuje, co má být důkazem dané dobře utvořené formule. Důkaz se provede indukcí podle struktury této formule:

* Důkazem P \wedge Q je dvojice kde a je důkazem P a b je důkazem Q. * Důkazem P \vee Q je dvojice kde a je 0 a b je důkazem P, nebo a je 1 a b je důkazem Q. +more * Důkazem P \to Q je funkce f, která převádí důkaz P na důkaz Q. * Důkazem \exists x \in S : \varphi(x) je dvojice kde a je prvkem S, a b je důkazem \varphi(a). * Důkazem \forall x \in S : \varphi(x) je funkce f, která převádí prvek a množiny S na důkaz \varphi(a). * Formule \neg P je definována jako P \to \bot, takže důkazem je funkce f, která převádí důkaz P na důkaz \bot. * Neexistuje důkaz \bot (spor, nepravda nebo prázdný typ, neskončení výpočtu v některých programovacích jazycích).

Předpokládá se, že interpretace primitivního výroku je známá z kontextu. V kontextu aritmetiky je důkazem formule s=t výpočet redukující oba členy na stejné číslo.

Kolmogorov použil stejný postup, ale svou interpretaci vyjádřil pomocí problémů a řešení. Prohlásit, že formule je pravdivá, znamená, že známe řešení problému reprezentovaného touto formulí. +more Například P \to Q je problém redukce Q na P ; jeho řešení vyžaduje nějakou metodu řešení problému Q, známe-li řešení problému P.

Příklady

Identita je důkazem formule P \to P, pro jakékoli P.

Zásada sporu \neg (P \wedge \neg P) produkuje (P \wedge (P \to \bot)) \to \bot: * Důkazem (P \wedge (P \to \bot)) \to \bot je funkce f, která převádí důkaz (P \wedge (P \to \bot)) na důkaz \bot. * Důkazem (P \wedge (P \to \bot)) je dvojice důkazů , kde a je důkazem P, a b je důkazem P \to \bot. +more * Důkazem P \to \bot je funkce, která převádí důkaz P na důkaz \bot. Zkombinováním uvedeného dostaneme, že důkazem (P \wedge (P \to \bot)) \to \bot je funkce f, která převádí dvojici - kde a je důkazem P, a b je funkce, která převádí důkaz P na důkaz \bot - na důkaz \bot. Existuje funkce f, která provádí tento převod, kde f(\langle a, b \rangle) = b(a), neboli dokazuje zásadu sporu, pro jakékoli P.

Stejným způsobem lze také dokázat (P \wedge (P \to Q)) \to Q pro libovolný výrok Q.

Na druhou stranu, zákon o vyloučení třetího P \vee (\neg P) je převeden na P \vee (P \to \bot), což obecně nemá důkaz. Podle interpretace je důkazem P \vee (\neg P) dvojice kde a je 0 a b je důkaz P, nebo a je 1 a b je důkaz P \to \bot. +more Tedy pokud ani P ani P \to \bot není dokazatelné, pak není dokazatelné ani P \vee (\neg P).

Co je spor?

Obecně však není možné, aby logický systém měl formální operátor negace takový, že existuje důkaz "not" P právě tehdy, když neexistuje důkaz P ; viz Gödelovy věty o neúplnosti. BHK interpretace místo toho předpokládá, že "not" P znamená, že P vede ke sporu značenému \bot, takže důkaz ¬P je funkce převádějící důkaz P na důkaz sporu.

Standardní příklad sporu se objevuje při práci s aritmetikou. Za předpokladu, že 0 = 1, lze pomocí matematické indukce a axiomu rovnosti 0 = 0 dokázat, že libovolná dvě přirozená čísla jsou si rovna. +more Indukce hypotézy: kdyby 0 byla rovna určitému přirozenému číslu n, pak 1 by byla rovna n+1, (Peanův axiom: Sm = Sn právě tehdy když m = n), ale pokud by platilo 0=1, byla by 0 také byla rovna n + 1. Indukcí lze dokázat, že pak by se 0 rovnala všem číslům, a proto libovolná dvě přirozená čísla by si byla rovna.

Existuje tedy způsob, jak od důkazu 0=1 přejít k důkazu libovolné elementární aritmetické rovnosti, a tedy k důkazu libovolně složitého aritmetického tvrzení. Pro získání tohoto výsledku navíc nebylo nutné použít Peanův axiom, který říká, že 0 "není" následníkem žádného přirozeného čísla. +more Díky tomu lze v Heytingově aritmetice používat 0=1 jako \bot (a Peanův axiom lze přepsat jako 0 = Sn → 0 = S0). Toto použití 0 = 1 validuje princip exploze.

Co je funkce?

BHK interpretace závisí na názoru, jaká může být funkce, která převádí jeden důkaz na jiný, nebo která převádí prvek domény na důkaz. Různé verze konstruktivismu se v tomto ohledu liší.

Kleeneova teorie realizovatelnosti identifikuje funkce s vyčíslitelnými funkcemi. Používá Heytingovu aritmetiku, v níž doménou kvantifikace jsou přirozená čísla a primitivní výroky mají tvar x=y. +more Důkazem x=y je jednoduše triviální algoritmus ověřující, zda se x vyhodnotí na stejné číslo jako y (což je pro přirozená čísla vždy rozhodnutelné), jinak důkaz neexistuje. Toto tvrzení pak rozšíříme indukcí na složitější algoritmy.

Pokud za definici pojmu funkce považujeme lambda kalkul, pak BHK interpretace popisuje Curryho-Howardův isomorfismus mezi přirozenou dedukcí a funkcemi.

Odkazy

Reference

Související články

Peanovy axiomy

Kategorie:Funkcionální programování Kategorie:Teorie programovacích jazyků Kategorie:Konstruktivismus (matematika)