Brouwerova–Heytingova–Kolmogorovova interpretace

Z Wikipedie, otevřené encyklopedie
Skočit na navigaci Skočit na vyhledávání

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[editovat | editovat zdroj]

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 je dvojice <ab> kde a je důkazem a b je důkazem .
  • Důkazem je dvojice <a, b> kde a je 0 a b je důkazem , nebo a je 1 a b je důkazem .
  • Důkazem je funkce , která převádí důkaz na důkaz .
  • Důkazem je dvojice <a, b> kde a je prvkem S, a b je důkazem .
  • Důkazem je funkce , která převádí prvek a množiny S na důkaz .
  • Formule je definována jako , takže důkazem je funkce f, která převádí důkaz na důkaz .
  • Neexistuje důkaz (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í. Například 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[editovat | editovat zdroj]

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

Zásada sporu produkuje :

  • Důkazem je funkce , která převádí důkaz na důkaz .
  • Důkazem je dvojice důkazů <a,b>, kde je důkazem P, a je důkazem .
  • Důkazem je funkce, která převádí důkaz P na důkaz .

Zkombinováním uvedeného dostaneme, že důkazem je funkce , která převádí dvojici <a,b> – kde je důkazem P, a je funkce, která převádí důkaz P na důkaz – na důkaz . Existuje funkce , která provádí tento převod, kde , neboli dokazuje zásadu sporu, pro jakékoli .

Stejným způsobem lze také dokázat pro libovolný výrok .

Na druhou stranu, zákon o vyloučení třetího je převeden na , což obecně nemá důkaz. Podle interpretace je důkazem dvojice <ab> kde a je 0 a b je důkaz P, nebo a je 1 a b je důkaz . Tedy pokud ani ani není dokazatelné, pak není dokazatelné ani .

Co je spor?[editovat | editovat zdroj]

Obecně však není možné, aby logický systém měl formální operátor negace takový, že existuje důkaz "not" právě tehdy, když neexistuje důkaz  ; viz Gödelovy věty o neúplnosti. BHK interpretace místo toho předpokládá, že "not" znamená, že vede ke sporu značenému , takže důkaz ¬ je funkce převádějící důkaz 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. 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. Díky tomu lze v Heytingově aritmetice používat 0=1 jako (a Peanův axiom lze přepsat jako 0 = Sn → 0 = S0). Toto použití 0 = 1 validuje princip exploze.

Co je funkce?[editovat | editovat zdroj]

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. 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[editovat | editovat zdroj]

Reference[editovat | editovat zdroj]

V tomto článku byl použit překlad textu z článku Brouwer–Heyting–Kolmogorov interpretation na anglické Wikipedii.

  • TROELSTRA, A. History of Constructivism in the Twentieth Century. www.illc.uva.nl. 1991. Dostupné online. 
  • TROELSTRA, A. Constructivism and Proof Theory (draft). citeseerx.ist.psu.edu. 2003. Dostupné online. 

Související články[editovat | editovat zdroj]