Iskazna logika

Zamislimo da smo jednog oblačnog jutra izašli na ulicu i zapitali se Da li je sinoć padala kiša? Jednostavan način da odgovorimo sami na ovo pitanje je da pogledamo samu ulicu. Ako je ulica suva, znaćemo da kiša te noći nije padala.

Dnevno donesemo desetine zaključaka slične prirode, često i ne razmišljajući pritom o samom procesu zaključivanja. Zbog toga se neretko mogu javiti logičke greške kojih često nismo ni svesni. Proučavanjem iskazne logike, oblasti logike koja proučava proces donošenja zaključaka na osnovu datih iskaza, možemo naučiti pravilan način donošenja zaključaka i time izbeći spomenute logičke greške. Kao što sâmo ime kaže, u iskaznoj logici bavićemo se iskazima. Iskazi (ili još propozicije ili sudovi) jesu iskazne rečenice koje mogu biti ili tačne ili netačne.

U prirodnom (maternjem) jeziku logička struktura unutar neke rečenice uspostavlja se korišćenjem logičkih veznika kojima se povezuju jednostavniji iskazi. U srpskom jeziku (kao i u ostalim prirodnim jezicima) osnovni logički veznici su nije…, …ili…, …i…, ako…tada… i …ako i samo ako…. Analogno prirodnom jeziku, u iskaznoj logici složeniji iskazi formiraju se vezivanjem jednostavnijih iskaza uz pomoć logičkih veznika iskazne logike.

Na osnovu datih iskaza, koristeći pravila koje propisuje logika moguće je doneti zaključak. Proces zaključivanja se često zapisuje u obliku liste. Na početku te liste nalaze se pretpostavke (kojih može biti proizvoljno, ali konačno mnogo), a na kraju liste nalazi se zaključak (koji se sastoji od samo jednog iskaza). Simbolom trotačke ∴ koji se nalazi u poslednjem redu ispred zaključka, ističe se da je ono što sledi zaključak. On se može čitati sledi…. Naš proces zaključivanja s početka poglavlja može se predstaviti sledećom listom:

1. Ako je kiša padala, ulice su mokre
2. Ulice nisu mokre
3. ∴ Kiša nije padala

Najjednostavnije iskaze koji nemaju svoju unutrašnju logičku strukturu, ili nas ona ne interesuje, predstavljamo iskaznim slovima. Pri tom vodimo računa da svakom iskazu pridružimo jedinstveno slovo. Na primer, složeni iskaz poput Ako je kiša padala tada su ulice mokre možemo predstaviti oblikom Ako A tada B, gde iskazno slovo A označava iskaz Kiša je padala, a iskazno slovo B označava iskaz Ulice su mokre. Tako prethodni primer postaje:

1. Ako A tada B
2. Nije B
3. ∴ Nije A

Gornja šema zaključivanja naziva se modus tollens, i primer je jednog od najosnovnijih pravila validnog donošenja zaključka. Bez obzira na to kakvi iskazi stoje umesto slova A i B zaključivanje će biti validno, tj. ako su obe pretpostavke tačne tada će i zaključak biti tačan. Naravno, neće svaka shema zaključivanja biti validna. Ako samo malo promenimo naš primer dobićemo nevalidno zaključivanje.

1. Ako A tada B
2. Nije A
3. ∴ Nije B

Na prvi pogled, gornja shema nam može delovati validno, ali ako se vratimo na primer s mokrim ulicama, videćemo u čemu je problem.

1. Ako je kiša padala, ulice su mokre
2. Kiša nije padala
3. ∴ Ulice nisu mokre

Ovako bismo zaključili da ako te noći nije padala kiša, onda ni ulice nisu mokre. Međutim, možda su baš tog jutra čistači oprali ulicu. Tada će, naravno, ulica biti mokra, iako nam naš zaključak govori suprotno.

Većina ljudi nema problema sa uviđanjem logičkih grešaka u ovako jednostavnom logičkom zaključivanju. Međutim, kada se taj isti logički zaključak apstrahuje uvođenjem logičkih slova, kako je i urađeno u pretposlednjem primeru, ili se složenost i broj iskaza uveća, većina ljudi ima problem sa uočavanjem grešaka, i sklona je i sama da ih pravi.

Da bismo izbegli ovakve greške, potrebno je upoznati se s pravilima logičkog rasuđivanja. Ovaj tekst je upravo posvećen sistematskom proučavanju iskazne logike. U njemu će biti opisana iskazna logika iz ugla matematičke logike, pa će ovaj tekst pratiti proces zaključivanja u matematici. Stoga će razni aspekti svakodnevnog logičkog rasuđivanja biti izostavljeni. Sadržaj teksta je naveden u sledećoj listi.

Naš prvi korak u proučavanju logike biće definisanje novog, simboličkog zapisa iskaza.

Sintaksa iskazne logike

U prethodnom delu, prilikom zapisivanja primera iskaznih rečenica poštovali smo pravila sintakse srpskog jezika. Niz reči koji ne zadovoljava pravila sintakse srpskog jezika Mokre je ako kiša ulice padala su nemoguće je razumeti iako sadrži samo srpske reči (i to čak samo one koje se nalaze u sasvim razumljivoj rečenici Ako je kiša padala, ulice su mokre).

Slično prirodnom jeziku, i rečenice u jeziku iskazne logike moraju zadovoljavati određena pravila. Upravo sintaksa iskazne logike opisuje strukturu složenih iskaza, posmatrajući iskaze pritom kao nizove simbola. Da bi se definisala sintaksa nekog jezika, potrebno je prvo definisati alfabet tog jezika.

Alfabet Σ je unija sledećih skupova:

• Prebrojivog skupa iskaznih slova. Uobičajno je da se iskazna slova obeležavaju malim latiničnim slovima, po potrebi sa indeksima.
• Skupa logičkih veznika kojeg čine jedan unarni veznik ¬ (negacija) i četiri binarna veznika ∨ (disjunkcija), ∧ (konjunkcija), ⇒ (implikacija) i ⇔ (ekvivalencija).
• Skupa logičkih konstanti kojeg čine simbol ⊤ (čita se te) i simbol ⊥ (čita se en-te).
• Skupa pomoćnih simbola kojeg čine leva i desna zagrada.

Reč nad alfabetom Σ je svaki konačan niz simbola iz Σ. Skup svih reči nad alfabetom Σ označavamo sa Σ*.

U skupu svih reči nad alfabetom jezika iskazne logike, nalaze se i nizovi poput ∨p⊥∧∧. Međutim, ovakvi nizovi za nas nisu interesantni. Zbog toga uvodimo pojam dobro formiranih formula¹ iskazne logike (kraće samo iskazne formule).

Skup izkaznih formula, u oznaci For, najmanji je podskup skupa svih reči nad alfabetom Σ, takav da važe sledeći uslovi:

• Iskazna slova i logičke konstante pripadaju skupu iskaznih formula.
• Ako formula α pripada skupu iskaznih formula, tada skupu iskaznih formula pripada i formula ¬α
• Ako formule α i β pripadaju skupu iskaznih formula, tada skupu iskaznih formula pripadaju i formule (α ∧ β), (α ∨ β), (α ⇒ β) i (α ⇔ β).

Skup iskaznih formula je induktivno definisan. U skup iskaznih formula prvo su uvedena iskazna slova i logičke konstante, da bi zatim bile uvedene složenije formule koje su negacije, konjunkcije, disjunkcije, implikacije i ekvivalencije iskaznih formula koje se već nalaze u skupu iskaznih formula. Uslovom da je skup iskaznih formula najmanji skup takav da zadovoljava navedene osobine, osigurali smo se da se u njemu ne mogu naći besmisleni nizovi simbola (poput p¬ ∧ q ⇔).

Primetimo da uz korišćenje binarnih veznika koristimo i zagrade. Zagrade se koriste da bi se izbegla moguća dvosmislenost iskaznih formula. Na primer, bez zagrada ne možemo znati da li formula p ⇒ q ∧ r označava p ⇒ (q ∧ r) ili (p ⇒ q) ∧ r. Sa druge strane, pisanje velikog broja zagrada u formulama može uticati na čitljivost formule. Zbog toga se uvodi konvencija o prioritetu logičkih veznika. Znak negacije ima najviši prioritet kao jedini unarni veznik. Zatim slede znaci ∧ i ∨ koji imaju podjednak prioritet, a za njima znaci ⇒ i ⇔ koji imaju takođe podjednak prioritet. Ova konvencija nam omogućava da obrišemo zagrade oko formula čiji veznik ima najveći prioritet. Tako u formuli p ⇒ (q ∧ r) možemo obrisati zagrade, znajući da onaj ko čita formulu može rekonstruisati početnu formulu stavljajući zagrade oko veznika s najvišim prioritetom idući pritom sleva nadesno. U formuli p ⇒ ¬(q ∧ r) ne bismo smeli obrisati zagrade, jer bi neko ko čita formulu p ⇒ ¬q ∧ r postavljajući zagrade na opisan način došao do formule p ⇒ ((¬q) ∧ r). Ipak, potrebno je biti pažljiv sa opisanom konvencijom, jer se u literaturi mogu sresti i druge konvencije o prioritetu veznika.

Zagrade je moguće u potpunosti izostaviti ako se koristi prefiksna poljska notacija. U takvoj notaciji, veznik se piše ispred simbola koje vezuje. Tako formula p ⇒ q postaje ⇒ p q a formula p ⇒ (q ∧ r) postaje ⇒ p ∧ q r. Ipak, ta notacija je još manje čitljiva od formula sa zagradama, pa je mi nećemo koristiti. Ako bismo ipak želeli da koristimo ovakav zapis, tada bi trebalo prepraviti gornje definicije alfabeta iskazne logike i skupa dobro formiranih formula.

Za obeležavanje proizvoljne iskazne formule, koristićemo mala grčka slova, po potrebi sa indeksom. Na taj način ćemo ih lako razlikovati od iskaznih slova (koja su i sama iskazne formule, ali nije svaka iskazna formula iskazno slovo).

Za dve formule α i β kažemo da su sintaksno identične (jednake) ako se sastoje od istih simbola poređanih istim redosledom. Činjenicu da su dve formule sintaksno identične zapisujemo α = β, a činjenicu da nisu α ≠ β.

Kako smo skup iskaznih formula izgradili induktivno, u njemu možemo upotrebiti princip matematičke indukcije.

Teorema (Indukcija nad skupom iskaznih formula): Neka je V neko svojstvo iskaznih formula. Ako:

1. za svako iskazno slovo i logičku konstantu važi V
2. za sve iskazne formule važi da ako formule α i β imaju svojstvo V tada svojstvo V imaju i formule ¬α, ¬β, α ∧ β, α ∨ β, α ⇒ β, α ⇔ β

tada svojstvo V važi za svaku iskaznu formulu.

Dokaz: Neka je L skup svih iskaznih formula koje poseduju svojstvo V. Skup L zadovoljava uslove date u definiciji skupa iskaznih formula For. Kako je skup iskaznih formula najmanji takav skup koji poseduje zadate uslove, sledi da je skup For podskup skupa L, tj. svojstvo V važi za svaku iskaznu formulu. □

Uvešćemo još dva pojma koja će nam biti od koristi u daljem izlaganju:

Skup potformula formule α je najmanji skup iskaznih formula za koji važi:

• Formula α pripada skupu potformula formule α.
• Ako je α formula oblika ¬β, tada potformule formule β pripadaju skupu potformula formule α.
• Ako je α formula oblika β ∧ γ, β ∨ γ, β ⇒ γ ili β ⇔ γ, tada potformule formula β i γ pripadaju skupu potformula formule α.

Složenost formule α, u oznaci c(α), jeste prirodan broj dodeljen formuli α za koji važi:

• Ako je formula α iskazno slovo ili logička konstanta, tada je c(α) = 0.
• Ako je α formula oblika ¬β, tada je složenost formule α data sa c(α) = c(β) + 1.
• Ako je α formula oblika β ∧ γ, β ∨ γ, β ⇒ γ ili β ⇔ γ, tada je složenost formule α data sa c(α) = c(β) + c(γ) + 1.

Semantika iskazne logike

Definisanjem sintakse iskazne logike osigurali smo se da iskazi s kojima ćemo raditi budu smisleno definisani. S definisanom sintaksom, ima smisla postavljati osnovno pitanje logike Da li je iskaz tačan? Definisanjem semantike iskazne logike moći ćemo da odgovorimo na sâmo pitanje tačnosti složenog iskaza na osnovu tačnosti iskaznih slova.

