Одлучивост

У логици, израз одлучиво се односи на постојање ефективног метода за одређивање припадности скупу формула. Логички системи попут исказног рачуна су одлучиви ако припадност њиховом скупу логички валидних формула (или теорема) може ефективно да се одреди. Теорија (скуп формула затворен у односу на логичке последице) у фиксираном логичком систему је одлучива ако постоји ефективни метод за одређивање да ли произвољне теорије припадају теорији.

Одлучивост и израчунљивост

Као и код концепта одлучивог скупа, дефиниција одлучиве теорије или логичког система се може дати било у терминима ефективног метода било у терминима израчунљиве функције. Ова два се генерално сматрају еквивалентним по Черчовој тези. Заиста, доказ да је логички систем или теорија неодлучива ће користити формалну дефиницију израчунљивости да покаже да одговарајући скуп није одлучив скуп, а затим се позвати на Черчову тезу да покаже да теорија или логички систем није одлучив било којим ефективним методом (Enderton 2001, pp. 206ff.).

Одлучивост логичког система

Сваки логички систем има своју синтаксу, која између осталог одређује појмове формуле, и семантику, која одређује појам логичке валидности. Логички валидна формула или систем се понекад називају теоремама система, посебно у контексту логике првог реда, где Геделова теорема о потпуности успоставља еквиваленцију између семантичке и синтаксичке последице. У другим поставкама, попут линеарне логике, релација синтаксичке последице (доказивост) се може користити за дефинисање теорема система.

Логички систем је одлучив ако постоји ефективни метод за одређивање да ли су произвољне формуле теореме логичког система. На пример, исказни рачун је одлучив, јер може да се користи на пример истинитосна таблица као метод за одређивање да ли је произвољна исказна формула логички валидна.

Логика првог реда није одлучива у општем случају; специјално, свака сигнатура која укључује једнакост и најмање један други предикат са два или више аргумената, даје неодлучив систем. Логички системи који проширују логику првог реда, као што су логика другог реда и теорија типова, су такође неодлучиви.

Са друге стране, монадни предикатски рачун је одлучив. Ово је систем логике првог реда ограничен на сигнатуре које немају функцијске симболе и чији релацијски симболи (изузев једнакости) никада не узимају више од јендог аргумента.

Неки логички системи нису адекватно представљени само скупом теорема. (На пример, Клинијева логика уопште нема теореме.) У таквим случајевима се често користе алтернативне дефиниције одлучивости логичког система, које траже ефективни метод за одређивање нечега општијег од валидности формула; на пример, валидност секвената или релација последице {(Г, A) | Г ⊧ A} логике.

Одлучивост теорије

Теорија је скуп формула, затворен у односу на логичку последицу. Питање одлучивости за теорију представља питање да ли постоји ефективна процедура која, за дату произвољну формулу у сигнатури теорије, одређује да ли формула припада теорији или не. Овај проблем се природно јавља када је теорија дефинисана као скуп логичких последица фиксираног скупа аксиома. Примери одлучивих теорија првог реда су теорија реалних затворених поља, и Пресбургерова аритметика, док су теорија група и Робинсонова аритметика примери неодлучивих теорија.

Постоји више основних резултата изучавања одлучивости теорија. Свака неконзистентна теорија је одлучива, јер је свака формула која је у њеној сигнатури њена логичка последица, и стога члан теорије. Свака комплетна рекурзивно пребројива теорија првог реда је пребројива. Проширење одлучиве теорије може да буде неодлучиво. На пример, постоје неодлучиве теорије у исказном рачуну, иако је скуп ваљаности (најмања теорија) одлучив.

Конзистентна теорија која има својство да је свако њено конзистентно проширење неодлучиво се назива суштински неодлучивом. Штавише, свако конзистентно проширење ће бити суштински неодлучиво. Теорија поља је неодлучива, али не и суштински неодлучива. Робинсонова аритметика је суштински неодлучива, и стога је свака конзистентна теорија која укључује или интерпретира Робинсонову аритметику такође (суштински) неодлучива.

