Intuicionistická logika a Curry–Howardova korešpondencia

Základné pojmy

Intuicionistická logika, môže byť stručne opísaná ako klasická logika bez:

• Aristotelovho pravidla vylúčenia tretieho $(φ \lor \neg φ)$,
• zákonu dvojitej negácie $¬¬φ ≡ φ$.

Intuicionizmus je filozofický a matematický prístup, ktorý sa zameriava na konštruktívny postup v matematike a tvrdí, že matematické objekty musia byť skutočne skonštruované, nie iba abstraktne definované. Intuicionisti odmietajú princípy klasického deduktívneho dôkazu, ktorý sa vychádza zo zákona vylúčenia tretieho, ktorý hovorí, že ak existuje nejaké tvrdenie, tak je buď pravdivé alebo nepravdivé.

Konštruktívny dôkaz je druh matematického dôkazu, ktorý dokazuje existenciu matematického objektu tým, že ukáže spôsob, ako tento objekt skutočne skonštruovať. Tento prístup k matematickému dôkazu sa líši od tradičného dôkazu, ktorý iba dokazuje existenciu objektu bez skutočnej konštrukcie.

Jazyk intuicionistickej logiky

Jazyk intuicionistickej logiky je rovnaký ako jazyk výrokovej logiky, avšak logické spojky intuicionistickej logiky nie sú definované rovnakým spôsobom ako v klasickej logike.

Syntax intuicionistickej logiky v BNF

Je definovaná produkčným pravidlom v Backus-Naurovej forme, prostredníctvom ktorého je možné konštruovať všetky prípustné tvary formúl: $$ \varphi ::= p \mid \top \mid \bot \mid \neg\varphi \mid \varphi \land \psi \mid \varphi \lor \psi \mid \varphi \Rightarrow \psi, $$ kde p je množina atomických výrokov. Platí rovnaká priorita a asociativita operátorov ako vo výrokovej logike.

Vlastnosti syntaxe intuicionistickej logiky

Žiadnu zo základných logických spojok nemožno vyjadriť pomocou ostatných a preto je nutná prítomnosť všetkých štyroch.

• Negácia je definovaná ako implikácia do absurda $\neg φ ≡ φ ⇒ ⊥$.
• Ekvivalencia $\Leftrightarrow$ nie je považovaná za základnú spojku, ale rovnako ako v klasickej výrokovej logike za konjunkciu dvoch implikácií.

Mnoho tautológii klasickej logiky neplatí v intuicionistickej logike. To zahŕňa nielen zákon vylúčenia tretieho či eliminácie dvojitej negácie, ale tiež Peirceové pravidlo $(((φ \Rightarrow ψ) \Rightarrow φ) \Rightarrow φ)$. Pretože nie všetky tautológie klasickej logiky sú teorémy intuicionistickej logiky, ale všetky teorémy intuicionistickej logiky platia v klasickej, je možné sa na intuicionistickú logiku pozerať ako na oslabenie klasickej logiky, avšak s mnohými užitočnými vlastnosťami.

Sémantika intuicionistickej logiky

Z dôvodu, že intuicionistická logika vynecháva niektoré vyššie spomenuté zákony, má táto logika širší rozsah sémantických interpretácií.

Brouwer-Heyting-Kolmogorova interpretácia sémantiky intuicionistickej logiky

Neformálna interpretácia sémantiky intuicionistickej logiky. Význam logických spojok je definovaný BHK podmienkami:

• Konštruktívny dôkaz $φ ∧ ψ$ pozostáva z konštruktívneho dôkazu $φ$ a z konštruktívneho dôkazu $ψ$.
• Konštruktívny dôkaz $φ ∨ ψ$ pozostáva buď z konštruktívneho dôkazu $φ$ alebo z konštruktívneho dôkazu $ψ$.
• Absurdum $⊥$ nemá konštruktívny dôkaz.
• Vérum $⊤$ je konštruktívny dôkaz formuly $⊤$.
• Konštruktívny dôkaz $φ ⇒ ψ$ pozostáva z konštrukcie, ktorá každý konštruktívny dôkaz $φ$ prevedie na konštruktívny dôkaz $ψ$.
• Konštruktívny dôkaz $¬φ$ pozostáva z konštrukcie, ktorá každý konštruktívny dôkaz $φ$ prevedie na absurdum $⊥$ (negácia je chápaná ako $φ ⇒ ⊥$).

Kripkeho sémantika možných svetov