Ako se osvrnemo na prirodni jezik, primetićemo da istinitosna vrednost složenih rečenica zavisi od istinitosti iskaza koji čine rečenicu, ali i od logičkih veznika koji spajaju te iskaze. Za rečenicu Danas je utorak i danas pada kiša reći ćemo da je tačna samo ako je danas baš utorak i danas baš pada kiša. Ako barem jedan od ta dva uslova nije ispunjen, za tu rečenicu ćemo reći da je lažna. Suprotno tome, za rečenicu koja se razlikuje samo u vezniku Danas je utorak ili danas pada kiša reći ćemo da je tačna ako je barem jedan od iskaza tačan.

Slično prirodnom jeziku, istinitost iskaza iskazne logike zavisi ne samo od istinitosti iskaznih slova, već i od veznika kojim su ta iskazna slova vezana. Zbog toga ćemo definisati dva nova pojma iskazne logike, koja će nam govoriti o istinitosti iskaznih slova i iskaznih formula sačinjenih od tih slova.

Valuacija je pravilo po kojem se svakom iskaznom slovu jezika iskazne logike pridružuje jedna i samo jedna vrednost: tačno ili netačno. Valuacije se najčešće obeležavaju malim slovima, po potrebi sa indeksima. Ako valuacija v iskaznom slovu p daje vrednost tačno, to ćemo označavati sa v(p) = 1. U suprotnom, pisaćemo v(p) = 0.

Interpretacija ili proširenje valuacije je pravilo po kojem se svakoj iskaznoj formuli pridružuje jedna i samo jedna istinitosna vrednost: tačno ili netačno. Analogno valuacijama, ako interpretacija I iskaznoj formuli ψ daje vrednost tačno, to ćemo označavati sa I(ψ) = 1, a u suprotnom I(ψ) = 0. Svaka interpretacija mora posedovati sledeće osobine:

• Ako je ψ iskazno slovo tada I(ψ) = v(ψ).
• Ako je ψ formula oblika ¬φ gde je φ isto iskazna formula, tada I(ψ) = 0 ako i samo ako I(φ) = 1, a I(ψ) = 1 ako i samo ako I(φ) = 0.
• Ako je ψ formula oblika α ∧ β gde su α i β iskazne formule, tada je I(ψ) = 1 ako i samo ako je I(α) = 1 i I(β) = 1.
• Ako je ψ formula oblika α ∨ β gde su α i β iskazne formule, tada je I(ψ) = 0 ako i samo ako je I(α) = 0 i I(β) = 0.
• Ako je ψ formula oblika α ⇒ β gde su α i β iskazne formule, tada je I(ψ) = 0 ako i samo ako je I(α) = 1 i I(β) = 0.
• Ako je ψ formula oblika α ⇔ β gde su α i β iskazne formule, tada je I(ψ) = 1 ako i samo ako je I(α) = I(β).
• Važi I(⊤) = 1 i I(⊥) = 0.

Jasno je da interpretacija direktno zavisi od valuacije koju proširuje. Ako želimo da naglasimo da je interpretacija I proširenje valuacije v, koristićemo oznaku I_v za interpretaciju I.

Pogledajmo svaki od veznika da bi nam bilo jasnije zašto su u definiciji interpretacije uzete baš navedene osobine.

Konjunkcija dve formule α i β, u oznaci α ∧ β, jeste formula koja je tačna samo ako su obe formule tačne. Prema tome, vrednost formule α ∧ β možemo predstaviti putem tabele u zavisnosti od vrednosti konjunkata α i β.

Veznik konjunkcije oslikava reč i u prirodnom jeziku. Na primer, rečenica Danas je ponedeljak i danas pada kiša biće tačna samo ako su tačne izjave Danas je ponedeljak i Danas pada kiša. Umesto znaka ∧, u literaturi (pogotovo starijoj) mogu se pronaći i znakovi & ili •.

Disjunkcija formula α i β, u oznaci α ∨ β, jeste formula koja je tačna samo ako je barem jedan od disjunkata α i β tačan. Slično konjunkciji, i disjunkciju možemo predstaviti tabelom:

Disjunkcija oslikava reč ili iz prirodnog jezika. Međutim, u prirodnom jeziku, reč ili može nositi dva različita značenja. U prvom slučaju celu rečenicu ćemo smatrati tačnom samo ako je jedan od disjunkata tačan, ali ne i oba. Na primer, zamislimo situaciju u kojoj zaposleni kaže svom poslodavcu Ili ćeš mi dati povišicu ili ću ja dati otkaz. Ako zaposleni dobije povišicu, a zatim da otkaz, smatraćemo njegov iskaz netačnim. Ali ako zaposleni dobije povišiću i ne da otkaz, ili ne dobije povišicu i da otkaz, njegov iskaz smatraćemo tačnim. Ovakvo korišćenje reči ili nazivamo isključujuće ili (na engleskom: exclusive or). Najčešće rečenice prirodnog jezika koje koriste isključujuće ili su u obliku ili …ili… Suprotno isključujućem, uključujuće ili (ili kraće samo ili) dozvoljava da oba disjunkta budu tačna. U birokratskom jeziku, često se može videti oznaka i/ili koja označava uključujuće ili. U iskaznoj logici i matematici, uvek se misli na uključujuće ili osim ako drugačije nije naglašeno. Mi ćemo se, naravno, držati matematičkog značenja reči ili.

Implikacija formula α i β, u oznaci α ⇒ β, jeste formula koja je netačna samo ako je α tačna formula i β netačna formula. Tabela za implikaciju izgleda ovako:

Znak implikacije donekle označava izraz Ako…tada… koji koristimo u prirodnom jeziku. Međutim, treba obratiti pažnju na to da će implikacija α ⇒ β biti tačna kad god je formula α netačna, bez obzira na logičku povezanost formula α i β. To se donekle kosi sa značenjem izraza Ako…tada… u prirodnom jeziku. Na primer, rečenica Ako je Zemlja ravna tada jednorozi postoje u iskaznoj logici se smatra tačnom jer je iskaz Zemlja je ravna netačan. U svakodnevnom govoru rečenicu Ako je Zemlja ravna tada jednorozi postoje ne bismo smatrali tačnom jer ne vidimo nikakvu uzročno-posledičnu vezu između iskaza.

U starijoj literaturi za implikaciju se ponekad koristi simbol ⊂. Ta notacija se danas izbegava, jer joj je dodeljeno drugo značenje.

Ekvivalencija formula α i β, u oznaci α ⇔ β, jeste formula koja je tačna samo kada i α i β imaju istu istinitosnu vrednost. Tabela za ekvivalenciju izgleda ovako:

Kao i ostali veznici, i ekvivalencija ima analogni veznik u prirodnom jeziku. To je izraz …ako i samo ako…. Često se taj izraz piše skraćeno sa …akko… ili, ako se radi o engleskom jeziku, …iff… (obratite pažnju na dupla slova k i f).

Negacija formule α, u oznaci ¬α, jeste formula čija istinitosna vrednost iznosi 1 samo ako istinitosna vrednost formule α iznosi 0. Zavisnost istinitosti ¬α od α možemo predstaviti sledećom tabelom:

Veznik negacije oslikava reči ne i nije u prirodnom jeziku.

Iskazna logika se zasniva samo na upotrebi do sada definisanih veznika, koji oslikavaju osnovne logičke veznike u prirodnom jeziku. Međutim, u prirodnom jeziku, logička struktura neke rečenice, uspostavlja se upotrebom još nekih vrsta reči, koje nisu predmet iskazne logike. Zbog toga mnoga validna zaključivanja iz prirodnog jezika, nije moguće opisati jezikom iskazne logike. Za matematiku je, uz iskaznu logiku, najznačajnija predikatska logika u kojoj se koriste kvantifikatori i predikati. Mi ćemo se u ovom tekstu, fokusirati samo na iskaznu logiku…

U prethodnim redovima dali smo prvo definiciju interpretacije kao pravilo koje svakoj formuli pridružuje njenu istinitosnu vrednost u zavisnosti od izabrane valuacije. Zatim smo detaljnije opisali svaki od veznika, da bismo time opravdali njihovu semantiku. Interpretacija upravo koristi semantiku tih veznika da bi odredila istinitosnu vrednost formule. Određivanje istinitosne vrednosti složene formule podrazumeva „cepkanje“ složene formule na jednostavnije potformule i određivanje njihove istinitosne vrednosti. Taj proces se ponavlja sve dok se ne stigne do samih iskaznih slova čija je istinitosna vrednost data valuacijom.

U praksi, za ispitivanje istinitosne vrednosti formule ψ pri različitim valuacijama postoje mnoge metode. Najjednostavnija je metoda istinitosne tablice (nešto slično smo već koristili za opisivanje veznika). U njoj za svaku potformulu formule ψ postoji jedinstvena kolona, a za svaku valuaciju koju želimo da ispitamo jedinstveni red. Počevši od iskaznih slova, izračunavaju se istinitosne vrednosti svih potformula sve dok se ne dođe do formule ψ. Ukoliko formula ψ sadrži n iskaznih slova, tada će nam od interesa biti najviše 2ⁿ različitih interpretacija.

Primer: Ispitajmo istinitost formule ¬(p ∧ q) ⇒ (¬p ∨ r) pri svim mogućim valuacijama za iskazna slova p, q i r:

▲

Loša strana ove metode je to što se broj potrebnih vrsta eksponencijalno povećava s brojem iskaznih slova koja se nalaze u formuli. Ali za jednostavnije formule ovom metodom lako možemo proveriti njihovu istinitost u zavisnosti od date valuacije. Posebno će nam biti od interesa one valuacije pri kojima je formula tačna. U prethodnom primeru takve su sve valuacije osim one zadate sa (p,q,r) ↦ (1,0,0).

Valuacija v je model formule α ako I_v(α) = 1. Tada pišemo v ⊨ α i za valuaciju kažemo da zadovoljava formulu α.

Jasno je da neke formule mogu imati više različitih modela, slično formuli iz primera. Za formule koje imaju barem jedan model kažemo da su zadovoljive. Veoma su interesantne formule koje su zadovoljive s bilom kojom valuacijom.

Tautologija ili valjana formula je formula koju svaka valuacija v zadovoljava. Činjenicu da je formula α tautologija zapisaćemo ⊨ α. Da je neka formula tautologija, možemo lako zaključiti na osnovu istinitosne tablice.

Kontradikcija je formula za koju ne postoji nijedna valuacija koja je zadovoljava. Slično tautologiji, i kontradikciju možemo lako uočiti na osnovu istinitosne tablice. Jasno, neka formula α je kontradikcija ako i samo ako je formula ¬α tautologija.

Za formule α i β koje pri istim valuacijama imaju iste istinitosne vrednosti reći ćemo da su semantički ekvivalentne i tu činjenicu ćemo zapisivati α ≡ β. Sintaksno ekvivalentne formule su očigledno i semantički ekvivalentne. Međutim, obrnuto ne mora da važi. Na primer, formule ¬p ∨ q i p ⇒ q imaju istu istinitosnu vrednost iako su to sintaksno različite formule.

Prilikom posmatranja neke valuacije ne moramo se ograničiti na posmatranje jedne iskazne formule. Umesto toga, možemo posmatrati istinitosnu vrednost celog skupa formula pri nekoj valuaciji.

Valuacija v je model skupa formula Γ = { α₁, α₂, …, α_n, … } ako za svako α_k iz Γ važi v ⊨ α_k. Za takav skup kažemo da je zadovoljiv i pišemo v ⊨ Γ. Ako valuacija v nije model skupa Γ tada pišemo v ⊭ Γ. Ako ne postoji model koji zadovoljava skup iskaznih formula Γ, tj. za svaku valuaciju važi v ⊭ Γ, tada za skup Γ kažemo da je kontradiktoran ili protivrečan.

Da bismo bolje proučili procese validnog zaključivanja (a setite se, to nam je glavna motivacija za izučavanje logike), potrebno je uvesti pojam koji će nam reći u kakvom su odnosu istinitost pretpostavki i istinitost zaključka. Zato uvodimo pojam semantičke posledice.

Semantička posledica skupa iskaznih formula Γ jeste formula α takva da za svaku valuaciju v za koju važi v ⊨ Γ sledi v ⊨ α. Činjenicu da je formula α semantička posledica skupa formula Γ obeležavamo sa Γ ⊨ α, a u suprotnom pišemo Γ ⊭ α.

Teorema: Neka je Γ proizvoljan skup formula i neka je α formula.

