Odlučivost

U logici, izraz odlučivo se odnosi na postojanje efektivnog metoda za određivanje pripadnosti skupu formula. Logički sistemi poput iskaznog računa su odlučivi ako pripadnost njihovom skupu logički validnih formula (ili teorema) može efektivno da se odredi. Teorija (skup formula zatvoren u odnosu na logičke posledice) u fiksiranom logičkom sistemu je odlučiva ako postoji efektivni metod za određivanje da li proizvoljne teorije pripadaju teoriji.

Odlučivost i izračunljivost

Kao i kod koncepta odlučivog skupa, definicija odlučive teorije ili logičkog sistema se može dati bilo u terminima efektivnog metoda bilo u terminima izračunljive funkcije. Ova dva se generalno smatraju ekvivalentnim po Čerčovoj tezi. Zaista, dokaz da je logički sistem ili teorija neodlučiva će koristiti formalnu definiciju izračunljivosti da pokaže da odgovarajući skup nije odlučiv skup, a zatim se pozvati na Čerčovu tezu da pokaže da teorija ili logički sistem nije odlučiv bilo kojim efektivnim metodom (Enderton 2001, pp. 206ff.).

Odlučivost logičkog sistema

Svaki logički sistem ima svoju sintaksu, koja između ostalog određuje pojmove formule, i semantiku, koja određuje pojam logičke validnosti. Logički validna formula ili sistem se ponekad nazivaju teoremama sistema, posebno u kontekstu logike prvog reda, gde Gedelova teorema o potpunosti uspostavlja ekvivalenciju između semantičke i sintaksičke posledice. U drugim postavkama, poput linearne logike, relacija sintaksičke posledice (dokazivost) se može koristiti za definisanje teorema sistema.

Logički sistem je odlučiv ako postoji efektivni metod za određivanje da li su proizvoljne formule teoreme logičkog sistema. Na primer, iskazni račun je odlučiv, jer može da se koristi na primer istinitosna tablica kao metod za određivanje da li je proizvoljna iskazna formula logički validna.

Logika prvog reda nije odlučiva u opštem slučaju; specijalno, svaka signatura koja uključuje jednakost i najmanje jedan drugi predikat sa dva ili više argumenata, daje neodlučiv sistem. Logički sistemi koji proširuju logiku prvog reda, kao što su logika drugog reda i teorija tipova, su takođe neodlučivi.

Sa druge strane, monadni predikatski račun je odlučiv. Ovo je sistem logike prvog reda ograničen na signature koje nemaju funkcijske simbole i čiji relacijski simboli (izuzev jednakosti) nikada ne uzimaju više od jendog argumenta.

Neki logički sistemi nisu adekvatno predstavljeni samo skupom teorema. (Na primer, Klinijeva logika uopšte nema teoreme.) U takvim slučajevima se često koriste alternativne definicije odlučivosti logičkog sistema, koje traže efektivni metod za određivanje nečega opštijeg od validnosti formula; na primer, validnost sekvenata ili relacija posledice {(G, A) | G ⊧ A} logike.

Odlučivost teorije

Teorija je skup formula, zatvoren u odnosu na logičku posledicu. Pitanje odlučivosti za teoriju predstavlja pitanje da li postoji efektivna procedura koja, za datu proizvoljnu formulu u signaturi teorije, određuje da li formula pripada teoriji ili ne. Ovaj problem se prirodno javlja kada je teorija definisana kao skup logičkih posledica fiksiranog skupa aksioma. Primeri odlučivih teorija prvog reda su teorija realnih zatvorenih polja, i Presburgerova aritmetika, dok su teorija grupa i Robinsonova aritmetika primeri neodlučivih teorija.

Postoji više osnovnih rezultata izučavanja odlučivosti teorija. Svaka nekonzistentna teorija je odlučiva, jer je svaka formula koja je u njenoj signaturi njena logička posledica, i stoga član teorije. Svaka kompletna rekurzivno prebrojiva teorija prvog reda je prebrojiva. Proširenje odlučive teorije može da bude neodlučivo. Na primer, postoje neodlučive teorije u iskaznom računu, iako je skup valjanosti (najmanja teorija) odlučiv.

Konzistentna teorija koja ima svojstvo da je svako njeno konzistentno proširenje neodlučivo se naziva suštinski neodlučivom. Štaviše, svako konzistentno proširenje će biti suštinski neodlučivo. Teorija polja je neodlučiva, ali ne i suštinski neodlučiva. Robinsonova aritmetika je suštinski neodlučiva, i stoga je svaka konzistentna teorija koja uključuje ili interpretira Robinsonovu aritmetiku takođe (suštinski) neodlučiva.

Primeri odlučivih teorija

Među odlučivim teorijama su (Monk 1976, pp. 234):

