Prirodna dedukcija i teorija dokaza

Sintaksička teorija dokaza i razvoj aksiomatskih sistema

• Tranzicija u logici: Nakon izučavanja teorije modela i teorije izračunljivosti, fokus se pomera na sintaksičku teoriju dokaza. Ova grana logike istražuje načine na koje se forme iskaznih formula transformišu prema pravilima zaključivanja kako bi se formirale sekvence po sleđenju.
• Semantika vs. Sintaksa: U ovom kontekstu semantika se privremeno ostavlja po strani. Pretpostavlja se da su tvrdnje o kojima se govori istinite, osim ako nije drugačije naznačeno.
• Aristotelov doprinos: Aristotel je postavio temelje ideje da se nauke moraju organizovati tako da se iz fundamentalnih, principijelnih tvrdnji nužno dedukuju druge istine o svetu.
• Definicija aksiomatskog sistema:   - To je skup iskaza određenog jezika.   - Aksiomi: Podgrupa iskaza koji su istiniti po definiciji i ne dokazuju se.   - Teoreme: Iskazi koji su istiniti jer se mogu izvesti iz aksioma ili već dokazanih teorema pomoću unapred definisanih pravila zaključivanja.   - Dokaz: Postupak demonstracije kako se u konačnom broju koraka od aksioma dolazi do teoreme primenom pravila.
• Problem istinitosti aksioma:   - Tradicionalno (Aristotel), aksiomi su smatrani istinitim zbog svoje samoočiglednosti (npr. zakon neprotivrečnosti).   - Problem: Samoočiglednost je subjektivna kategorija.   - Formalna logika rešava ovo tako što se istinitost u sistemu ne oslanja na iskustvo ili subjektivni utisak, već na definiciju. Aksiomi su "izvor istine" iz kojeg teoreme crpe svoju istinitost.
• Sloboda u formalnoj logici: Logičari imaju slobodu da predlože bilo kakav formalni sistem.   - Primer: Sistem u kojem je aksiom "Ja sam najbogatija osoba na svetu". Važenje ove istine je ograničeno isključivo na taj sistem i ne utiče na spoljašnju realnost (npr. banke).   - Intuicionističke logike: Nastale početkom XX veka kada je grupa logičara ispitala sisteme u kojima ne važi zakon isključenja trećeg ($p \nvdash \neg p$), što je dovelo do smislenih sistema sa specifičnim primenama.

Razvoj prirodne dedukcije i logicizam

• Logicistička ambicija: Autori poput Fregea ($Gottlob ext{ } Frege$), Rasela ($Bertrand ext{ } Russell$) i Vajtheda ($Alfred ext{ } North ext{ } Whitehead$) težili su da pokažu da se cela matematika (aritmetika, geometrija) može izvesti iz minimalnog skupa logičkih aksioma i pravila.
• Odnos aksioma i pravila:   - Sistemi sa malo aksioma zahtevaju veliki broj pravila zaključivanja.   - Sistemi sa mnogo aksioma mogu funkcionisati sa malim brojem pravila (idealno samo jednim).
• Kritika stroge aksiomatizacije: Iako elegantni, sistemi sa mnogo aksioma i jednim pravilom često su bili glomazni, nečitljivi i "neprirodni".
• Nastanak prirodne dedukcije:   - Razvili su je Stanislav Jaskovski ($Stanisław ext{ } Jaśkowski$) i Gerhard Gencen ($Gerhard ext{ } Gentzen$).   - Pristup: Mali broj aksioma, ali veliki broj pravila koja odgovaraju uobičajenom ljudskom rezonovanju.   - Prednost: Lakša za čitanje i razumevanje, mada zahteva kreativnost u izvođenju.
• Notacije prirodne dedukcije:   - Postoje dijagramatske notacije i Gencenovo drveće dokaza.   - U ovom kursu koristi se Lemon-Supizova tabularna notacija ($Lemmon-Suppes$) jer je pogodna za tekstualni prikaz.

Logički nizovi i sintaksička rampa

• Koncept logičkog niza: Služi za prikazivanje relacija sleđenja između dve grupe tvrdnji. Iz prve grupe nužno sledi druga grupa primenom pravila.
• Sintaksička rampa ($\vdash$):   - Leva strana (uspravna): Premise (tvrdnje iz kojih se izvodi).   - Desna strana (vodoravna): Konkluzije (tvrdnje koje se izvode).   - Čitanje: "Iz zadatih premisa sledi određena konkluzija".
• Struktura niza:   - Broj premisa može biti nula ili više (odvajaju se zarezima).   - Broj konkluzija je minimalno jedna.   - Primer: p ightarrow q , eg q ext{ } vdash ext{ } eg p

Tehnika tabularnog dokazivanja

• Zadatak dokazivanja: Pronaći pravila i redosled njihove primene kako bi se premise transformisale u konkluziju.
• Elementi tabele (Primer niza p ightarrow ( q ightarrow r ) , p ightarrow q ext{ } vdash ext{ } p ightarrow r):   1. Broj koraka: Redni broj operacije.   2. Iskaz: Formula u tom koraku.   3. Izvor: Koraci iz kojih se trenutni korak izvodi.   4. Pravilo: Skraćenica pravila koje je primenjeno (npr. A, MPP, KD).   5. Aktivne pretpostavke: Brojevi pretpostavki na kojima počiva istinitost tog koraka (ispisuju se krajnje levo).
• Definicija završenog dokaza: Niz je dokazan kada dođemo do konkluzije, a u tom koraku su aktivne isključivo pretpostavke koje su bile date u samom nizu (bez preostalih uslovnih pretpostavki).
• Strategija: Dokazivanje je eksperimentalno i tendenciozno. Moguće je više puteva do rešenja; ako jedan ne uspe, logičar se vraća unazad i isprobava drugo pravilo (poput učenja šahovskih obrazaca).