1. Ako α pripada skupu Γ tada Γ ⊨ α.
2. Formula α je tautologija ako i samo ako je α semantička posledica praznog skupa formula.
3. Ako Γ ⊨ α i Γ je podskup skupa Δ, tada Δ ⊨ α.
4. Ako je skup Γ kontradiktoran, tada je svaka formula α semantička posledica skupa Γ.
5. Ako je α tautologija, tada za svaki skup formula Γ važi Γ ⊨ α.
6. Ako Γ ⊨ α i formula γ iz Γ je tautologija, tada Γ \ { γ } ⊨ α.

Dokaz: Navedena tvrđenja se jednostavno dokazuju.

1. Prvo tvrđenje trivijalno sledi iz same definicije semantičke posledice. Naime, ako proizvoljna valuacija zadovoljava skup Γ, onda ona zadovoljava i svaki element skupa Γ pa samim tim i α.
2. Ako je formula α tautologija, tada je njen model svaka valuacija, pa i ona valuacija koja zadovoljava prazan skup. Dakle, ona je semantička posledica praznog skupa. Obrnuto, ako je α semantička posledica praznog skupa tada je ona i tautologija (jer je svaka valuacija model praznog skupa)².
3. Ako je Γ podskup skupa Δ, tada važi da svaki model skupa Δ jeste i model skupa Γ. Kako Γ ⊨ α, sledi da je svaki model skupa Γ takođe i model formule α, pa iz toga zaključujemo da je svaki model skupa Δ ujedno i model formule α. Da bismo se uverili da obrnuto ne važi dovoljno je da posmatramo skup Δ = { p, p ∨ ¬p } i njegov podskup Γ = { p ∨ p }. Za date skupove važi Δ ⊨ p ali ne važi Γ ⊨ p.
4. Ako je skup Γ kontradiktoran, tada ne postoji nijedna valuacija koja zadovoljava Γ. Iz toga sledi da svaka valuacija koja zadovoljava Γ zadovoljava i α.
5. Kako je α tautologija, tada će je svaka valuacija zadovoljiti pa će je zadovoljiti i valuacija koja zadovoljava Γ.
6. Ako je γ tautologija, tada će svaki model skupa Γ \ { γ } biti i model skupa Γ, iz čega sledi Γ \ { γ } ⊨ α.

□

Osim navedenih osobina, semantička posledica se lepo slaže s veznikom implikacije. Navešćemo teoremu koja ovo pokazuje.

Stav: Γ, α ⊨ β ako i samo ako Γ ⊨ α ⇒ β.

Dokaz: Pretpostavimo prvo da važi Γ, α ⊨ β. Neka je valuacija v takva da zadovoljava skup Γ. Dokažimo da tada mora važiti Γ ⊨ α ⇒ β. Pretpostavimo suprotno, tj. da I_v(α ⇒ β) = 0. Po definisanoj semantici iskazne logike, zaključujemo da je I_v(α) = 1 i I_v(β) = 0. Iz toga sledi da valuacija v zadovoljava i Γ ∪ {α}. Po prvoj pretpostavci, tada valuacija v zadovoljava i formulu β. Međutim, to je nemoguće jer smo zaključili da je I_v(β) = 0. Dakle, pretpostavka da je I_v(α ⇒ β) = 0 je pogrešna. Iz toga zaključujemo da ako je Γ, α ⊨ β tada Γ ⊨ α ⇒ β.

Da bismo dokazali drugi smer tvrđenja pretpostavimo da važi Γ ⊨ α ⇒ β. Neka je v valuacija koja zadovoljava skup Γ ∪ { α }. Kako v zadovoljava i sam skup Γ, sledi da je I_v(α ⇒ β) = 1. Kako odabrana valuacija zadovoljava i formulu α na osnovu semantike znaka implikacije, zaključujemo da v zadovoljava i β. □

U ovom dosadašnjem izlaganju ustanovili smo sintaksu iskazne logike (način građenja iskaznih formula), a zatim smo definisali i semantiku iskazne logike (ustanovili smo značenje logičkih veznika). Osim toga, definisali smo pojmove valuacije, interpretacije, modela, semantičke posledice i dali smo jedan način za ispitivanje tačnosti formule uz pomoć tabela. U narednom poglavlju, Sistemi dedukcije u iskaznoj logici, ispitaćemo da li možemo nešto zaključiti o istinitosti formule na osnovu same njene strukture, bez korišćenja interpretacija, i uvešćemo pojam sintaksne posledice.

Ali, pre nego što pređemo na sledeće poglavlje, zadržimo se još malo na semantici logičkih veznika.

Potpun sistem veznika

Prilikom definisanja semantike iskazne logike, spomenuli smo da veznik disjunkcije oslikava takozvano uključujuće ili. U prirodnom jeziku osim njega postoji i isključujuće ili, koje je tačno samo ako je jedan od disjunkata tačan (ali ne i oba!). Međutim, u iskaznoj logici ni u jednom trenutku nismo uveli veznik koji bi predstavljao ovakav veznik prirodnog jezika. Postavlja se pitanje da li smo time na neki način oslabili našu logiku. Takođe, nameće se i pitanje da li osim spomenutog veznika postoji još veznika koje nismo uključili u sintaksu logike.

Na sreću, odgovor na prvo pitanje je odričan. Izostavljanjem znaka za isključujuću disjunkciju nismo ni na dobitku ni na gubitku. Uvedimo za trenutak u naš alfabet iskazne logike binarni veznik ⊻ i dodelimo mu semantiku na sledeći način:

Sasvim je sigurno da je novi veznik drugačiji od onih koje smo definisali. Međutim, ako ispitamo istinitost iskazne formule ¬(α ⇔ β), videćemo da dobijamo istu tabelu.

Prema tome, formulu α ⊻ β možemo zameniti formulom ¬(α ⇔ β) i veznik ⊻ nam više nije potreban.

Šta je sa ostalim mogućim veznicima? Ako pogledamo bolje, videćemo da par logičkih simbola može imati četiri istinitosne vrednosti. Svaki binarni veznik dodeljuje jednu istinitosnu vrednost svakom od ta četiri moguća para koje vezuje. Prema tome, ukupno postoji 2⁴ moguća binarna veznika. Dokazaćemo sada da nam je dovoljno samo ono sa čim raspolažemo da bismo izrazili svaki od ovih potencijalnih veznika.

Teorema: Svaki n-arni veznik se može predstaviti kao kombinacija veznika ∧, ∨, ¬.

Dokaz: Neka je ◇(p₁, p₁, …, p_n) n-arni logički veznik. Tada ◇ može biti definisan tablicom koja ima 2ⁿ vrsta od kojih svaka sadrži jednu od mogućih kombinacija istinitosnih vrednosti koje mogu biti dodeljene slovima p₁, p₂, …, p_n, kao i istinitosnu vrednost ◇(p₁, p₁, …, p_n). Za indeks 1≤k≤2ⁿ definišimo formulu γ_k kao konjunkciju β₁ ∧ β₂ ∧ … ∧ β_n, gde je β_l = p_l ako je u toj vrsti slovu p_l dodeljena vrednost 1, a u suprotnom β_l = ¬p_l. Dalje, neka je Δ disjunkcija svih formula γ_k takvih da ◇(p₁, p₂, …, p_n) ima vrednost 1 u k-toj vrsti za svako 1≤k≤2ⁿ. Ako takvih vrsta nema, onda veznik ◇ možemo zameniti bilo kojom kontradikcijom, npr. p₁ ∧ ¬p₁. Dokažimo da vezniku ◇ odgovara formula Δ. Neka je v proizvoljna valuacija. Ako u proizvoljnoj vrsti l formula ◇(p₁, p₂, …, p_n) ima istinitosnu vrednost 1, tada se u Δ nalazi γ_l pa Δ ima vrednosti 1 u toj vrsti. Ako u toj vrsti formula ◇(p₁, p₂, …, p_n) ima istinitosnu vrednost 0, tada i Δ ima istinitosnu vrednost 0 jer ne sadrži γ_l, a sve ostale γ_k imaju istinitosnu vrednost 0. Kako smo dokazali tvrđenje za proizvoljnu vrstu, zaključujemo da isto važi za sve vrste, pa Δ zaista jeste zamena za formulu ◇(p₁, p₂, …, p_n). □

Primetimo da u prethodnom dokazu nismo koristili veznike implikacije i ekvivalencije za konstruisanje formule Δ. Posledica toga je da je i te veznike moguće zameniti nekim formulama sastavljenim od negacije, konjunkcije i disjunkcije. Jedna takva zamena mogla bi ovako da izgleda:

• ¬α ∨ β umesto α ⇒ β
• (¬α ∨ β) ∧ (¬β ∨ α) umesto α ⇔ β

Za skup logičkih veznika pomoću kojih možemo predstaviti ostale logičke veznike, kažemo da je potpun.

Takav je skup veznika { ∧, ∨, ¬ }, a svakako je to i njegov nadskup { ¬, ∧, ∨, ⇒, ⇔ }. U iskaznoj logici najčešće koristimo veznike iz skupa { ¬, ∧, ∨, ⇒, ⇔ } jer baš ti logički veznici oslikavaju veznike koje imamo u prirodnom jeziku. Time se postiže bolja čitljivost i razumljivost iskaznih formula.

Ne moramo se ograničiti ni na tri veznika. Veznik disjunkcije možemo predstaviti formulom ¬(¬α ∧ ¬β), koja koristi samo negaciju i konjunkciju. A možemo i konjunkciju α ∧ β predstaviti formulom ¬(¬α ∨ ¬β) koja koristi samo negaciju i disjunkciju. Dakle, svaki od skupova { ∧, ¬ } i { ∨, ¬ } je potpun. Slično se može pokazati da je i skup { ⇒, ¬ } potpun.

Štaviše, možemo se ograničiti na jedan jedini veznik. Uvedimo dva nova veznika: Lukašievičevu³ strelicu ↓ i Šeferovu⁴ strelicu ↑, i definišimo ih na sledeći način:

Sada negaciju ¬α možemo zameniti formulom α ↑ α ili α ↓ α, a konjunkciju α ∧ β možemo zameniti sa (α ↓ α) ↓ (β ↓ β) ili (α ↑ β) ↑ (α ↑ β). Kako je skup { ¬, ∧ } potpun, potpuni su i jednočlani skupovi { ↓ } i { ↑ }.

Šeferova i Lukašievičeva strelica su dobro poznati veznici u računarskim i elektrotehničkim naukama, gde su često poznati i kao NAND i NOR operatori.

Normalne forme

Za razliku od ostalih opisanih veznika, Šeferova i Lukašievičeva strelica se ne pojavljuju kao veznici u prirodnom jeziku. Zbog toga ljudi nemaju intuitivni osećaj za rad sa iskaznim formulama u kojima figurišu ovi veznici. Sa veznicima disjunkcije, konjunkcije i negacije veoma je lako raditi. Ta lakoća delimično potiče od njihovih pojavljivanja u prirodnom jeziku, a delimično i od algebarskih zakonitosti koje ovi veznici poseduju. O tome govori sledeća teorema.

Teorema: Za sve iskazne formule α, β i γ važe sledeće semantičke ekvivalencije:

Dokaz: Dokaz navedenih ekvivalencija (zakona) vrši se diskusijom po mogućim istinitosnim vrednostima formula α, β i γ, ili primenom već dokazanih zakonitosti. Dokaz izostavljamo jer je idejno jednostavan. □

Primetimo da će formula oblika α₁ ∧ α₂ ∧ … ∧ α_n biti tačna ako i samo ako je svaka od formula α_i za 1≤i≤n tačna. S druge strane, formula oblika α₁ ∨ α₂ ∨ … ∨ α_n biće tačna ako je barem jedna od formula α_i za 1≤i≤n tačna. Ako je svaka formula α_i oblika p_i ili ¬p_i, tada ćemo veoma lako odrediti da li neka data valuacija zadovoljava formule α₁ ∧ α₂ ∧ … ∧ α_n ili α₁ ∨ α₂ ∨ … ∨ α_n.

Sve ovo navedeno nas upućuje na značaj formula koje su sačinjene samo od disjunkcija, konjunkcija i negacija iskaznih slova. Zato uvodimo naredne pojmove:

Literal je iskazna formula oblika p ili ¬p, gde je p iskazno slovo. Za iskaznu formulu α kažemo da je u konjunktivnoj normalnoj formi (KNF), ako je α oblika:

gde je svaka od formula _jα_i, za 1≤i≤n_j i 1≤j≤k, literal. Za iskaznu formulu α kažemo da je u disjunktivnoj normalnoj formi (DNF), ako je α oblika:

gde je svaka od formula _jα_i, za 1≤i≤n_j i 1≤j≤k, literal.