• Skup logičkih valjanosti prvog reda u signaturi koja ima samo jednakost, uspostavio Leopold Levenhajm, 1915.
• Skup logičkih valjanosti prvog reda u signaturi sa jednakošću i jednom unarnom funkcijom, uspostavio Erenfojht, 1959.
• Teorija prvog reda celih brojeva sa signaturom sa jednakošću i sabiranjem, poznata i kao Presburgerova aritmetika. Kompletnost uspostavio Mojžeš Presburger, 1929.
• Teorija prvog reda Bulovih algebri, uspostavio Alfred Tarski, 1949.
• Teorija prvog reda algebarski zatvorenih polja date karakteristike, uspostavio Tarski, 1949.
• Teorija prvog reda realnih-zatvorenih uređenih polja, uspostavio Tarski, 1949.
• Teorija prvog reda Euklidske geometrije, uspostavio Tarski, 1949.
• Teorija prvog reda hiperboličke geometrije, uspostavio Švabhojzer, 1959.

Među metodima za uspostavljanje odlučivosti su eliminacija kvantifikatora, kompletnost modela, i Votov test (Vaught).

Primeri neodlučivih teorija

Među neodlučivim teorijama su (Monk 1976, pp. 279):

• Skup logičkih valjanosti u svakoj signaturi prvog reda sa jednakošću i: relacionim simbolom arnosti ne manje od 2, ili dva unarna funkcijska simbola, ili jedan funkcijski simbol arnosti ne manje od dva, uspostavio Trahtenbrot, 1953.
• teorija prvog reda sa sabiranjem, množenjem i jednakošću, uspostavili Tarski i Andžej Mostovski, 1949.
• Teorija prvog reda racionalnih brojeva sa sabiranjem, množenjem i jednakošću, uspostavila Džulija Robinson, 1949.
• Teorija prvog reda grupa, uspostavio Mal'cev, 1961. Mal'cev je takođe ustanovio da su teorija semigrupa i teorija prstena neodlučive. Robinson je 1949. ustanovila da je teorija polja neodlučiva.

Metod interpretabilnosti se često koristi da se dokaže neodlučivost neke teorije. Ako je neodlučivu teoriju T moguće interpretirati u konzistentnoj teoriji S, onda je i S neodlučiva.

Poluodlučivost

Svojstvo teorije ili logičkog sistema, koje je slabije od odlučivosti je poluodlučivost. Teorija je poluodlučiva ako postoji efektivni metod koji će za datu proizvoljnu formulu uvek ispravno reći ako je formula u teoriji, ali će dati ili negativan odgovor ili neće dati odgovora ako formula nije u teoriji. Logički sistem je poluodlučiv ako postoji efektivni metod za generisanje teorema (i samo teorema), takav da će u nekom momentu svaka izabrana teorema biti generisana. Ovo se razlikuje od odlučivosti, jer za poluodlučiv sistem ne mora da postoji efektivna procedura koja proverava da li formula nije teorema.

Svaka odlučiva teorija ili logički sistem je poluodlučiva, ali u opštem slučaju obratno ne važi; teorija je odlučiva ako i samo ako su i ona i njen komplement poluodlučivi. Na primer, skup logičkih valjanosti V logike prvog reda je poluodlučiv, ali ne i odlučiv. U ovom slučaju, to je zato što ne postoji efektivni metod za proizvoljnu formulu A, koji utvrđuje da A nije u V. Slično, skup logičkih posledica svakog rekurzivno prebrojivog skupa aksioma prvog reda je poluodlučiv. Mnogi od primera neodlučivih teorija prvog reda, datih gore imaju ovu formu.

Odlučivost i potpunost

Odlučivost ne treba mešati sa potpunošću. Na primer, teorija algebarski zatvorenih polja je odlučiva ali nije potpuna, dok je skup svih istinitih iskaza prvog reda o nenegativnim celim brojevima u jeziku sa + i × potpun, ali ne i odlučiv.

Vidi još

• Potpunost
• Presburgerova aritmetika
• Alonzo Čerč
• Laslo Kalmar

Literatura

• Zoran Ognjanović, Nenad Krdžavac, Uvod u teorijsko računarstvo, FON, Beograd, 2004.
• Barwise, Jon (1982). „Introduction to first-order logic”. Ur.: Barwise, Jon. Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland. ISBN 978-0-444-86388-1. 
• Chagrov, Alexander; Zakharyaschev, Michael (1997). Modal logic. Oxford Logic Guides. 35. The Clarendon Press Oxford University Press. ISBN 978-0-19-853779-3. MR1464942. 
• Davis, Martin (1958), Computability and Unsolvability, McGraw-Hill Book Company, Inc, New York 
• Enderton, Herbert (2001). A mathematical introduction to logic (2nd izd.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3. 
• Keisler, H. J. (1982). „Fundamentals of model theory”. Ur.: Barwise, Jon. Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam: North-Holland. ISBN 978-0-444-86388-1. 
• Monk, J. Donald (1976), Mathematical Logic, Berlin, New York: Springer-Verlag