Примери одлучивих теорија

Међу одлучивим теоријама су (Monk 1976, pp. 234):

Скуп логичких ваљаности првог реда у сигнатури која има само једнакост, успоставио Леополд Левенхајм, 1915.
Скуп логичких ваљаности првог реда у сигнатури са једнакошћу и једном унарном функцијом, успоставио Еренфојхт, 1959.
Теорија првог реда целих бројева са сигнатуром са једнакошћу и сабирањем, позната и као Пресбургерова аритметика. Комплетност успоставио Мојжеш Пресбургер, 1929.
Теорија првог реда Булових алгебри, успоставио Алфред Тарски, 1949.
Теорија првог реда алгебарски затворених поља дате карактеристике, успоставио Тарски, 1949.
Теорија првог реда реалних-затворених уређених поља, успоставио Тарски, 1949.
Теорија првог реда Еуклидске геометрије, успоставио Тарски, 1949.
Теорија првог реда хиперболичке геометрије, успоставио Швабхојзер, 1959.

Међу методима за успостављање одлучивости су елиминација квантификатора, комплетност модела, и Вотов тест (Vaught).

Примери неодлучивих теорија

Међу неодлучивим теоријама су (Monk 1976, pp. 279):

Скуп логичких ваљаности у свакој сигнатури првог реда са једнакошћу и: релационим симболом арности не мање од 2, или два унарна функцијска симбола, или један функцијски симбол арности не мање од два, успоставио Трахтенброт, 1953.
теорија првог реда са сабирањем, множењем и једнакошћу, успоставили Тарски и Анджеј Мостовски, 1949.
Теорија првог реда рационалних бројева са сабирањем, множењем и једнакошћу, успоставила Џулија Робинсон, 1949.
Теорија првог реда група, успоставио Мал'цев, 1961. Мал'цев је такође установио да су теорија семигрупа и теорија прстена неодлучиве. Робинсон је 1949. установила да је теорија поља неодлучива.

Метод интерпретабилности се често користи да се докаже неодлучивост неке теорије. Ако је неодлучиву теорију T могуће интерпретирати у конзистентној теорији S, онда је и S неодлучива.

Полуодлучивост

Својство теорије или логичког система, које је слабије од одлучивости је полуодлучивост. Теорија је полуодлучива ако постоји ефективни метод који ће за дату произвољну формулу увек исправно рећи ако је формула у теорији, али ће дати или негативан одговор или неће дати одговора ако формула није у теорији. Логички систем је полуодлучив ако постоји ефективни метод за генерисање теорема (и само теорема), такав да ће у неком моменту свака изабрана теорема бити генерисана. Ово се разликује од одлучивости, јер за полуодлучив систем не мора да постоји ефективна процедура која проверава да ли формула није теорема.

Свака одлучива теорија или логички систем је полуодлучива, али у општем случају обратно не важи; теорија је одлучива ако и само ако су и она и њен комплемент полуодлучиви. На пример, скуп логичких ваљаности V логике првог реда је полуодлучив, али не и одлучив. У овом случају, то је зато што не постоји ефективни метод за произвољну формулу A, који утврђује да A није у V. Слично, скуп логичких последица сваког рекурзивно пребројивог скупа аксиома првог реда је полуодлучив. Многи од примера неодлучивих теорија првог реда, датих горе имају ову форму.

Одлучивост и потпуност

Одлучивост не треба мешати са потпуношћу. На пример, теорија алгебарски затворених поља је одлучива али није потпуна, док је скуп свих истинитих исказа првог реда о ненегативним целим бројевима у језику са + и × потпун, али не и одлучив.

Види још

Литература

Зоран Огњановић, Ненад Крџавац, Увод у теоријско рачунарство, ФОН, Београд, 2004.
Barwise, Jon (1982). „Introduction to first-order logic”. Ур.: 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 изд.). Boston, MA: Academic Press. ISBN 978-0-12-238452-3.
Keisler, H. J. (1982). „Fundamentals of model theory”. Ур.: 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