Primer: Formule (p₁ ∧ ¬p₂ ∧ ¬p₃) ∨ (p₁ ∧ ¬p₄) i (¬p₁ ∧ p₂) ∨ p₁ su u DNF, dok su formule (p₁ ∨ ¬p₂) ∧ (p₂ ∨ ¬p₃) ∧ (p₃ ∨ ¬p₁) i p₂ ∧ (p₃ ∨ ¬p₃) u KNF. Formule p₁ ∧ p₂ ∧ ¬p₃ i p₁ ∨ ¬p₁ istovremeno su i u KNF i u DNF, dok formule p₁ ∨ (p₂ ∧ (p₃ ∨ p₄)) i p₁ ⇒ p₂ nisu ni u KNF ni u DNF. ▲

Primer: U dokazu teoreme o n-arnom vezniku mi smo zapravo konstruisali jednu formulu koja je u DNF i pritom je semantički ekvivalentna formuli ◇(p₁, p₂, …, p_n).

Disjunktivne odnosno konjunktivne normalne forme su pogodne za utvrđivanje da li je neka forma zadovoljiva, odnosno da li neka formula nije tautologija. Naime, ako želimo da pronađemo neku valuaciju koja zadovoljava formulu u DNF, dovoljno je da nađemo valuaciju koja zadovoljava barem jedan disjunkt oblika α₁ ∧ α₂ ∧ … ∧ α_n, što je veoma lako. Ako želimo da dokažemo da neka formula u KNF nije tautologija, dovoljno je da nađemo barem jednu valuaciju koja ne zadovoljava konjunkt oblika α₁ ∨ α₂ ∨ … ∨ α_n.

Šta je s formulama koje nisu ni u KNF ni u DNF? Njih veoma lako možemo transformisati u semantički ekvivalentne KNF ili DNF formule. Naredna dva algoritma opisuju postupak ovih transformacija. Oba algoritma se zasnivaju na tome da su skupovi { ¬, ∧ } odnosno { ¬, ∨ } potpuni sistemi veznika, kao i na osobinama koje su navedene u prethodnoj teoremi.

algoritam KNF
ulaz:     Iskazna formula F
izlaz:    Konjunktivna normalna forma formule F

Eliminisati logičke konstante primenom semantičke ekvivalencije
⊥ ≡ (A ∧ ¬A) i ⊤ ≡ (A ∨ ¬A)

Eliminisati veznik ekvivalencije iz F koristeći semantičku ekvivalenciju
(A ⇔ B) ≡ ((A ⇒ B) ∧ (B ⇒ A))

Eliminisati veznik implikacije iz F koristeći semantičku ekvivalenciju
(A ⇒ B) ≡ (¬A ∨ A)

Dok god je to moguće, unutar F primenjivati De Morganove zakone
¬(A ∧ B) ≡ (¬A ∨ ¬B) i ¬(A ∨ B) ≡ (¬A ∧ ¬B)

Eliminisati dvostruku negaciju iz F primenom semantičke ekvivalencije
¬¬α ≡ α

Dok god je to moguće, unutar F primenjivati zakone distributivnosti
(A ∨ (B ∧ C)) ≡ ((A ∨ B) ∧ (A ∨ C)) i 
((B ∧ C) ∨ A) ≡ ((B ∨ A) ∧ (C ∨ A))

Vratiti F

algoritam DNF
ulaz:     Iskazna formula F
izlaz:    Disjunktivna normalna forma formule F

Eliminisati logičke konstante primenom semantičke ekvivalencije
⊥ ≡ (A ∧ ¬A) i ⊤ ≡ (A ∨ ¬A)

Eliminisati veznik ekvivalencije iz F koristeći semantičku ekvivalenciju
(A ⇔ B) ≡ ((A ⇒ B) ∧ (B ⇒ A))

Eliminisati veznik implikacije iz F koristeći semantičku ekvivalenciju
(A ⇒ B) ≡ (¬A ∨ A)

Dok god je to moguće, unutar F primenjivati De Morganove zakone
¬(A ∧ B) ≡ (¬A ∨ ¬B) i ¬(A ∨ B) ≡ (¬A ∧ ¬B)

Eliminisati dvostruku negaciju iz F primenom semantičke ekvivalencije
¬¬α ≡ α

Dok god je to moguće, unutar F primenjivati zakone distributivnosti
(A ∧ (B ∨ C)) ≡ ((A ∧ B) ∨ (A ∧ C)) i 
((B ∨ C) ∧ A) ≡ ((B ∧ A) ∨ (C ∧ A))

Vratiti F

Primer: Pokažimo primenu algoritama KNF na formulu (p ⇔ q) ∨ (¬r ∧ q):

Iz konjunktivne forme vidimo da formula (p ⇔ q) ∨ (¬r ∧ q) nije tautologija. ▲

Sistemi dedukcije u iskaznoj logici

U prethodnom delu formulisali smo i dokazali sledeće tvrđenje: Γ, α ⊨ β ako i samo ako Γ  ⊨ α ⇒ β. Specijalno, ako je Γ prazan skup, važi:

Ovaj iskaz nam govori da ako tačnost formule α povlači tačnost formule β pri različitim interpretacijama, tada je formula α ⇒ β tautologija. I obrnuto, ako je α ⇒ β tautologija, tada tačnost formule α povlači tačnost formule β.

Dokažimo još jedan sličan iskaz: Ako važi ⊨ α i važi ⊨ α ⇒ β, tada važi i ⊨ β.

Dokaz je sasvim jednostavan. Po prethodnom tvrđenju važi α ⊨ β, pa po definiciji znaka semantičke posledice i znanja da važi ⊨ α, zaključujemo ⊨ β.

Ovakvim iskazima uspostavili smo odnos između istinitosti dve formule i njihove implikacije bez potrebe da ispitujemo istinitost formula tablicom, i bez potrebe traženja modela. U tome nam je pomoglo znanje da su formule bile tautologije. Možemo ovu tvrdnju nazvati deduktivnim pravilom ili pravilom izvođenja. Sada, sa ovako formiranim pravilom, uvek možemo zaključiti da je formula φ tačna pri nekoj valuaciji v ako znamo da su formule ψ i ψ ⇒ φ tačne pri valuaciji v.

Da li bismo mogli na sličan način uspostaviti odnose između formula i za ostale veznike? Verovatno da možemo, ali mi to nećemo raditi. Umesto toga mi ćemo pretpostaviti da važe tvrđenja poput dva koja smo naveli. Uz pomoć takvih tvrđenja mi ćemo izvoditi logičke posledice nekih formula. U ovoj glavi udaljićemo se od semantičkog pogleda na iskaznu logiku, i počećemo da proučavamo odnose među izkaznim formulama iz sintaksnog ugla. U narednoj glavi videćemo kakva je veza između ova dva pogleda.

Od sada, za nas će centrali pojam proučavanja biti deduktivni sistem. Deduktivni sistem 𝓛 čine:

• Alfabet sistema Σ_𝓛 kojeg čine simboli.
• Skup iskaznih formula For_𝓛 nad alfabetom Σ_𝓛.
• Skup aksioma Ax_𝓛 koji je podskup skupa For_𝓛.
• Skup deduktivnih pravila Z_𝓛.

Prva dva sastojka deduktivnog sistema, alfabet teorije i skup iskaznih formula, poznati su nam iz prethodnih razmatranja. Alfabet je proizvoljan neprazan, prebrojiv skup. Skup iskaznih formula podrazumeva skup svih nizova simbola koji se mogu izgraditi konačnom primenom određenih pravila.

Skup aksioma je nov pojam. Aksioma je iskazna formula za koju pretpostavljamo da važi. Iako aksioma ne mora biti u opštem slučaju tautologija, mi ćemo uvek za aksiome uzimati tautologije. Kasnije ćemo videti zašto je ovo bitno za naša razmatranja. Kako je svaka aksioma iskazna formula, skup aksioma Ax_𝓛 je podskup skupa iskaznih formula For_𝓛. Skup aksioma ne mora biti konačan. Za deduktivne sisteme koji imaju konačan skup aksioma kažemo da su konačno aksiomatizabilni. Aksiome deduktivnih sistema koji nisu konačno aksiomatizabilni navode se uz pomoć aksiomatskih šema. Aksiomatska šema predstavlja pravilo po kojem se može generisati beskonačno mnogo aksioma. Deduktivne teorije često nisu konačno aksiomatizabilne, ali zato sadrže konačno mnogo aksiomatskih šema.

Skup deduktivnih pravila čine pravila po kojima iz nekog konačnog skupa iskaznih formula { α₁, α₂, …, α_n } možemo zaključiti, izvesti, novu iskaznu formulu α_n+1. Sama pravila se zapisuju u obliku „razlomka“; iznad crte se navode pretpostavke, a ispod crte se navodi zaključak. Aksiome možemo shvatiti kao pravila koja nemaju pretpostavke.

Sva četiri navedena elementa deduktivnog sistema možemo u potpunosti proizvoljno uzeti, i time konstruisati formalnu teoriju koja nama odgovara. Međutim, interesantni su samo neki od beskonačnog broja mogućih deduktivnih sistema. Mi ćemo u narednom delu ovog teksta upravo opisati one najznačajnije i najkorisnije. Ipak, navešćemo jedan trivijalan deduktivni sistem 𝓣 kao primer.

Primer: Neka je alfabet sistema 𝓣 sačinjen od dva simbola { a, b }. Gramatika sistema 𝓣 zadata je na sledeći način: Simboli a i b su formule sistema 𝓣; Ako je α neka formula sistema 𝓣, tada su αa i αb takođe formule. Dakle, skup svih formula sistema 𝓣 čine svi konačni nizovi simbola a i b. Sistem 𝓣 sadrži dve aksiome: ab i bb. Jedino pravilo dedukcije sistema 𝓣 je pravilo nadovezivanja: ako su nam date formule α i β, tada možemo izvesti formulu αβ. Ovo pravilo ćemo označavati sa N. U opisanom sistemu možemo, na primer, izvesti formulu abbbab nadovezivanjem aksioma određenim redosledom. Međutim, formulu a ne možemo izvesti u ovom sistemu. Štaviše, ne možemo izvesti nijednu formulu koja se završava simbolom a. ▲

U deduktivnim sistemima postoji pojam sintaksne posledice, za razliku od semantičke posledice koju smo do sada koristili. Za neku formulu α kažemo da je sintaksna posledica u deduktivnom sistemu 𝓛, ako formulu α možemo dobiti konačnim brojem primena deduktivnih pravila deduktivnog sistema 𝓛. Tu činjenicu zapisujemo simbolički na sledeći način:

Znak ⊢ nazivamo rampa, a čitavu gornju formulu nazivamo sekvent⁶. Kada je jasno u kom deduktivnom sistemu se radi, možemo izostaviti indeks 𝓛 pored znaka rampe. Za formulu koja je sintaksna posledica aksioma teorije 𝓛, kažemo da je teorema teorije 𝓛. Dokaz teoreme podrazumeva konačan niz iskaznih formula od kojih je svaka aksioma teorije 𝓛 ili je dobijena primenom pravila izvođenja teorije 𝓛 na prethodne članove niza. Prema tome tome izraz ⊢_𝓛 α označava da postoji dokaz formule α u sistemu 𝓛.

Ako postoji efektivna metoda kojom se odlučuje da li je svaka formula i teorema teorije 𝓛, tada za tu teoriju kažemo da je odlučiva. U suprotnom, za teoriju 𝓛 kažemo da je neodlučiva.

Osim aksioma, ponekad koristimo i iskazne formule koje se ne nalaze u skupu aksioma. Tada taj skup navodimo s leve strane rampe i nazivamo ih pretpostavke ili hipoteze, a formulu s desne strane nazivamo deduktivnom posledicom ili zaključkom hipoteza.

Primer: U sistemu 𝓣 opisanom u prethodnom primeru, važi  ⊢_𝓣 abbbab, ali zato ne važi ⊢_𝓣 abbba. Ali, ako bismo pretpostavili formulu a tada bismo mogli da izvedemo formulu abbba, i u tom slučaju pisali bismo a ⊢_𝓣 abbba. ▲

Dokazi se u praksi mogu zapisati na više različitih načina. Najčešće se zapisuju u obliku liste ili stabla. Prilikom prikazivanja dokaza u obliku liste, svaka izkazna formula se piše u novom redu, a pored nje se zapisuje da li je ona aksioma, dodatna pretpostavka ili je dobijena primenom dodatnog pravila (u tom slučaju se piše koje je pravilo primenjeno na koje formule). Prilikom zapisivanja dokaza u obliku stabla, crta se stablo u čijem se vrhu (listovima) nalaze pretpostavke i aksiome, a u korenu zaključak. Čvorovi stabla predstavljaju primene pravila, a pored čvora se u uglastim zagradama navodi ime pravila ili aksiome.