Osnovna pravila zaključivanja u prirodnoj dedukciji

Pravilo pretpostavljanja (A)

• Definicija: U bilo kom trenutku može se uvesti bilo koji iskaz kao pretpostavka.
• Dve vrste pretpostavki:   1. Bezuslovne (date) pretpostavke: Zadate su nizom, ne zahtevaju opravdanje.   2. Uslovne pretpostavke (označavaju se sa $[A]$ i uglastim zagradama): Uvode se kao "kredit" za pomoć u dokazu. Moraju se "otpuštati" ili "ubiti" pre kraja dokaza.
• Svaka pretpostavka dobija svoj jedinstveni broj. U budućim koracima, sve pretpostavke koje su korišćene u prethodnim koracima postaju aktivne i za dobijeni iskaz.

Dupla negacija (DN)

• Definicija: Uvođenje ili eliminisanje dvostruke negacije bez promene istinitosti.
• Primeri:   - Uvođenje: p ext{ } vdash ext{ } eg eg p   - Eliminisanje: eg eg p ext{ } vdash ext{ } p
• U prirodnom jeziku: "Nije da nije pohlepan" znači "Pohlepan je".

Modus ponendo ponens (MPP)

• Definicija: Ako imamo implikaciju i afirmaciju njenog antecedensa, zaključujemo na afirmaciju konsekvensa.
• Šema: p ightarrow q , p ext{ } vdash ext{ } q
• Napomene: Afirmiše se ceo antecedens. Čak i negativna tvrdnja (npr. $\neg p$) može biti afirmisana u kontekstu pravila ako se pojavi u identičnom obliku.

Modus tollendo tollens (MTT)

• Definicija: Ako imamo implikaciju i negaciju konsekvensa, zaključujemo na negaciju antecedensa.
• Šema: p ightarrow q , eg q ext{ } vdash ext{ } eg p
• Preciznost: Ako je antecedens već negativan, negacija će rezultirati duplom negacijom koju kasnije treba ukloniti putem DN.

Kondicionalni dokaz (KD)

• Definicija: Pravilo za opravdavanje uslovnih pretpostavki i uvođenje implikacije.
• Postupak: Iskaz dobijen u dokazu stavlja se u konsekvens, a jedna od aktivnih pretpostavki u antecedens. Ta pretpostavka se tada "ubija" (briše iz aktivnih).
• Heuristika: Ako je konkluzija implikacija (p ightarrow r), verovatno će se koristiti KD, a antecedens ($p$) će biti uslovna pretpostavka.

Pravila za konjunkciju (U$\land$ i E$\land$)

• Uvođenje (Uwedge): Iz $p$ i $q$ sledi p wedge q. Korisno ako je konkluzija konjunktivna.
• Eliminisanje (Ewedge): Iz p wedge q možemo izvesti bilo $p$, bilo $q$. Svaki konjunkt zahteva poseban korak u tabeli.

Pravila za disjunkciju (U$\lor$ i E$\lor$)

• Uvođenje (Uvee): Bilo koji iskaz može se proširiti proizvoljnom disjunkcijom (p ext{ } vdash ext{ } p vee z).   - Ovo je "slabo" pravilo jer u dokaz može uvesti potpuno irelevantne (pa i netačne) iskaze, ali je korisno za finalizaciju dokaza.
• Eliminacija (Evee): Najkomplikovanije pravilo. Ako iz oba disjunkta (svakog ponaosob kao uslovne pretpostavke) možemo doći do istog rezultata, taj rezultat sledi iz cele disjunkcije.   - Primer "Tamni vilajet": Sultanova vojska u mraku. Glas kaže: "Ako uzmeš kamenje, kajaćeš se (u ightarrow k); ako ne uzmeš, kajaćeš se (n ightarrow k)". Pošto vojska ili uzima ili ne uzima (u vee n), svakako im sledi kajaće se ($k$).   - Zahteva tri prethodna koraka: disjunkciju te dve grane zaključivanja koje vode ka istom cilju.

Reductio ad absurdum (RAA)

• Definicija: Posredni dokaz. Pretpostavimo suprotno od onoga što želimo da dokažemo (antiteza).
• Postupak: Ako nas antiteza dovede do kontradikcije ($\bot$), npr. q wedge eg q, onda pretpostavljena antiteza mora biti netačna, a njena negacija istinita.
• Pravilo RAA takodje "ubija" uslovnu pretpostavku koja je dovela do kontradikcije.

Supstitucije i izvedena pravila

• Ekvivalencija ($\leftrightarrow$): Tretira se kao konjunkcija dve implikacije (p ightarrow q wedge q ightarrow p). Koristi se oznaka Df (supstitucija po definiciji) umesto posebnog pravila.
• Izvedena pravila: Obrasci koji se mogu dokazati osnovnim pravilima, ali se koriste radi brzine.   - Modus tollendo ponens (MTP): p vee q , eg p ext{ } vdash ext{ } q   - Modus ponendo tollens (MPT): eg ( p wedge q ) , p ext{ } vdash ext{ } eg q   - De Morganova pravila (DM):     - eg ( p vee q ) ext{ } vdash vdash ext{ } eg p wedge eg q     - eg ( p wedge q ) ext{ } vdash vdash ext{ } eg p vee eg q   - Oznaka vdash vdash označava da niz važi u oba smera.