Rozhodnutelnost

Rozhodnutelnost je matematický pojem z oblasti matematické logiky. Vyjadřuje, zda existuje konečný algoritmus, který pro každou formuli určí, zda je v dané teorii dokazatelná nebo není. Teorie, pro niž takový algoritmus existuje, se nazývá rozhodnutelná, v opačném případě pak nerozhodnutelná. Problematika rozhodnutelnosti úzce souvisí s Gödelovými větami o neúplnosti.

Úvod

Rozhodnutelnost je vlastnost exaktního světa (matematika, formální logika, geometrie, Turingův stroj, exaktní hry např. šachy…) v němž veškeré entity mají exaktní interpretaci. Příklady rozhodnutelnosti: A je/není větší než B; formule W je pravdivá/nepravdivá; y je/není prvkem množiny Y; Turingův stroj zastaví/nezastaví…Rozhodnutelnost nelze instalovat v přirozeném světě vágní, emocionální a subjektivní lidské psýchy, používající přirozený jazyk s vágní (vnitřní vágnost), emocionální a subjektivní interpretací měnící se od člověka k člověku a u každého z nich v čase, které se říká konotace.

Nemůže proto existovat např. logika postavená nad přirozeným jazykem, může existovat pouze formální logika postavená nad umělým formálním jazykem, který má z principu exaktní (s nulovou vnitřní vágností) interpretaci.

Definice

Rozhodnutelná teorie Teorie je rozhodnutelná, pokud množina všech formulí v ní dokazatelných je rekurzivní. Není-li teorie rozhodnutelná, nazývá se nerozhodnutelná.

Silně nerozhodnutelná struktura Struktura se nazývá silně nerozhodnutelná, je-li nerozhodnutelná každá teorie, která ji má za model.

Vlastnosti Rozhodnutelnost či nerozhodnutelnost se přenáší mezi teoriemi, mezi nimiž je určitý vztah. Nejpoužívanější tvrzení, která o tomto hovoří, jsou následující: Rozšíření rozhodnutelné teorie o konečně mnoho axiomů v témže jazyce je rozhodnutelné. Rozšíření rozhodnutelné teorie o definice je rozhodnutelné. Teorie, v níž je interpretovatelná nerozhodnutelná teorie, je také nerozhodnutelná. Konzervativní rozšíření nerozhodnutelné teorie je nerozhodnutelné.

O silně nerozhodnutelných strukturách platí: Je-li v nějaké struktuře definovatelná silně nerozhodnutelná struktura, pak je tato struktura také silně nerozhodnutelná.

Dále se často používá: Rekurzivně axiomatizovatelná nerozhodnutelná teorie je neúplná.

Rozhodnutelnost výroku v logickém systému

Výrok (nazývaný také tvrzení) se v axiomatické teorii považuje za rozhodnutelný, pokud ho lze v rámci této teorie dokázat nebo dokázat jeho negaci. Matematický výrok je proto v teorii nerozhodnutelný, pokud ho nelze odvodit, nebo odvodit jeho negaci, z axiomů té teorie. Abychom odlišili tento pojem nerozhodnutelnosti od pojmu algoritmické nerozhodnutelnosti (viz níže), říkáme také, že výrok je nezávislý na systému axiomů. To platí zejména pro slavný Euklidův postulát rovnoběžek, vztahující se k jeho geometrii, Euklides: Základy, Kniha I , Postulát 5. nebo pro hypotézu kontinua vztahující se ke klasické teorii množin, podle níž neexistuje žádná mohutnost mezi mohutností množiny přirozených celých čísel a mohutností množiny reálných čísel, kterou Paul Cohen Cohen, Paul Joseph (2008) : Set theory and the continuum hypothesis. Mineola, New York City: Dover Publications. p. 151. v roce 1963 prokázal jako nerozhodnutelnou.

V klasické logice je podle věty o úplnosti výrok v teorii nerozhodnutelný, pokud existují modely teorie, kde je výrok nepravdivý, a modely, kde je pravdivý. Modely se často používají k prokázání, že výrok je nezávislý na systému axiomů (v tomto kontextu dáváme přednost použití slova nezávislý před nerozhodnutelným).

Vlastnost použitá v tomto případě není věta o úplnosti, ale její bezprostřední obrácení, nazývané věta o správnosti. Ta říká, že forma deduktivního u je správná tehdy a jen tehdy, je- li platná a všechny její premisy jsou pravdivé. Takto se také poprvé objevil pojem modelu, když Eugenio Beltrami v 19. století zkonstruoval modely neeuklidovských geometrií (které nazýval reprezentacemi). Ty neověřovaly axiom rovnoběžek (připouštějí zcela intuitivní fakt, že euklidovská geometrie je koherentní), ale posloužily k důkazu, že axiom rovnoběžek je nezávislý na ostatních axiomech geometrie, nebo dokonce nerozhodnutelný v systému tvořeném zbývajícími axiomy.

