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

## Viited

## Välislingid
*