Algoritmická rozhoditelnost je vlastnost formální teorie mít algoritmus , který pomocí daného vzorce určuje, zda je odvoditelná z množiny axiomů dané teorie či nikoliv. O teorii se říká , že je rozhodnutelná , pokud takový algoritmus existuje, a jinak nerozhodnutelná . Otázka odvoditelnosti ve formální teorii je zvláštním, ale zároveň nejdůležitějším případem obecnějšího problému rozhodnutelnosti .
Koncepty algoritmu a axiomatického systému mají dlouhou historii. Oba jsou známy již od starověku . Stačí si připomenout postuláty Euklidovy geometrie a algoritmus pro nalezení největšího společného dělitele téhož Euklida. Přesto dlouho neexistovala jasná matematická definice kalkulu a zejména algoritmu. Zvláštností problému spojeného s formální definicí nerozhodnutelnosti bylo, že k prokázání existence nějakého algoritmu stačí jej pouze najít a předvést. Pokud se algoritmus nenajde, je možné, že neexistuje, a to je třeba důsledně dokázat. A k tomu musíte přesně vědět, co je to algoritmus.
Velkého pokroku ve formalizaci těchto pojmů dosáhl na počátku 20. století Hilbert a jeho škola. Nejprve byly vytvořeny pojmy kalkulu a formální derivace a poté si Hilbert ve svém slavném programu zdůvodňování matematiky stanovil ambiciózní cíl formalizovat celou matematiku. Program poskytoval mimo jiné možnost automatické kontroly pravdivosti libovolného matematického vzorce. Na základě práce Hilberta Gödel poprvé popsal třídu takzvaných rekurzivních funkcí , pomocí kterých dokázal své slavné teorémy neúplnosti . Následně byla představena řada dalších formalismů, jako je Turingův stroj , λ-počet , který se ukázal být ekvivalentní rekurzivním funkcím. Každý z nich je nyní považován za formální ekvivalent intuitivního pojmu vyčíslitelné funkce. Tato ekvivalence je postulována Churchovou tezí .
Když byly koncepty kalkulu a algoritmu upřesněny, následovala řada výsledků o nerozhodnutelnosti různých teorií. Jedním z prvních takových výsledků byla věta dokázaná Novikovem o neřešitelnosti problému slov ve skupinách . Rozhodnutelné teorie byly známy dlouho předtím.
Intuitivně platí, že čím je teorie složitější a výraznější, tím větší je šance, že se ukáže jako nerozhodnutelná. Zhruba řečeno, „nerozhodnutelná teorie“ je tedy „komplexní teorie“.
Formální počet v obecném případě musí definovat jazyk , pravidla pro konstrukci termínů a vzorců , axiomy a pravidla vyvozování. Pro každý teorém T je tedy vždy možné sestrojit řetězec A 1 , A 2 , … , A n = T , kde každá formule A i je buď axiom, nebo ji lze odvodit z předchozích vzorců podle některého z odvození pravidla. Řešitelnost znamená, že existuje algoritmus, který pro každou dobře utvořenou větu T v konečném čase dává jednoznačnou odpověď: ano, tato věta je odvoditelná v rámci kalkulu nebo ne, není odvoditelná.
Je zřejmé, že protichůdná teorie je rozhodnoutelná, protože jakýkoli vzorec bude odvoditelný. Na druhé straně, jestliže počet nemá rekurzivně vyčíslitelnou množinu axiomů, jako je logika druhého řádu , samozřejmě nemůže být rozhodnutelný.
Rozhodnutelnost je velmi silná vlastnost a většina užitečných a praktických teorií ji nemá. V souvislosti s tím byl zaveden slabší pojem semirozhodnosti . Polorozhodnutelný znamená mít algoritmus, který vždy v konečném čase potvrdí, že věta je pravdivá, pokud je pravdivá, ale pokud není, může běžet donekonečna.
Požadavek semirozhoditelnosti je ekvivalentní schopnosti efektivně vyjmenovat všechny teorémy dané teorie. Jinými slovy, množina vět musí být rekurzivně spočetná . Většina teorií používaných v praxi tento požadavek splňuje.
Účinné semi-permisivní postupy pro logiku prvního řádu mají velký praktický význam, protože umožňují (polo)automaticky dokazovat formalizovaná tvrzení velmi široké třídy. Průlomem v této oblasti byl Robinsonův objev metody rozlišení v roce 1965 .
V matematické logice se tradičně používají dva pojmy úplnosti: vlastní úplnost a úplnost s ohledem na nějakou třídu výkladů (nebo struktur). V prvním případě je teorie úplná, pokud je každá věta v ní buď pravdivá, nebo nepravdivá. V druhém případě, pokud je odvoditelná jakákoli věta, která je pravdivá ve všech interpretacích z dané třídy.
Oba pojmy úzce souvisí s rozhodností. Pokud je například množina axiomů úplné teorie prvního řádu rekurzivně spočetná, pak je rozhodnoutelná. Vyplývá to ze slavné Postovy věty , která říká, že pokud jsou množina i její doplněk rekurzivně spočetné, pak jsou také rozhodnutelné . Intuitivně je argument ukazující pravdivost výše uvedeného tvrzení následující: pokud je teorie úplná a soubor jejích axiomů je rekurzivně vyčíslitelný, pak existují semipermisivní postupy pro testování pravdivosti jakéhokoli tvrzení a také jeho negace. Pokud spustíte oba tyto postupy paralelně , pak by se vzhledem k úplnosti teorie měl jeden z nich jednoho dne zastavit a dát kladnou odpověď.
Pokud je teorie kompletní s ohledem na nějakou třídu interpretací, lze to použít ke konstrukci rozhodovací procedury. Například výroková logika je kompletní s ohledem na výklad na pravdivostních tabulkách . Proto konstrukce pravdivostní tabulky podle tohoto vzorce bude příkladem algoritmu řešení pro výrokovou logiku.