Intuitsionistlik loogika

Intuitsionistlik loogika (inglise intuitionistic logic) ehk konstruktiivne loogika (inglise constructive logic) on mitteklassikaline loogika, mis seondub ideega konstruktiivsest tõestusest, mis tõestab matemaatilise objekti olemasolu, kirjeldades meetodit selle objekti loomiseks.

Intuitsionistlikus loogikas ei tunnistata klassikalise loogika tuletusreegleid välistatud kolmanda seadust ja kahekordse eituse seadust (väite eituse eitusest tulenevat jaatust).

Formaalsele intuitsionistlikule loogikale pani aluse hollandi matemaatik Arend Heyting, et luua formaalne põhi L. E. J. Brouweri intuitsionistlikule lähenemisele matemaatikale. Tõestusteoreetiliselt on Heytingi arvutus piiratud variant klassikalisest loogikast, millest on välistatud kolmanda ja kahekordse eituse seadused eemaldatud. Välistatud kolmandat ja kahekordse eituse elimineerimist on küll võimalik siiski tõestada teatud väidete puhul, aga need ei kehti universaalselt nagu klassikalises loogikas. Intuitsionistlikule loogikale antakse tavaliselt Brouweri-Heytingi-Kolmogorovi tõlgendus.

Süntaks

Loogiliste vormide süntaks intuitsionistlikus loogikas sarnaneb lauseloogikale ja esimest järku predikaatloogikale, aga intuitsionistlikke konnektoreid ei ole võimalik defineerida üksteise põhjal, nagu seda on võimalik klassikalises loogikas – seega on nende valik tähtis. Intuitsionistlikus lauseloogikas (IPL) on põhilisteks konnektoriteks tavaliselt →, ∧, ∨, ⊥, ning eitust ¬A koheldakse kui lühendit vormist (A → ⊥). Intuitsionistlik loogika nõuab kvantoreid ∃ ja ∀.

Hilberti stiilis arvutus

Intuitsionistlikku loogikat saab defineerida järgneva Hilberti stiilis arvutuse järgi. Klassikalist lauseloogikat saab sarnasel moel aksiomatiseerida.

Lauseloogikas on tuletusreegel modus ponens:

• MP: kui $\phi \to \psi$ ning $\phi$, siis $\psi$

ning aksioomid on

• THEN-1: $\psi \to (\phi \to \psi )$
• THEN-2: ${\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}(\chi \to \phi )\to (\chi \to \psi ){\big )}$
• AND-1: $\phi \land \chi \to \phi$
• AND-2: $\phi \land \chi \to \chi$
• AND-3: $\phi \to {\big (}\chi \to (\phi \land \chi ){\big )}$
• OR-1: $\phi \to \phi \lor \chi$
• OR-2: $\chi \to \phi \lor \chi$
• OR-3: $(\phi \to \psi )\to {\Big (}(\chi \to \psi )\to {\big (}(\phi \lor \chi )\to \psi ){\Big )}$
• FALSE: $\bot \to \phi$

Et teha sellest esimese järgu lauseloogika süsteem, lisatakse üldistusreeglid

• $\forall$-GEN: kui $\psi \to \phi$, siis $\psi \to (\forall x\ \phi )$, kui propositsioon $\psi$ ei sõltu $x$-ist
• $\exists$-GEN: kui $\phi \to \psi$, siis $(\exists x\ \phi )\to \psi$, kui propositsioon $\psi$ ei sõltu $x$-ist

koos predikaate käsitlevate aksioomidega

• PRED-1: $(\forall x\ \phi (x))\to \phi (t)$, kui term $t$ on vabalt asendatav muutujaga $x$ predikaadi $\phi$ puhul (kui ükski muutuja termi $t$ puhul ei ole seotud predikaadi $\phi (t)$ puhul)
• PRED-2: $\phi (t)\to (\exists x\ \phi (x))$, sama piiranguga nagu PRED-1

Eitus

Et lisada eituse jaoks konnektor $\neg$ selle asemel, et kohelda seda kui lühendit vormist $\phi \to \bot$, piisab sellest, kui lisada:

• NOT-1': $(\phi \to \bot )\to \neg \phi$
• NOT-2': $\neg \phi \to (\phi \to \bot )$

Ekvivalents

Ekvivalentsi konnektorit $\leftrightarrow$ võib kohelda kui lühendit, kus $\phi \leftrightarrow \chi$ on lühend vormist $(\phi \to \chi )\land (\chi \to \phi )$. Alternatiivina võib lisada aksioomid

• IFF-1: $(\phi \leftrightarrow \chi )\to (\phi \to \chi )$
• IFF-2: $(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
• IFF-3: $(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$

IFF-1 ja IFF-2 võib soovi korral liita kokku üheks aksioomiks $(\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))$ kasutades konjunktsiooni.

Vaata ka

• Klassikaline loogika

Välislingid

• Apinis, Kalmer (2021). "LTAT.03.019 Funktsionaalprogrammeerimine: Curry-Howard'i vastavus" (PDF). Tartu Ülikool.