Formálne možno definovať sémantiku intuicionistickej logiky prostredníctvom relatívne novej metódy, ktorú definoval Saul Kripke. Táto metóda sa niekedy označuje ako sémantika možných svetov alebo prosto Kripkeho model.

Kripkeho model intuicionistickej logiky je usporiadaná trojica: $$M=(W, ≤, ⊩),$$ kde:

• $W$ je neprázdna množina možných svetov v tvare $W = \{x_1, x_2,...\}$.
• $≤$ je relácia dosiahnuteľnosti na svetoch $≤ \subseteq W × W$. Je reflexívna a tranzitívna.
• $⊩$ je relácia platnosti formuly vo svete $⊩ ⊆ W × Prop$.

Zároveň:

• Jednotlivé svety je možné chápať ako stavy, prostredia, vrcholy a podobne.
• Zápis $x_1 ≤ x_2$ je možné prečítať ako "zo sveta $x_1$ je možné dosiahnuť svet $x_2$" alebo "svet $x_2$ je dosiahnuteľný zo sveta $x_1$".
• Zápis $x⊩p$ je možné prečítať ako "vo svete $x$ platí atomický výrok $p$".

Reláciu platnosti definujeme vzhľadom na syntax jazyka: $$ \begin{array}{lcl} x⊩p & \text{potom} & ∀x' \quad \text{ak}\quad x≤x' \quad\text{potom}\quad x'⊩p \\ x⊩φ ∧ ψ & \text{vtt.} & x⊩φ \quad \text{a} \quad x⊩ψ\\ x⊩φ ∨ ψ & \text{vtt.} & x⊩φ \quad \text{alebo} \quad x⊩ψ \\ x⊩φ ⇒ ψ & \text{vtt.} & ∀x', x≤x' (\text{ak} \quad x'⊩φ \quad \text{potom} \quad x'⊩ψ) \\ x⊩ ¬φ & \text{vtt.} & ∀x', x≤x' (x' ⊯ φ)\\ x⊩⊤ & & \\ x⊩⊥ & & \end{array} $$

Definícia relácia platnosti hovorí:

• Prvý riadok opisuje pravidlo perzistencie. To znamená ak atomický výrok $p$ platí v určitom svete $x$, potom platí v každom svete $x'$ z neho dosiahnuteľnom.
• Druhý riadok jednoducho definuje konjunkciu a to tak, že formula $φ ∧ ψ$ platí vo svete $x$ ak $x⊩φ$ a zároveň $x⊩ψ$.
• Tretí riadok definuje disjunkcia tak, že formula $φ ∨ ψ$ platí vo svete $x$ ak platí $x⊩φ$ alebo $x⊩ψ$.
• Štvrtý riadok definuje implikáciu. Formula $φ ⇒ ψ$ platí vo svete $x$, ak vo všetkých z neho dosiahnuteľných svetoch $x'$, "ak platí $x'⊩φ$ potom $x'⊩ψ$".
• Piaty riadok definuje negáciu. Formula $¬φ$ platí vo svete $x$ ak vo všetkých z neho dosiahnuteľných svetoch $x'$, formula neplatí $x' ⊯ φ$.
• Posledné dva riadky hovoria, že konštanty $⊤, ⊥$ platia vždy resp. nikdy v danom svete.

Dedukčné kalkuly

Gerhard Gentzen prirodzenú dedukciu (systém NJ) a sekventový kalkul (systém LJ) pre intuicionistickú logiku jednoduchými modifikáciami jeho dedukčných kalkulov pre klasickú logiku.

Obidva systémy sú úplné a konzistentné.

Každá formula dokázateľná v intuicionistickej logike je dokázateľná aj v klasickej logike, avšak neplatí to naopak.

Prirodzená dedukcia

Prirodzená dedukcia (nazývaný aj systém NJ) intuicionistickej logiky je definovaná ako dedukčný kalkul prirodzenej dedukcie klasickej logiky (systém NK) bez dedukčného pravidla sporu.

Pravidlo sporu (neplatí v intuicionistickej logike)

Dedukčné pravidlá systému NJ:

Sekventový kalkul

Sekventový kalkul (systém LJ) získame obmedzením tvaru sekventu tak, že v závere sa môže nachádzať maximálne jedna formula.

Intuicionistický sekvent má tvar: $$Γ⊢φ,$$ pričom na pravej strane sekventu je najviac jedna formula.

Pravidlo identity a rezu:

Logické pravidlá:

Negácia

Konjunkcia

Disjunkcia

Implikácia

Konštanty

Štrukturálne pravidlá:

