Brouwerova–Heytingova–Kolmogorovova interpretace

logická 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

editovat

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

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

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

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.

Reference

editovat

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