Az algoritmikus eldönthetőség egy formális elmélet azon tulajdonsága , hogy van egy algoritmusa , amely egy adott formulával meghatározza, hogy az adott elmélet axiómáiból származtatható-e vagy sem. Egy elméletről azt mondják , hogy eldönthető , ha létezik ilyen algoritmus, és eldönthetetlen egyébként. A levezethetőség kérdése a formális elméletben egy sajátos, de egyben a legfontosabb esete a eldönthetőség egy általánosabb problémájának .
Az algoritmus és az axiomatikus rendszer fogalma hosszú múltra tekint vissza. Mindkettő az ókor óta ismert . Elég, ha felidézzük Eukleidész geometriájának posztulátumait és ugyanazon Eukleidész legnagyobb közös osztójának megtalálására szolgáló algoritmust . Ennek ellenére a kalkulusnak és különösen az algoritmusnak világos matematikai definíciója nagyon sokáig nem létezett. A eldönthetetlenség formális definíciójával kapcsolatos probléma sajátossága az volt, hogy ahhoz, hogy megmutassuk, hogy létezik valamilyen algoritmus, elég azt megtalálni és bemutatni. Ha az algoritmus nem található, akkor lehetséges, hogy nem létezik, és akkor ezt szigorúan be kell bizonyítani. Ehhez pedig pontosan tudnia kell, hogy mi az algoritmus.
A 20. század elején Hilbert és iskolája nagy előrelépést ért el e fogalmak formalizálásában . Ezután először a számítás és a formális levezetés fogalmát alkották meg, majd Hilbert a matematika alátámasztásának híres programjában az egész matematika formalizálását tűzte ki ambiciózus célul. A program többek között lehetőséget biztosított arra, hogy bármilyen matematikai képletet automatikusan ellenőrizzünk az igazság szempontjából. Hilbert munkája alapján Gödel először leírta az úgynevezett rekurzív függvények osztályát , amellyel bebizonyította híres befejezetlenségi tételeit . Ezt követően számos más formalizmust vezettek be, mint például a Turing-gépet , a λ-számítást , amelyekről kiderült, hogy egyenértékűek a rekurzív függvényekkel. Ezek mindegyikét ma már a kiszámítható függvény intuitív fogalmának formális megfelelőjének tekintjük. Ezt az egyenértékűséget Church tézise feltételezi .
A számítás és az algoritmus fogalmának finomítása után számos eredmény következett a különféle elméletek eldönthetetlenségére vonatkozóan. Az egyik első ilyen eredmény a Novikov által bizonyított tétel a szavak csoportos problémáinak megoldhatatlanságáról . Dönthető elméletek már jóval korábban ismertek voltak.
Intuitív módon minél összetettebb és kifejezőbb az elmélet, annál nagyobb az esélye annak, hogy eldönthetetlennek bizonyul. Ezért durván szólva a „megdönthetetlen elmélet” „összetett elmélet”.
A formális számításnak általános esetben meg kell határoznia a nyelvet , a kifejezések és képletek készítésének szabályait , az axiómákat és a következtetés szabályait. Így minden T tételhez mindig létre lehet hozni egy A 1 , A 2 , … , A n = T láncot , ahol minden A i képlet vagy axióma, vagy levezethető az előző formulákból valamelyik levezetés szerint. szabályokat. A feloldhatóság azt jelenti, hogy van egy algoritmus, amely minden egyes jól formált T mondatra véges idő alatt egyértelmű választ ad: igen, ez a mondat származtatható a kalkulus keretein belül vagy sem, nem származtatható.
Nyilvánvaló, hogy az ellentmondásos elmélet eldönthető, hiszen bármely képlet származtatható lesz. Másrészt, ha egy kalkulusnak nincs rekurzívan megszámlálható axiómakészlete, mint például a másodrendű logika , akkor nyilvánvalóan nem lehet eldönteni.
A döntésképesség nagyon erős tulajdonság, és a legtöbb hasznos és gyakorlati elmélet nem rendelkezik vele. Ezzel kapcsolatban bevezették a félig elhatárolhatóság gyengébb fogalmát . A félig eldönthető azt jelenti, hogy van egy olyan algoritmus, amely véges időn belül mindig megerősíti, hogy a mondat igaz, ha igaz, de ha nem, akkor a végtelenségig futhat.
A félig eldönthetőség követelménye egyenértékű azzal, hogy egy adott elmélet összes tételét hatékonyan fel tudjuk sorolni. Más szavakkal, a tételek halmazának rekurzívan felsorolhatónak kell lennie . A gyakorlatban alkalmazott elméletek többsége eleget tesz ennek a követelménynek.
Az elsőrendű logika hatékony, félig megengedő eljárásai nagy gyakorlati jelentőséggel bírnak, mivel lehetővé teszik egy nagyon széles osztály formalizált állításainak (fél)automatikus bizonyítását. Ezen a területen áttörést jelentett Robinson 1965 -ben a felbontási módszer felfedezése .
A matematikai logikában hagyományosan a teljesség két fogalmát használják: a tulajdonképpeni teljességet és az értelmezések (vagy struktúrák) bizonyos osztályaira vonatkozó teljességet. Az első esetben egy elmélet akkor teljes, ha minden mondata igaz vagy hamis. A második esetben, ha az adott osztályból bármely értelmezés szerint igaz mondat származtatható.
Mindkét fogalom szorosan összefügg a döntésképességgel. Például, ha egy teljes elsőrendű elmélet axiómáinak halmaza rekurzívan megszámlálható, akkor eldönthető. Ez Post híres tételéből következik , amely kimondja, hogy ha egy halmaz és komplementere is rekurzívan megszámlálható, akkor ezek is eldönthetők . Intuitív módon a fenti állítás igazságát mutató érv a következő: ha az elmélet teljes, és axiómáinak halmaza rekurzívan megszámlálható, akkor léteznek félig megengedő eljárások bármely állítás igazságának, valamint tagadásának tesztelésére. Ha mindkét eljárást párhuzamosan futtatja , akkor az elmélet teljessége miatt az egyiknek egyszer le kell állnia, és pozitív választ kell adnia.
Ha az elmélet bizonyos értelmezési osztályok tekintetében teljes, akkor ez felhasználható egy döntési eljárás megalkotására. Például a propozíciós logika teljes az igazságtáblázatok értelmezése tekintetében . Ezért az igazságtábla e képlet szerinti felépítése egy példa lesz a propozíciós logika feloldó algoritmusára.