Primer: U nastavku je naveden jedan dokaz sekventa  ⊢_𝓣 abbbab zapisan pomoću liste i stabla:

▲

Iako smo na početku ovog poglavlja motivisali uvođenje deduktivnog pravila koristeći se osobinama semantičke posledice, od sada više nećemo koristiti taj pojam. Više nas neće interesovati istinitosna vrednost samih formula, već njihov sintaksni odnos, tj. mogućnost da se jedna formula izvede od druge, ili obrnuto, primenom deduktivnih pravila. Na formule ćemo od sada gledati čisto kao na nizove simbola, bez potrebe da im pridružimo značenje. Isto tako, deduktivna pravila više nećemo formalno opravdavati koristeći se semantičkom posledicom.

To nas donekle oslobađa ranije predstave o istinitosti iskaza⁷. Naime, deduktivni sistemi s različitim aksiomatskim skupom odgovaraju različitim filozofskim pravcima koji se različito odnose prema pojmu istine. Nama će od interesa biti najviše klasična dvovrednosna logika, s kojom smo do sada radili. U njoj svaki iskaz može biti ili istinit ili lažan, ali ne može biti i istinit i lažan istovremeno. Posledica toga je da nedostatak jednog epiteta povlači postojanje drugog. Tako, ako znamo da neki iskaz nije istinit, onda znamo da je on lažan. I obrnuto, ako znamo da neki iskaz nije lažan za njega ćemo reći da je istinit. Osim klasične logike, postoje još mnoge logike, a nama će biti od interesa samo još intuicionistička logika. Nasuprot klasičnoj logici, u intuicionističkoj logici iskazi ne moraju biti istiniti niti lažni, već mogu imati vrednost neodređenosti. Posledica toga je da ne možemo više nešto zaključiti o istinitosti iskaza samo na osnovu znanja da on nije tačan ili znanja da on nije istinit. Kao što ćemo videti, intuicionistička logika ne priznaje neke principe klasične logike. Takođe, svi dokazi intuicionističke logike biće validni u klasičnoj logici, ali ne i obrnuto.

Pojam deduktovnog sistema je stvoren radi formalnog proučavanja dokaza. Pojam dokaza je centralan u matematici i javlja se još kod antičkih Grka. Međutim, dokazi starih Grka, zapisani na prirodnom jeziku, daleko su bili od bilo kakvih dokaza sprovedenih u formalnim sistemima. Prve nagoveštaje onoga što danas nazivamo deduktivnim sistemom, dao je Lajbnic ⁸ tokom sedamnaestog veka. Lajbnic je verovao da se proces razmišljanja može svesti na nekakvu vrstu računa. Ipak bilo je potrebno još nekoliko stotina godina, da bi se Lajbnicove ideje sprovele u delo.

Prvi deduktivni sistem bio je Fregeov⁹ sistem izložen u knjizi Begriffsschrift¹⁰ iz 1879. godine. Fregeove ideje su imale jak uticaj na matematičare poput Hilberta¹¹ i Rasela¹², koji su početkom dvadesetog veka pokušali da zasnuju čitavu matematiku (ili barem geometriju i aritmetiku) uz pomoć deduktivnih sistema. U nastavku teksta biće izložen Hilbertov deduktivni sistem, kao i Račun prirodne dedukcije, koji je nastao tridesetih godina prošlog veka.

Hilbertov sistem

U literaturi su opisani mnogi deduktivni sistemi, nazvani po Hilbertu, koji imaju male razlike (najčešće u izboru aksioma). Svi oni se uglavnom odlikuju velikim brojem aksioma, i malim brojem deduktivnih pravila. Sistem koji je opisan u nastavku poznat je pod imenom Lukašievičev formalni sistem. U ovom sistemu se koriste samo veznici negacije i implikacije.

Lukašievičev deduktivni sistem ℋ ima tri aksiomatske šeme:

1. ϕ ⇒ (ψ ⇒ ϕ)
2. (ϕ ⇒ (ψ ⇒ χ)) ⇒ ((ϕ ⇒ ψ) ⇒ (ϕ ⇒ χ))
3. (¬ϕ ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ)

Jedino pravilo izvođenja u ℋ je modus ponens koje glasi: Ako su nam poznate formule ψ i ψ ⇒ ϕ, tada možemo zaključiti formulu ϕ.. Simbolički zapisano:

Dokazi u Hilbertovim sistemima zapisuju se u obliku liste.

Primer: U Lukašievičevom sistemu možemo dokazati da važi ⊢_ℋ p ⇒ p.

▲

U navedenom primeru iz praznog skupa pretpostavki dokazana je formula p ⇒ p. Sledeći primer ilustruje kako se mogu načiniti dodatne pretpostavke, a zatim dokazati željena formula.

Primer: p ⇒ r, p ⇒ (r ⇒ q) ⊢_ℋ p ⇒ q.

▲

Hilbertovi sistemi su jednostavni po svojoj konstrukciji. Međutim, dokazi u njima nisu jednostavni niti oponašaju prirodan način rezonovanja. Zbog toga se u dvadesetim godinama dvadesetog veka javlja jaka potreba za sistemom dedukcije koji će bolje opisati prirodan proces zaključivanja.

Prirodna dedukcija

Račun prirodne dedukcije uveli su, nezavisno jedan od drugog, Gerhard Gencen¹³ i Stanislav Jaskovski¹⁴.

Kao i kod Hilbertovih sistema, u literaturi se nalaze različite ali veoma slične definicije ovog sistema. Prirodnu dedukciju odlikuju velik broj pravila izvođenja i mali broj aksioma. Najčešće se u prirodnoj dedukciji koriste logički veznici ∧, ∨, ⇒, ¬ i logička konstanta ⊥.

Za svaki veznik u prirodnoj dedukciji postoje pravila za eliminaciju i pravila za uvođenje (introdukciju) tog veznika. Osim ovih pravila, postoji još jedno pravilo, Ex falso quodlibet. U prirodnoj dedukciji klasične logike postoji i jedna aksiomatska šema Tertium non datur koja se ne nalazi u prirodnoj dedukciji intuicionističke logike. Prirodna dedukcija intuicionističke logike ne sadrži aksiomatske šeme. Osim ove razlike, prirodna dedukcija za klasičnu logiku i prirodna dedukcija za intuicionističku logiku su identične.

Za razliku od Hilbertovog sistema, prilikom rada u sistemu prirodne dedukcije moguće je koristiti iskaze koji ranije nisu dokazani. Takve iskaze nazivamo dodatne pretpostavke. Svaku dodatnu pretpostavku moramo zatvoriti pre kraja dokaza korišćenjem odgovarajućeg pravila. Otvaranjem i zatvaranjem dodatne pretpostavke mi definišemo poddokaz, tj. dokaz unutar dokaza.

U jednom dokazu možemo imati i više poddokaza, ali se ti poddokazi ne smeju preklapati osim u slučaju kada je jedan poddokaz ujedno i poddokaz drugog poddokaza (dakle, ceo se sadrži u njemu). Sve što smo dokazali pre otvaranja poddokaza možemo koristiti unutar poddokaza, ali ono što smo dokazali unutar poddokaza ne smemo koristiti van tog poddokaza. Zaključak poddokaza, tj. formulu koju smo izveli zatvaranjem poddokaza možemo slobodno koristiti u nastavku dokaza.

Originalno, Gencen je dokaze zapisivao u obliku stabla. Uz ovakvo zapisivanje dokaza, lako je pratiti zavisnost dokazanih iskaza od pretpostavljenih. Međutim, crtanje stabla nije praktično za duže i komplikovanije dokaze. Često se prilikom crtanja stabla dokazi nekih iskaza ponavljaju, što dovodi do nepotrebnog uvećavanja stabla.

Za razliku od Gencena, Jaskovski je preferirao linearni zapis dokaza. U nastavku ovog poglavlja dokaze ćemo davati u Fičovom¹⁵ zapisu, koji se zasniva na notaciji koju je koristio Jaskovski. U ovakvom zapisu dokazi su dati u vidu numerisane liste. U svakom redu liste nalazi se tačno jedna iskazna formula pored koje je navedeno da li je ta formula pretpostavka, dodatna pretpostavka, ili je dobijena primenom nekog pravila na prethodne formule (u tom slučaju se navodi skraćeno ime tog pravila, kao i redni brojevi formula na koje je pravilo primenjeno). Ako se u nekom trenutku u dokazu uvede dodatna pretpostavka, tada se s leve strane liste dopisuje crta koja se spušta sve dok se dodatna pretpostavka ne oslobodi primenom nekog pravila.

Sada ćemo detaljno opisati svako pravilo prirodne dedukcije.

Konjunkcija

Kao i za svaki veznik, za konjunkciju imamo dve vrste pravila: pravila za eliminaciju i pravila za uvođenje konjunkcije.

Pravilo za introdukciju konjunkcije govori nam da ako znamo da važe formule α i β, tada znamo da važi i njihova konjunkcija α ∧ β. Ovo pravilo zapisujemo na sledeći način:

Za eliminaciju konjunkcije postoje dva (slična) pravila. Prilikom primene prvog pravila iz konjunkcije α ∧ β možemo da zaključimo levi konjunkt α. Slično, prilikom primene drugog pravila možemo zaključiti desni konjunkt.

Disjunkcija

Pravila uvođenja disjunkcije pokazuju nam da iz formule α možemo zaključiti formulu α ∨ β, gde je β proizvoljna formula. Kao i za eliminaciju konjunkcije, i pravilo za uvođenje disjunkcije ima svoj L i R oblik

Pravilo za eliminaciju disjunkcije donekle je komplikovanije od dosadašnjih pravila. Ako želimo da u našem dokazu iz α ∨ β izvedemo γ moramo ispitati dva posebna slučaja, tj. napraviti dva dodatna poddokaza. U prvom poddokazu pretpostavljamo α i iz toga izvodimo zaključak γ. U drugom poddokazu pretpostavljamo β i iz toga izvodimo γ. Tek tada, primenjujući pravilo na disjunkciju, i navedene dokaze, možemo zaključiti γ.

Implikacija

Pravilo eliminacije implikacije je ništa drugo nego svima dobro poznat modus ponnens. Ono nam govori da ako znamo da iz α sledi β, i znamo još da važi α, tada možemo zaključiti β.

Uvođenje implikacije sastoji se iz uvođenja dodatne pretpostavke α. Kada uz pomoć te pretpostavke uspemo da dokažemo željenu formulu β, možemo zaključiti da važi α ⇒ β, i pri tom poddokaz zatvoriti.

Napominjemo, opet, da van poddokaza u kom smo pretpostavili α i dokazali β, u opštem slučaju ne možemo se pozivati na formule α ili β, već samo na implikaciju α ⇒ β.

Negacija

Upotrebom pravila eliminacije negacije na formulu i njenu negaciju, dobijamo kontradikciju.

Pravilom uvođenja negacije iz poddokaza koji se završava kontradikcijom možemo zaključiti negaciju dodatne pretpostavke kojom je započet poddokaz.

Pravilom eliminacije kontradikcije, Ex falso quodlibet, koje ne deluje ni na jedan veznik, uklanjamo kontradikciju zamenjujući je bilo kojom formulom.

Tertium non datur

Kao što smo spomenuli ranije, u sistemu prirodne dedukcije za klasičnu logiku nalazi se i jedna aksiomatska šema. Ona se naziva tertium non datur (isključenje trećeg) i glasi:

Aksiomatsku šemu uvek možemo iskoristiti u bilo kom delu dokaza za bilo koju dobro formiranu formulu α. Ona nam govori da formula α može važiti ili ne važiti (treća mogućnost se isključuje), baš onako kako se klasična logika odnosi prema istinitosnim vrednostima.

Često se u matematici koristi oblik dokaza poznat pod nazivom Dokaz kontradikcijom. Ovaj dokaz ima sledeću formu:

Da bismo dokazali φ, dovoljno je da pretpostavimo ¬φ, a zatim izvedemo kontradikciju.

Dokaz kontradikcijom je validan u klasičnoj logici jer iz φ ∨ ¬φ lako možemo izvesti φ koristeći pravila eliminacije disjunkcije, uvođenja negacije i eliminacije kontradikcije (videti disjunktivne silogizme u nastavku teksta). U intuicionističkoj logici, ovakva forma dokaza nije dozvoljena, jer intuicionistička logika ne priznaje zakon isključenja trećeg. Ipak, u intuicionističkoj logici je validan Dokaz negacijom, koji ima sledeću formu:

Da bismo dokazali ¬φ, dovoljno je da pretpostavimo φ, a zatim izvedemo kontradikciju.