Pravidlá zoslabenia

Pravidlá kontrakcie

Pravidlá výmeny

Curry–Howardova korešpondencia

Curry-Howardova korešpondencia (niekedy nazývaná aj Curry-Howardovov izomorfizmus, z ang. Curry–Howard correspondence, proofs-as-programs) je základným konceptom v informatike a matematickej logike, ktorý opisuje korešpondenciu medzi logikou a programovaním. Táto korešpondencia tvrdí, že existuje priama súvislosť medzi dôkazmi v matematickej logike a programami v informatike. Konkrétne tvrdí, že dôkaz matematickej vety korešponduje s programom, ktorý rieši výpočtový problém, a naopak. Táto korešpondencia nám umožňuje uvažovať o programoch ako logických dôkazoch a naopak. To znamená, že správne typovaný program funkcionálnej paradigmy je konštruktívny dôkaz tvrdenia korešpondujúceho s jeho typom a naopak.

Vo všeobecnosti teda platí korešpondencia s výpočtovým systémom funkcionálnej paradigmy, ktorý opisuje určitá teória typov a logickým systémom. V našom prístupe sa budeme venovať korešpondencii medzi intuicionistickou logikou a jednoducho-typovaným $λ$-kalkulom.

Jednoducho-typovaný $λ$-kalkul

Je to jedna z teórii typov, opisuje typový systém pre jednoduchý funkcionálny jazyk - $λ$-kalkul s jediným typovým konštruktorom $→$ funkčného typu, ktorý zo základných typov buduje funkčné typy. V našom prístupe budeme používať jazyk rozšírený o typové súčinové a súčtové konštruktory. Pre jednoduchosť uvádzame fragment syntaxe a s využitím binárnych súčinových a súčtových typov.

Syntax jednoducho-typovaného $λ$-kalkulu

Jednoducho-typovaný $λ$-kalkul s funkčným, súčinovým a súčtovým typom má jednoduchú syntax.

• Základom jazyka je term $t$.
• Typová anotácia $t:T$ hovorí, že term $t$ je typu $T$.

Syntax v BNF: $$ \begin{array}{l} t::= x ~|~ λx:T.t ~|~ t~ t ~|~ ⟨t,t⟩ ~|~ t.i ~|~ inl~t ~|~ inr~t ~|~ case~t~of~ inl~x ⇒ t || inr~x ⇒ t \\ T::= A ~|~ T → T ~|~ T × T ~|~ T + T \end{array} $$ kde:

• $t$ metapremenná, označuje ľubovoľný term (vypočítateľný výraz).
• $x$ premenná.
• $λx:T.t$ je $λ$ abstrakcia. Výraz označuje funkciu, ktorá berie argument $x$ typu $T$ s telom $t$, pričom bodka oddeľuje argumenty funkcie od jej tela.
• $t t$ aplikácia funkcie $t$ na $t$.
• $⟨t,t⟩$ dvojica súčinového typu, po zovšeobecnení je možné rozšíriť na n-ticu.
• $t.i$ i-ta projekcia na terme súčinového typu.
• $inl~t, inr~t$ termy súčtového typu.
• $case~t~of~ x_i ⇒ t_i$ operácia selektora na terme súčtového typu.
• $T$ typová metapremenná.
• $A$ množina základných typov.
• $T → T$ funkčný typ.
• $T × T$ súčinový typ.
• $T + T$ súčtový typ.

Typové kontrola jednoducho-typovaného $λ$-kalkulu

Typovú kontrolu programov jednoducho-typovaného $λ$-kalkulu, vykonáme prostredníctvom typovacích pravidiel, ktoré sú definované pre každú alternatívu syntaxe jazyka nasledovne:

Curry–Howardová korešpondencia medzi jednoducho typovaným $λ$-kalkulom a intuicionistickou logikou

V 1943 Haskell Curry spozoroval korešpondenciu medzi intuicionistickym logickým systémom a výpočtovým systémom, ktorú neskôr znovuobjavil William Howard v 1969 a publikoval v 1980.

Korešpondencia medzi logikou a teóriou typov vychádza z princípu výroky ako typy, ktorý definuje presný vzťah medzi jednoducho typovaným $λ$-kalkulom a intuicionistickou logikou:

• Výrok $φ$ považujeme za typ.
• Dôkaz výroku $φ$ je term typu $φ$.
• Dokazovanie formuly prirodzenou dedukciou korešponduje s typovou kontrolou
• Zjednodušenie dôkazov korešponduje s vyhodnocovaním termu.