Matematická teorie, pro kterou je každý výrok rozhodnutelný, se nazývá úplná, jinak se nazývá neúplná. Mnoho matematických teorií je neúplných proto, že existují výroky sice vyjádřitelné jazykem teorie, které však nejsou určeny axiomy (teorie grup, teorie okruhů atd.). Některé teorie, jako například teorie algebraicky uzavřených těles dané charakteristiky,On le montre facilement par le théorème de Vaught, par exemple Chang et Keisler 1990, p. 139-140 ou ces notes de cours [archive] d'Elisabeth Bouscaren à Paris-Sud. teorie uzavřených reálných tělesC.C. Chang, H.J. Keisler: Model Theory, Elsevier, Third Edition, 1990, p. 344. nebo Presburgerova aritmetika,Annoncée en Chang et Keisler 1990, p. 43, exercice du chapitre 5. jsou úplné. Gödelova věta o neúplnosti zaručuje, že jakákoli konzistentní axiomatická teorie, dostatečně silná k důkazu Peanovy aritmetiky (obvyklé aritmetiky), je neúplná za předpokladu, že je axiomatizována takovým způsobem, že lze v algoritmickém smyslu (viz níže) rozhodnout, zda je výrok axiomem či nikoli. Tento poslední předpoklad, jehož formulace se zdá být poněkud složitá, je velmi přirozený a ověřen obvyklými axiomatickými teoriemi v matematice.

Rozhodnutelnost algoritmická a nerozhodnutelnost rozhodovacího problému

Definice

Rozhodovací problém se nazývá rozhodnutelný, pokud existuje algoritmus, mechanický postup, který se dokončí v konečném počtu kroků a který problém rozhodne, tj. který na kladenou otázku odpoví ANO nebo NE. Pokud takový algoritmus neexistuje, říká se, že problém je nerozhodnutelný.

Například Turingův problém zastavení je nerozhodnutelný. Pojem funkce vyčíslitelné algoritmem nebo mechanickým postupem lze formalizovat různými způsoby, například lze použít Turingův stroj. Všechny použité metody se ukazují jako ekvivalentní, pokud jsou dostatečně obecné, což vede k formulaci Churchovy teze: Funkce vyčíslitelné mechanickým postupem jsou tytéž, jaké jsou vypočítány podle jednoho z těchto výpočetních modelů. Jinými slovy říká: Ke každému algoritmu existuje ekvivalentní Turingův stroj. Churchova teze je nezbytná pro interpretaci důkazu nerozhodnutelnosti daným způsobem.

Pokud žádný mechanický proces nebo algoritmus nemůže na otázku odpovědět, můžeme hovořit o algoritmické nerozhodnutelnosti, abychom odlišili tento pojem od logické nerozhodnutelnosti (nebo někdy od rozhodnutelnosti algoritmické v Turingově smyslu od rozhodnutelnosti logické v Gödelově smyslu).

Na rozdíl od logické nerozhodnutelnosti, která se týká pravdivosti nebo nepravdivosti jediného výroku (přesněji nemožnosti jeho dokázání nebo dokázání jeho negace v daném axiomatickém systému), se algoritmická nerozhodnutelnost týká nemožnosti řešení problému v obecném případě, což nevylučuje možnost jeho řešení v určitých konkrétních případech.

Rozhodnutelné a nerozhodnutelné množiny

Podmnožina přirozených čísel se nazývá rozhodnutelná, když se dá zjistit, zda jakékoli celé číslo patří do této množiny. Toto se přímo zobecňuje na n-tice celých čísel. Rozhodnutelná množina se také nazývá rekurzivní. Doplněk rozhodnutelné množiny je rozhodnutelný. V teorii vyčíslitelnosti se ukazuje, že rekurzivně spočetná množina, jejíž doplněk je rekurzivně spočetný, je rekurzivní (tj. rozhodnutelná).

Tyto pojmy jsou zobecněny na formální jazyky, použije-li se Gödelovo číslování (tj. každé větě jazyka se přiřadí celé číslo); je také možné je definovat přímo. V případě axiomatické teorie hovoříme o rozhodnutelné teorii nebo nerozhodnutelné teorii. Teorie T se nazývá rozhodnutelná, pokud je množina Gödelových čísel označujících věty teorie T rekurzivní množina, jinak se nazývá nerozhodnutelná.Cori et Lascar, Logique Mathématique, Tome 2, Chapitre 6 "Théorème de Gödel", paragraphe 3.8. Tyto pojmy by neměly být zaměňovány s pojmy úplné a neúplné teorie, protože (ačkoli to má malý praktický význam) lze za axiomy zcela klidně považovat všechny pravdivé výroky (ve smyslu „pravdivé v daném modelu“) a pak je teorie úplná, i když zůstává nerozhodnutelná; a protože naopak velmi nedokonalá teorie, jako je teorie komutativních grup, má mnoho modelů, a je tedy neúplná, zatímco lze snadno určit, které z jejích výroků jsou věty, a proto je rozhodnutelná.