Gornja forma se oslanja samo na pravilo uvođenja negacije koje je validno u intuicionističkoj logici.

Često se ove dve forme dokaza poistovećuju iako nisu iste. Razlog njihovog poistovećivanja je intuicija razvijena u klasičnoj logici po kojoj možemo skraćivati duplu negaciju. U intuicionističkoj logici, sekvent ¬¬φ ⊢ φ nije moguće dokazati.

Izvedena pravila

Često dokazi u sebi sadrže delove koji su veoma slični. Zbog toga je korisno formulisati dodatna, izvedena pravila koja znatno skraćuju dokaz. Formalno gledano, u dokazima se smeju koristiti samo pravila koja su navedena prilikom definisanja deduktivnog sistema, ali je intuitivno jasno da se svaka primena dodatnog pravila, može opravdati „raspisivanjem“ dokaza dodatnog pravila. Naredna pravila nisu navedena prilikom definisanja deduktivnog sistema baš zbog toga što se mogu izvesti iz ostalih, a poželjno je da skup pravila (kao i skup aksioma) bude što manji.

Modus tollens i kontrapozicija su pravila koja se često koriste u matematičkim dokazima. Modus tollens nam govori da ako znamo da važe formule α ⇒ β i ¬β, tada možemo zaključiti da važi ¬α. Slično tome, kontrapozicija nam govori da ako znamo da važi implikacija α ⇒ β, tada možemo zaključiti da važi implikacija ¬β ⇒ ¬α.

Dokaz pravila modus tollens:

Veznik implikacije ima osobinu tranzitivnosti. Ova osobina se iskazuje sledećim pravilom:

Za veznik negacije, vezana su pravila uvođenja i eliminacije dvostruke negacije:

Izvođenje pravila uvođenja dvostruke negacije svodi se na upotrebu pravila eliminacije negacije i uvođenja negacije. Pravilo eliminacije negacije zasniva se na upotrebi aksiome tertium non datur.

Ako u prirodnoj dedukciji konjunkciju dve implikacije predstavimo kao uz pomoć veznika ekvivalencije, jednostavno se mogu dokazati pravila uvođenja i eliminacije ekvivalencije:

Disjunktivni silogizam je pravilo klasične logike koje nam dopušta da se lako „rešimo“ disjunkcije ako imamo datu negaciju jednog od disjunkata. Ovo pravilo se lako dokazuje upotrebom aksiome tertium non datur.

Prva dva De Morganova pravila govore nam šta možemo zaključiti iz negacije konjunkcije i iz negacije disjunkcije.

Druga dva De Morganova pravila nam govore šta možemo zaključiti iz konjunkcije dve negacije i iz disjunkcije dve negacije. Kao što možete videti, razlika između narednog i prethodnog para pravila jeste u tome što su pretpostavke i zaključci zamenili mesta.

Navedena pravila se jednostavno dokazuju:

Zanimljivo je da se od sva četiri pravila, samo ¬(α ∧ β) ⊢ ¬α ∨ ¬β ne može dokazati u intuicionističkoj logici¹⁶.

Metateoreme iskazne logike

Čitaoci su nesumnjivo do sada primetili da se tokom ovog teksta često povlačila paralela između prirodnog jezika i iskazne logike. Štaviše, mnogi izrazi poput veznik, alfabet, sintaksa, semantika direktno su preuzeti iz lingvističkih nauka. Razlog tome je taj što smo se mi do sada i bavili nekom vrstom lingvistike. Naime, mi smo napravili veštački jezik definišući njegov alfabet, reči i način građenja rečenica (za nas su to formule). Zatim smo pokazali kako rečenice (formule) oslikavaju logičku strukturu u prirodnom jeziku, i pokazali smo kako je moguće zaključivati na čistom jeziku iskazne logike bez potrebe prevođenja rečenica na prirodni jezik (upotrebom deduktivnog sistema).

Sve ovo smo uspeli da uradimo koristeći srpski jezik (koji je poznat svima koji ovo čitaju). Za srpski jezik reći ćemo da je metajezik, jer smo uz pomoć njega opisali drugi jezik. Za jezik koji smo konstruisali uz pomoć metajezika, a u ovom slučaju to je jezik iskazne logike, reći ćemo da je objektni jezik.

Ni metajezik ni objektni jezik nisu morali da budu baš srpski jezik i jezik iskazne logike. Isti ovaj rad mogli smo da napišemo na engleskom ili španskom. Isto tako, mogli smo da opišemo jezik nekakve sasvim druge logike. Takođe, objektni jezik uopšte ne mora biti veštački jezik, niti metajezik mora biti prirodni. Tako, na primer, u gramatici grčkog jezika koja je napisana na srpskom, metajezik je srpski, a objektni jezik je grčki. S druge strane, računari koriste formalne opise prirodnih jezika, kako bi s tim jezicima uspešno radili.

Ovakvo razdvajanje pojma metajezika od objektnog jezika povlači sa sobom razdvajanje pojma metateorema od pojma teorema sistema 𝓛. Metateoreme su one teoreme koje govore o osobinama formalnog sistema. Takve teoreme su formulisane i dokazane korišćenjem metajezika. Za razliku od njih, teoreme teorije 𝓛 su formulisane i dokazane unutar same teorije 𝓛.

Nama će biti interesantne metateoreme koje govore o potpunosti i neprotivrečnosti sistema prirodne dedukcije. Za neki formalni sistem reći ćemo da je potpun ako se u njemu svaka tautologija može dokazati. Suprotno tome, za formalne sisteme u kojima je svaka dokazana tvrdnja tautologija, reći ćemo da su saglasni (neprotivrečni, konzistentni).

Neke metateoreme govore i o odnosima dva formalna sistema. Tako, na primer, može se lako dokazati da su Hilbertov sistem i račun prirodne dedukcije za klasičnu logiku, dati u ovom tekstu, ekvivalentni tj. sve što se može dokazati u prvom može se dokazati i u drugom¹⁷.

U nastavku će biti navedene metateoreme koje se odnose na račun prirodne dedukcije klasične logike.

Teorema saglasnosti Ako Γ ⊢ α onda Γ ⊨ α.

Dokaz: Dokaz tvrđenja ćemo izvršiti indukcijom po dužini dokaza formule. Prvo ćemo tvrđenje dokazati za dokaze dužine jedan, a zatim ćemo iz pretpostavke da tvrđenje važi za dokaze dužine k, dokazati da tvrđenje važi za dokaze dužine k + 1.

Pretpostavimo da je iskazna formula α sintaksna posledica skupa formula Γ i da je njen dokaz dužine 1. To znači da α ∈ Γ ili je formula α aksioma, pa tvrđenje Γ ⊨ α trivijalno sledi.

Pretpostavimo sada da tvrđenje važi za sve formule koje imaju dokaz dužine k. Neka se formula α može dokazati dokazom dužine k + 1. Tada je iskazna formula α dobijena primenom jednog od pravila prirodne dedukcije na formule δ₁, δ₂, …, δ_l koje imaju dokaz dužine najviše k. Razlikovaćemo slučajeve u zavisnosti od toga koje je pravilo poslednje primenjeno na neke od formula iz skupa Δ = { δ₁, δ₂, …, δ_l }.

Ako je poslednje primenjeno pravilo uvođenja konjunkcije, tada je formula α oblika δ_i ∧ δ_j, gde za formule δ_i i δ_j po induktivnoj pretpostavci važi v ⊨ δ_i i v ⊨ δ_j za svaku valuaciju v koja zadovoljava skup Γ. Prema tome, važi i Γ ⊨ α.

Ako je poslednje primenjeno pravilo eliminacije konjunkcije, tada je formula α dobijena iz formule δ_i koja ima oblik α ∧ ε ili ε ∧ α. Kako je po induktivnoj pretpostavci Γ ⊨ δ_i, sledi da Γ ⊨ α.

Ako je poslednje primenjeno pravilo uvođenja disjunkcije, tada je formula α oblika δ_i ∨ ε ili ε ∨ δ_j, gde po induktivnoj pretpostavci važi Γ ⊨ δ_j, i ε je proizvoljna iskazna formula. Prema tome, Γ ⊨ α.

Ako je poslednje primenjeno pravilo eliminacije disjunkcije, tada je formula α dobijena iz formule δ_j koja je oblika ε₁ ∨ ε₂, gde važi Γ, ε₁ ⊢ α i Γ, ε₂ ⊢ α. Ako za neku valuaciju v važi v ⊨ Γ, tada po induktivnoj pretpostavci važi v ⊨ ε₁∨ ε₂, tj. v ⊨ Γ ∪ { ε₁ } ili v ⊨ Γ ∪ { ε₂ }. U bilo kom slučaju v ⊨ α, tj. Γ ⊨ α.

Ako je poslednje primenjeno pravilo uvođenja implikacije, tada je formula α oblika ω ⇒ ψ. Jasno je da se dokaz sekventa Γ ⊢ α lako može transformisati u dokaz sekventa Γ, ω ⊢ ψ koji je dužine k. Neka je v proizvoljna valuacija koja zadovoljava skup Γ. Ako v zadovoljava i ω, tada v ⊨ Γ ∪ { ω } pa po induktivnoj pretpostavci v ⊨ ψ, iz čega sledi v ⊨ ω ⇒ ψ. Ako v ne zadovoljava ω, tada trivijalno sledi da v ⊨ ω ⇒ ψ. Dakle, Γ ⊨ α.

Ako je formula dobijena upotrebom pravila eliminacije implikacije, onda je formula α dobijena primenom pravila eliminacije implikacije na formule δ_i i δ_j, gde je formula δ_j oblika δ_i ⇒ α. Kako po induktivnoj pretpostavci znamo da Γ ⊨ δ_i i Γ ⊨ δ_j, sledi da Γ ⊨ α.

Ako je u poslednjem koraku iskorišćeno pravilo uvođenja negacije, tada je formula α oblika ¬ε i važi sekvent Γ, ε ⊢ ⊥. Ako bi za neku valuaciju v koja zadovoljava Γ važilo i v ⊨ ε, tada bi po induktivnoj pretpostavci važilo v ⊨ ⊥, što je nemoguće. Dakle, za svaku valuaciju v koja zadovoljava Γ važi v ⊨ ¬ε, iz čega sledi Γ ⊨ α.

Ako je u poslednjem koraku iskorišćeno pravilo eliminacije negacije, tada je formula α logička konstanta ⊥. Kako je pravilo eliminacije negacije primenjeno na formulu oblika ε ∧ ¬ε, sledi da u dokazu formule α postoje dokazi sekvenata Γ ⊢ ε i Γ ⊢ ¬ε. Ako neka valuacija v zadovoljava Γ, tada bi ona po induktivnoj pretpostavci zadovoljavala formulu ε ∧ ¬ε. Međutim, to je nemoguće. Dakle, Γ ⊨ ⊥.

Ako je u poslednjem koraku iskorišćeno pravilo eliminacije kontradikcije, tada u dokazu formule α postoji dokaz sekventa Γ ⊢ ⊥. Po indukcijskoj pretpostavci Γ ⊨ ⊥, što znači da ne postoji nijedna valuacija v koja zadovoljava skup Γ. Prema tome, svaka valuacija koja zadovoljava Γ zadovoljavaće i α, tj. Γ ⊨ α.

Kako smo ispitali sve moguće slučajeve, i u svakom došli do željenog zaključka, dokaz smatramo završenim. □

Kontrapozitivni oblik teoreme o saglasnosti poznat je kao:

Teorema o neprotivrečnosti: Ako Γ ⊭ α onda Γ ⊬ α.

Teoremu o potpunosti prirodne dedukcije dokazaćemo koristeći teoremu o kompaktnosti. Teorema kompaktnosti tvrdi da je skup iskaznih formula Γ zadovoljiv ako i samo ako je svaki konačan podskup Γ₀ od Γ zadovoljiv. Za skupove iskaznih formula koji imaju osobinu da je njihov svaki konačan podskup zadovoljiv kažemo da su konačno zadovoljivi. Prema toj definiciji, teorema kompaktnosti mogla bi da glasi ovako: skup Γ je zadovoljiv ako i samo ako je konačno zadovoljiv. Pre dokaza teoreme kompaktnosti, dokažimo sledeću lemu.

Lema: Neka je skup iskaznih formula Γ konačno zadovoljiv, i α proizvoljna iskazna formula. Tada je ili Γ ∪ { α } ili Γ ∪ { ¬α } konačno zadovoljiv skup.

