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
muudaLoogiliste 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
muudaIntuitsionistlikku loogikat saab defineerida järgneva Hilberti stiilis arvutuse järgi. Klassikalist lauseloogikat saab sarnasel moel aksiomatiseerida.[1]: 8
Lauseloogikas on tuletusreegel modus ponens:
- MP: kui ning , siis
ning aksioomid on
Et teha sellest esimese järgu lauseloogika süsteem, lisatakse üldistusreeglid
- -GEN: kui , siis , kui propositsioon ei sõltu -ist
- -GEN: kui , siis , kui propositsioon ei sõltu -ist
koos predikaate käsitlevate aksioomidega
- PRED-1: , kui term on vabalt asendatav muutujaga predikaadi puhul (kui ükski muutuja termi puhul ei ole seotud predikaadi puhul)
- PRED-2: , sama piiranguga nagu PRED-1
Eitus
muudaEt lisada eituse jaoks konnektor selle asemel, et kohelda seda kui lühendit vormist , piisab sellest, kui lisada:
- NOT-1':
- NOT-2':
Ekvivalents
muudaEkvivalentsi konnektorit võib kohelda kui lühendit, kus on lühend vormist . Alternatiivina võib lisada aksioomid
- IFF-1:
- IFF-2:
- IFF-3:
IFF-1 ja IFF-2 võib soovi korral liita kokku üheks aksioomiks kasutades konjunktsiooni.
Vaata ka
muudaViited
muuda- ↑ Bezhanishvili, Nick; De Jongh, Dick. "Intuitionistic Logic" (PDF). Amsterdami Ülikool (Loogika, keele ja arvutuse instituut).
Välislingid
muuda- Apinis, Kalmer (2021). "LTAT.03.019 Funktsionaalprogrammeerimine: Curry-Howard'i vastavus" (PDF). Tartu Ülikool.