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

muuda

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

muuda

Intuitsionistlikku 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

  • THEN-1:  
  • THEN-2:  
  • AND-1:  
  • AND-2:  
  • AND-3:  
  • OR-1:  
  • OR-2:  
  • OR-3:  
  • FALSE:  

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

muuda

Et lisada eituse jaoks konnektor   selle asemel, et kohelda seda kui lühendit vormist  , piisab sellest, kui lisada:

  • NOT-1':  
  • NOT-2':  

Ekvivalents

muuda

Ekvivalentsi 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

muuda

Viited

muuda
  1. Bezhanishvili, Nick; De Jongh, Dick. "Intuitionistic Logic" (PDF). Amsterdami Ülikool (Loogika, keele ja arvutuse instituut).

Välislingid

muuda