Příklady rozhodnutelných množin a problémů

Všechny konečné podmnožiny celých čísel jsou rozhodnutelné (stačí otestovat rovnost u každého z celých čísel v množině). Můžeme sestrojit algoritmus, který rozhodne, zda je přirozené číslo sudé či nikoli (dělíme dvěma, pokud je zbytek nula, číslo je sudé, pokud je zbytek jedna, sudé není), takže množina sudých přirozených čísel je rozhodnutelná; totéž platí pro množinu prvočísel. Tj. množina může být teoreticky rozhodnutelná, aniž by bylo možné rozhodnutí učinit v praxi, protože by to vyžadovalo příliš mnoho času (více než je stáří vesmíru) nebo příliš mnoho zdrojů (více než je počet atomů ve vesmíru). Účelem teorie složitosti algoritmů je studovat rozhodovací problémy s ohledem na výpočetní zdroje a výpočetní čas.

Platnost výroku v Presburgerově aritmetice je rozhodnutelná. (Presburgerova aritmetika je axiomatický systém přirozených čísel, který zahrnuje sčítání, ale vylučuje násobení.)

Příklady nerozhodnutelných problémů

Nerozhodnutelnost problému zastavení demonstroval Alan Turing v roce 1936. Neexistuje žádný algoritmus, který by dokázal rozhodnout, zda se při daném Turingově stroji a vstupním slově, se jeho výpočet zastaví či nikoli. Vzhledem k Churchově tezi je tento výsledek velmi obecný. Od nástupu informatiky jej lze interpretovat následovně: Neexistuje žádný program, který by dokázal otestovat jakýkoli počítačový program v dostatečně výkonném jazyce, jako jsou všechny používané v praxi, aby ve všech případech dospěl k závěru, zda se výpočet zastaví v konečném čase, nebo zda bude probíhat donekonečna.

Obecněji řečeno, Riceova věta říká, že jakákoli otázka týkající se počítačových programů, která závisí pouze na výsledku výpočtu (zda se ukončí či nikoli, vypočítaná hodnota atd.), je nerozhodnutelná nebo triviální (zde se „triviální“ chápe jako: odpověď je vždy stejná (ANO nebo NE) bez ohledu na program).

Zda je výrok logiky prvního řádu univerzálně platný (prokazatelný v jakékoli teorii), závisí na zvoleném jazykovém podpisu (symboly operací nebo relací atd.). Tento problém, někdy nazývaný rozhodovací problém, je nerozhodnutelný pro jazyk aritmetiky a obecněji pro jakýkoli rovnocenný jazyk logiky prvního řádu, který obsahuje alespoň jeden symbol binární relace (například symbol < nebo ∈). Pro jazyk prvního řádu obsahující pouze unární predikátové symboly je rozhodnutelný.

Zda výrok vyjádřený v jazyce aritmetiky (obsahující obě operace sčítání a násobení) je pravdivý ve standardním modelu aritmetiky, je nerozhodnutelné (to je důsledek Gödelovy první věty o neúplnosti nebo Tarského věty).

Dokazatelnost výroků z axiomů Peanovy aritmetiky je nerozhodnutelná (viz rozhodovací problém). Gödel ukázal, že tato množina je striktně zahrnuta v předchozím. Protože Peanovy axiomy mají nekonečně mnoho axiomů, nevyplývá to přímo z nerozhodnutelnosti rozhodovacího problému v jazyce, jak bylo uvedeno dříve. Oba výsledky vyplývají z obecného výsledku pro aritmetické teorie, které splňují určité podmínky. Peanova aritmetika tyto podmínky splňuje, ale stejně tak i Robinsonova Q-aritmetika, která má konečný počet axiomů.

Dokazatelnost výroků z axiomů koherentní teorie množin a obecněji jakékoli koherentní teorie, která umožňuje vyjádřit „dostatečnou“ formální aritmetiku, je nerozhodnutelná (viz rozhodovací problém).

Otázka, zda má diofantická rovnice řešení. Důkazem její nerozhodnutelnosti je Matijasevičova věta.

Otázka, zda jsou dva členy lambda kalkulu β-ekvivalentní, nebo podobně identita dvou členů kombinatorické logiky. Její nerozhodnutelnost dokázal Alonzo Church.