Dokaz: Pretpostavimo suprotno, da je Γ konačno zadovoljiv i Γ ∪ { α } i  ∪ { ¬α } nisu konačno zadovoljivi. Iz pretpostavke da Γ ∪ { α } nije konačno zadovoljiv sledi da postoji konačan podskup Γ₁ od Γ za koji važi da Γ₁ ∪ { α } nije konačno zadovoljiv. Prema tome, svaka valuacija v koja zadovoljava Γ₁ mora zadovoljavati formulu ¬α. Sličnim postupkom, iz pretpostavke da Γ ∪ { ¬α } nije konačno zadovoljiv, zaključujemo da postoji konačan podskup Γ₂ od Γ takav da svaka valuacija koja zadovoljava Γ₂ zadovoljava i formulu α. Neka je Δ unija skupova Γ₁ i Γ₂. Kako su skupovi Γ₁ i Γ₂ konačni, konačan je i skup Δ. Kako je Δ podskup od konačno zadovoljivog skupa Γ, sledi da postoji valuacija w takva da zadovoljava Δ. Iz toga sledi da w zadovoljava sve formule iz Γ₁ i sve formule iz Γ₂. Međutim, to je nemoguće jer bi tada w zadovoljavalo istovremeno formule α i ¬α. Prema tome, pretpostavka da Γ ∪ { α } ili Γ ∪ { ¬α } nisu konačno zadovoljivi je pogrešna. □

Teorema kompaktnosti: Skup iskaznih formula Γ je zadovoljiv ako i samo ako je konačno zadovoljiv.

Dokaz: Jedan smer tvrđenja je trivijalan: iz pretpostavke da je Γ zadovoljiv direktno sledi da je Γ konačno zadovoljiv. Pretpostavimo zato da je Γ konačno zadovoljiv. Konstruišimo 𝒫, kolekciju svih konačno zadovoljivih skupova koji sadrže Γ:

Skup 𝒫 nije prazan jer Γ pripada njemu. Relacija inkluzije ⊆ je relacija uređenja na skupu 𝒫. Neka je 𝒵 proizvoljan lanac u (𝒫, ⊆). Uniranjem celog lanca 𝒵 dobijamo novi skup:

Skup L je konačno zadovoljiv jer za svaki njegov konačan podskup { α₁, α₂, …, α_k } postoje skupovi A₁, A₂, …, A_k takvi da važi α₁ ∈ A₁, α₂ ∈ A₂, …, α_k ∈ A_k i konačno zadovoljiv A_j u lancu takav da A₁, A₂, …, A_k ⊆ A_j.

Skup Γ je podskup skupa L. Prema tome, L ∈ 𝒫. Kako za svako A ∈ 𝒵 važi A ⊆ L, sledi da je L gornje ograničenje lanca 𝒵. Prema Cornovoj lemi¹⁸ u strukturi (𝒫, ⊆) postoji maksimalan element. Obeležimo ga sa M. On je takođe konačno zadovoljiv. Po prethodnoj lemi, za svaku formulu α važi da je M ∪ { α } konačno zadovoljiv ili je M ∪ { ¬α } konačno zadovoljiv. Kako je element M maksimalan u lancu, za svaku formulu α važi α ∈ M ili ¬α ∈ M. Koristeći skup M, sada možemo definisati valuaciju w za sva iskazna slova na sledeći način:

Ako dokažemo da w ⊨ M, tada će slediti da w ⊨ Γ jer važi Γ ⊆ M, i time će dokaz da je Γ zadovoljiv skup iskaznih formula biti završen. Poslednji korak u dokazu izvršićemo dokazom po složenosti formule. Dokažimo da za svaku formulu α važi w ⊨ α ako i samo ako α ∈ M.

Baza indukcije trivijalno važi po definiciji valuacije w.

Pretpostavimo da tvrđenje važi za sve formule koje su složenosti ne veće od n i neka je formula α složenosti n + 1. Tada razlikujemo narednih pet slučajeva:

1. Formula α je oblika ¬β. Valuacija w će zadovoljavati α ako i samo ako je w(β) = 0, a to će se desiti (po indukcijskoj pretpostavci) samo ako je β ∉ M, što znači da ¬β ∈ M. Dakle, w zadovoljava α ako i samo ako α ∈ M.
2. Formula α je oblika φ ∧ ψ. Pretpostavimo da w ⊨ α. To znači da w ⊨ φ i w ⊨ ψ. Ako φ ∧ ψ ∉ M, tada ¬(φ ∧ ψ) ∈ M, a kako je M konačno zadovoljiv, mora postojati valuacija koja zadovoljava skup { φ, ψ, ¬(φ ∧ ψ) }. Takva valuacija ne postoji, pa prema tome, mora biti da α ∈ M. Da bismo dokazali drugi smer tvrđenja, pretpostavimo da α ∈ M. Pretpostavimo dodatno da φ ∉ M ili ψ ∉ M. Ako φ ∉ M, tada ¬φ ∈ M, ali skup { ¬φ, φ ∧ ψ } ne može biti zadovoljiv. Prema tome, φ ∈ M. Na potpuno isti način zaključujemo da ψ ∈ M. Po induktivnoj pretpostavci, w ⊨ φ i w ⊨ ψ, pa važi w ⊨ φ ∧ ψ.
3. Formula α je oblika φ ∨ ψ. Neka w ⊨ α i neka φ ∨ ψ ∉ M. Tada mora postojati valuacija koja zadovoljava skup { φ, ¬(φ ∨ ψ) } ili skup { ψ, ¬(φ ∨ ψ) }. Međutim, to je nemoguće. Dakle, α ∈ M. Ako α ∈ M, tada mora barem jedna od formula φ i ψ pripadati takođe skupu M. Kako po indukcijskoj pretpostavci sledi da w ⊨ φ ili w ⊨ ψ, zaključujemo da w ⊨ φ ∨ ψ.
4. Formula α je oblika φ ⇒ ψ. Ako w ⊨ α, tada w ⊨ ψ. Formula α mora pripadati skupu M, jer bi u suprotnom postojala valuacija koja zadovoljava skup { ψ, ¬(φ ⇒ ψ) }. Ako α pripada skupu M, tada i formula ψ mora pripadati skupu M. Odavde, po indukcijskoj pretpostavci sledi da w ⊨ α.
5. Formula α je oblika φ ⇔ ψ. Kako je formula φ ⇔ ψ semantički ekvivalentna formuli (φ ⇒ ψ) ∧ (ψ ⇒ φ), tvrđenje sledi na osnovu dokaza drugog i četvrtog slučaja.

Dakle, w zaista zadovoljava skup M, a time i skup Γ. □

Pre nego što dokažemo samu teoremu slabe potpunosti, uvešćemo novu notaciju i dokazaćemo dve leme koje će nam pomoći pri dokazivanju teoreme saglasnosti. Uvedimo sledeću oznaku: Ako je v neka valuacija, i α dobro formirana formula, tada:

Lema: Za svaki veznik ⋆ ∈ { ∧, ∨, ⇒, ⇔ } i svaku valuaciju v važi:

Dokaz: Za dokazivanje gornjeg tvrđenja potrebno je za svaki veznik dokazati četiri različita sekventa. Prepuštamo to čitaocu. □

Lema: Neka iskazna formula α sadrži iskazna slova p₁, p₂, …, p_n (ne nužno sva). Tada za svaku valuaciju v važi:

Dokaz: Dokaz ćemo sprovesti indukcijom po složenosti formule. Baza indukcije čini dokaz za formule složenosti 1, a to su iskazna slova. Za njih tvrđenje trivijalno važi.

Pretpostavimo sada da tvrđenje važi za formule složenosti manje ili jednake sa k. Neka je formula α složenosti k + 1. Tada razlikujemo dva slučaja:

Neka je formula α oblika ¬β, gde je β formula složenosti k. Ako je I_v(α) = 1 tada je I_v(β) = 0, pa je α^v = α i β^v = ¬β. Kako po pretpostavci važi p₁^v, p₂^v, …, p_n^v ⊢ β^v, sledi da p₁^v, p₂^v, …, p_n^v ⊢ ¬β, a kako je α = ¬β, važi p₁^v, p₂^v, …, p_n^vv ⊢ α. Ako je I_v(α) = 0 tada je I_v(β) = 1, pa je α^v = ¬α i β^v = β. Tada iz induktivne pretpostavke p₁^v, p₂^v, …, p_n^v ⊢ β pravilom uvođenja dvostruke negacije važi p₁^v, p₂^v, …, p_n^v ⊢ ¬¬β, pa kako je α = ¬β, sledi p₁^v, p₂^v, …, p_n^v ⊢ ¬α.

Neka je formula α u obliku β⋆γ, gde ⋆ ∈ { ∧, ∨, ⇒, ⇔ }, pri čemu tvrđenje važi za formule β i γ (po induktivnoj pretpostavci). Tada po prethodnoj lemi p₁^v, p₂^v, …, p_n^v ⊢ (β⋆γ)^v. □

Uz dokazanu lemu, sada možemo lako da dokažemo teoremu saglasnosti.

Teorema slabe potpunosti: Ako ⊨ α onda ⊢ α.

Dokaz: Neka je iskazna formula α tautologija. Tada za svaku valuaciju v važi I_v(α) = 1 tj. α^v = α i prema prethodnoj lemi p₁^v, p₂^v, …, p_n^v ⊢ α. Neka je w proizvoljna valuacija. Tada važi p₁^w, p₂^w, …, p_n ⊢ α ili p₁^w, p₂^w, …, ¬p_n ⊢ α, tj. po teoremi dedukcije p₁^w, p₂^w, …, p_n-1^w ⊢ p_n ⇒ α ili p₁^w, p₂^w, …, p_n-1^w ⊢ ¬p_n ⇒ α. To dalje znači da p₁^w, p₂^w, …, p_n-1^w ⊢ α jer je formula ¬p_n ∨ p_n aksiomatska šema. Ponavljajući ovaj proces još n - 1 puta, dolazimo do sekventa ⊢ α, što smo i želeli da pokažemo. □

Teorema jake potpunosti: Ako Γ ⊨ α onda Γ ⊢ α.

Dokaz: Neka važi Γ ⊨ α. Tada po teoremi kompaktnosti postoji konačan skup Γ₀⊆Γ takav da važi Γ₀ ⊨ α. Iz osobina semantičke posledice, sledi da važi γ₁ ∧ γ₂ ∧ … ∧ γ_n ⊨ α, tj. ⊨ γ₁ ∧ γ₂ ∧ … ∧ γ_n ⇒ α. Iz teoreme slabe potpunosti sledi da važi ⊢ γ₁ ∧ γ₂ ∧ … ∧ γ_n ⇒ α, što dalje znači da je Γ₀ ⊢ α na osnovu teoreme dedukcije i pravila uvođenja konjunkcije. Samim tim važi i Γ ⊢ α. Ovim je dokaz završen. □

Kontrapozitivni oblik teoreme jake potpunosti poznat je kao:

Teorema o postojanju modela Ako Γ ⊬ α onda Γ ⊭ α.

Kombinujući teoremu saglasnosti i teoremu jake potpunosti, dobijamo sledeće tvrđenje.

Teorema: Γ ⊨ α ako i samo ako Γ ⊢ α.

Direktna posledica navedene teoreme je:

Teorema: Sistem prirodne dedukcije za klasičnu iskaznu logiku je odlučiva teorija.

Dokaz: Po prethodnoj teoremi, formula α je teorema prirodne dedukcije, ako i samo ako je i tautologija. Metodom istinitosnih tablica možemo efektivno proveriti da li je α tautologija, iz čega sledi da je sistem prirodne dedukcije odlučiva teorija. □

Primetimo da je u mnogim dokazima navedenih metateorema iskorišćeno to da se pravila prirodne dedukcije lepo slažu sa istinitnosnim vrednostima formula. Tačnije, sva pravila prirodne dedukcije su poštovala princip očivanja istinitosti, salva verite, po kojem se od istinitih pretpostavki mora doneti i istinit zaključak. Kao što smo rekli na početku ove glave, pravila dedukcije su mogla biti izabrana proizvoljno, ali za proizvoljne izbore deduktivnih pravila ne bi bilo moguće dokazati metateoreme analogne onima koje smo dokazali. Isto ovo važi i za izbor aksioma: iako aksiome ne moraju biti tautologije, samo će deduktivni sistemi čije su aksiome tautologije posedovati „lepe“ osobine.

Račun sekvenata

Na kraju prošlog poglavlja dokazali smo metateoremu koja nam kaže da je sistem prirodne dedukcije za klasičnu logiku odlučiva teorija. Štaviše, ako malo bolje pogledamo dokaz teoreme slabe potpunosti, videćemo da se u njoj krije algoritam koji daje dokaz svake teoreme prirodne dedukcije. Ipak, ovakav algoritam ima barem dve mane. Prvo, dokazi koji se dobijaju na ovaj način nisu ni nalik onima koji konstruišu ljudi, već su komplikovani i nepotrebno dugački. Drugo, ovaj ili sličan algoritam je nemoguće primeniti na neke druge logike. Na primer, ovakav algoritam ne može „proći” u slučaju intuicionističke logike, jer ta logika ne priznaje zakon isključenja terćeg na kom je pomenuti algoritam zasnovan.

Sve ovo nas navodi u potragu za dodatnom teorijom koja će nam bolje opisati relaciju dokazivosti. Ispostavlja se da je ta teorijia račun sekvenata koju je konstruisao Gerhard Gencen tridesetih godina prošlog veka. Račun sekvenata je zapravo deduktivni sistem u kome se ne radi direktno sa iskaznim formulama, već sa sekventima. Radeći sa sekventima mi proučavamo relaciju sintaksne posledice ⊢ koja je usko vezana sa pojmom dokaza.

Tačnije, u računu sekvenata mi ćemo raditi sa malo opštijim pojmom sekventa. Za nas će od sada sekvent biti izraz oblika X ⊢ Y gde su X i Y multiskupovi¹⁹ iskaznih formula, koji mogu biti i prazni. Ako je X = [α₁,…,α_n] i Y = [β₁,…,β_m] tada izraz X ⊢ Y možemo intutivno svatiti kao
α₁ ∧ … ∧ α_n ⊢ β₁ ∨ … ∨ β_m, gde se ⊢ u poslednjoj formuli može odnositi na sintaksnu posledicu u prirodnoj dedukciji. Ako je X prazan multiskup tada sekvent X ⊢ Y označavamo sa  ⊢ Y i interpretiramo intuitivno kao  ⊢ β₁ ∨ … ∨ β_m, a ako je Y prazan multiskup tada sekvent X ⊢ Y označavamo sa X ⊢ i interpretiramo intuitivno kao ⊢ ¬(α₁ ∧ … ∧ α_n). Ako su oba multiskupa X i Y prazna, tada sekvent X ⊢ Y označavamo sa ⊢ i interpretiramo intuitivno kao ⊥.

Ako su X, Y i Z multiskupovi, izraz oblika X, Y ⊢ Z je skraćeni zapis²⁰ za X ∪ Y ⊢ Z. Analogno se definiše i izraz X ⊢ Y, Z. Multiskupove sa jednim elementom, koji se pritom samo jednom ponavlja, poistovećujemo sa tim elementom, pa tako pišemo A, α ⊢ β umesto A, {α} ⊢ β.

Kao i kod prirodne dedukcije, postoji račun sekvenata za klasičnu i intuicionističku logiku. U računu sekvenata za intuicionističku logiku dozvoljeno je samo raditi sa sekventima oblika X ⊢ α ili X⊢, gde je α neka iskazna formula.

Račun sekvenata, i za klasičnu i za intuicionističku logiku, ima samo jednu aksiomatsku šemu, koju nazivamo inicijalni sekvent:

Deduktivna pravila računa sekvenata mogu se podeliti u dve grupe: logička pravila i strukturalna pravila. Kao što smo već napomenuli u računu sekvenata za intucionističku logiku dozvoljeno je koristiti samo sekvente koji sa desne strane rampe imaju prazan ili multiskup sa jednim elementom (i pritom je višestrukost tog elementa 1). Zbog toga u sistemu intuicionističke logike je potrebno malo izmeniti naredna pravila tako da se sa desne strane rampe svih sekvenata nalazi najviše jedna formula. Koristeći gorenavedenu, „intuitivnu”, intrepretaciju sekventa, motivacija za svako od narednih pravila postaje jasna.

Logička pravila računa sekvenata su pravila koja se odnose na veznike. Svako od ovih pravila uvodi neki od veznika ∧, ∨, ⇒ ili ¬. U računu sekvenata ne postoje pravila eliminacije veznika. Sva logička pravila imaju svoj levi (L) i desni (R) oblik, u zavisnosti od toga na koju stranu relacije ⊢ deluju, odnosno u zavisnosti sa koje strane znaka ⊢ se vrši uvođenje veznika. Pravila ∧_L i ∨_R dolaze u dve varijante koje se razlikuju u tome sa koje strane formule uvode veznik. U dokazima je jasno koja od ove dve varijante je primenjena, pa mi nećemo uvoditi posebne oznake za različite varijante tih pravila.

U računu sekvenata postoje tri strukturalna pravila: slabljenje (eng. weakening), sužavanje (eng. contraction) i sečenje (end. cutting). Pravila slabljenja i sužavanja imaju levi i desni oblik, dok pravilo sečenja ima samo jedan oblik.

Primer: Dokažimo sekvent ⊢ ¬(α∧β) ⇒ ¬α∨¬β.

▲

Prisetimo se da smo na početku ove glave račun sekvenata predstavili kao alat za traženje dokaza. Šta to tačno znači? Jedan od razloga zašto je u računu sekvenata lako tražiti dokaze, je taj što račun sekvenata poseduje samo pravila uvođenja. Iako ovo na prvi pogled deluje kao ograničavajući faktor, zapravo je na ovaj način postignuta veća simetrija u dokazima. Tačnije, stablo dokaza možemo da čitamo na dva načina: odozgo ka dole, i obrnuto, odozdo ka gore. Do sada smo stabla konstruisali i čitali, odozgo ka dole što odgovara dokazima u kojima se, polazeći od aksioma, konstruiše dokaz odgovarajućeg iskaza. Ovaj način konstrukcije dokaza karakterišemo kao sintetički. Ali ako stablo počnemo da gradimo odozdo ka gore, pravila uvođenja veznika sada postaju pravila eliminacije veznika. Prema tome, pri obrunutom čitanju stabla (odozdo ka gore), sva pravila rastavljaju formule na još jednostavnije formule. Dokaz smatramo završenim kada stignemo do aksioma ili dodatnih pretpostavki. Ovaj način interpretacije stabla odgovara analitičkoj konstrukciji dokaza.

Postoji samo jedno pravilo koje „ometa” analitički način konstrukcije dokaza: pravilo sečenja. Jedino kod pravila sečenja u pretpostavkama postoji formula koja se ne pojavljuje u zaključku (kao samostalna formula ili kao potformula neke formule). Ključan Gencenov doprinos teoriji dokaza je njegov dokaz metateoreme Hauptsatz koja kaže da je pravilo sečenja suvišno²¹, odnosno da sve što se može dokazati sa ovim pravilom, može se dokazati i bez njega. Ovo omogućuje mnogo bolje razumevanje dokaza na metateorijskom nivou u računu sekvenata, nego u prirodnoj dedukciji.

Dokaz metatoreme Hauptsatz u suštini daje jedan efektivan postupak²² za eliminaciju pravila sečenja iz dokaza. Međutim, ovoj algoritam je najčešće u praksi neupotrebljiv, jer se njegovom primenom dokazi mogu uvećati i hipereksponencijalno. Ovo ujedno i objašnjava zašto pravilo sečenja zadržavamo iako je suvišno.

Kao što smo napomenuli ranije, samo pravilo sečenja nema osobinu da se u pretpostavkama nalaze samo formule koje se pojavljuju i u zaključku pravila. Kako je to pravilo suvišno, možemo smatrati da sva pravila računa sekvenata imaju tu osobinu. Ovo zapravo znači da za svaku teoremu A ⊢ B računa sekvenata postoji dokaz u kome se pojavljuju samo potformule formula A i B. Ovo svojstvo računa sekvenata u potpunosti opravdava analitičko građenje dokaza. Analitički dokazi su toliko jednostavni, da je lako napraviti program koji će ih graditi. Takvi programi se nazivaju automatski dokazivači teorema, i od sedamdestih godina prošlog veka kada su prvi put konstruisani, pa sve do danas, predstavljaju aktivnu oblast istraživanja moderne matematike…

1. Naziv dobro formirane formule potiče od engleskog jezika, u kome se one zovu well formed formula, i kraće se obeležavaju oznakom wff. ↩
2. Kao što smo već napomenuli, činjenicu da je formula α tautologija obeležavamo sa ⊨ α, a ne sa ∅ ⊨ α kao što bi se očekivalo iz ovog dokaza. ↩
3. Jan Łukasiewicz (1878–1956), poljski logičar i filozof. ↩
4. Henry Maurice Sheffer (1882–1964), američki logičar. ↩
5. Augustus De Morgan (1806–1871), engleski logičar i matematičar. ↩
6. Naziv sekvent je nastao od nemačke reči za niz – Sequenz prilikom prevoda radova Gerharda Gencena na engleski jezik. ↩
7. Između ostalog, sistem 𝓣 je uzet za primer zbog toga što lepo demonstrira ovu činjenicu. Iako nismo znali značenje simbola a i b, mogli smo da izvedemo neke zaključke u ovom sistemu, kao i da opišemo neke od formula koje se ne mogu izvesti bez dodatnih pretpostavki. ↩
8. Gottfried Wilhelm von Leibniz (1646–1716), nemački filozof, matematičar i pravnik. ↩
9. Friedrich Ludwig Gottlob Frege (1848–1925), nemački filozof i matematičar. ↩
10. Zapisivanje pojmova. ↩
11. David Hilbert (1862–1943), nemački matematičar. ↩
12. Bertrand Arthur William Russell (1872–1970), engleski matematičar i filozof. ↩
13. Gerhard Karl Erich Gentzen (1909–1945), nemački matematičar. ↩
14. Stanisław Jaśkowski (1906–1965), poljski logičar. ↩
15. Frederic Brenton Fitch (1908–1987), američki logičar. ↩
16. Jedan od načina dokazivanja ovog tvrđenja zasnivao bi se na konstruisanju modela intuicionističke logike, u kome pravilo ¬(α ∧ β) ⊢ ¬α ∨ ¬β ne važi. Hejtingove algebre se često uzimaju za modele intuicionističke logike. ↩
17. Da bismo dokazali da se svaka teorema Hilbertovog sistema može dokazati u prirodnoj dedukciji, potrebno je i dovoljno dokazati da u prirodnoj dedukciji važe aksiomatske šeme Hilbertovog sistema i pravilo modus ponens. Da bismo dokazali da sve teoreme prirodne dedukcije jesu i teoreme Hilbertovog sistema, prvo je potrebno definisati preslikavanje koje formule s veznicima konjunkcije i disjunkcije preslikava u odgovarajuće formule u kojima figuriše samo veznik implikacije i negacije. Tek onda se može dokazati da sva pravila izvođenja i aksiomatska šema prirodne dedukcije važe i u Hilbertovom sistemu. ↩
18. Cornova lema glasi: Ako u nepraznom, parcijalno uređenom skupu P svaki lanac ima gornje ograničenje, tada u P postoji barem jedan maksimalan element. Cornova lema je ekvivalentna aksiomi izbora (u ZF teoriji skupova). ↩
19. Multiskupovi (eng. multiset) su kolekcije elemenata u kojima, za razliku od skupova, elementi mogu da se ponavljaju. Formalno multiskup 𝔄 može da se definiše kao par (A,m) gde je A skup elemenata koji se pojavljuju u multiskupu, a m: A → ℕ funkcija koja svakom elementu iz A dodeljuje njegovu višestrukost, odnosno odgovarajući broj ponavljanja u multiskupu 𝔄. ↩
20. Unija multiskupova 𝔄 = (A,m_A) i 𝔅 = (B,m_B) je multiskup (A∪B,m), gde je m: A ∪ B → ℕ definisano kao m(x) = m_A(x) + m_B(x) (pritom ako neki od izraza m_A(x) ili m_B(x) nije definisan za njegovu vrednost se uzima 0). ↩
21. Ove ne znači da je pravilo sečenja i izvodljivo iz ostalih pravila. Primene pravila sečenja ne možemo prosto zameniti nekom shemom ostalih pravila, kao što smo to radili u slučaju izvedenih pravila kod prirodne dedukcije. Zbog toga dokaz Gencenove Hauptsatz metateoreme nije trivijalan. ↩
22. Ovaj postupak se satoji u tome da da se svako pojavljivanje pravila sečenja „gura” ka listovima stabla dokaza. ↩

Literatura

1. Kosta Došen, Osnovna logika
2. Nebojša Ikodinović, Uvod u matematičku logiku
3. Andrzej Indrzejczak, Natural Deduction
4. Predrag Janičić, Matematička logika u računarstvu
5. Jan von Plato, The Development of Proof Theory
6. Boban Veličković, Aleksandar Jovanović i Aleksandar Perović, Teorija skupova