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,^[1] 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^[2] 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,^[3] teorie uzavřených reálných těles^[4] nebo Presburgerova aritmetika,^[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á.^[6]
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á.^[7] (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.

• Postův korespondenční problém je neřešitelný.

Rozhodnutelné teorie

Axiomatická teorie je rozhodnutelná, když jsou všechny její věty rozhodnutelné, tj. když existuje algoritmus, který vždy odpovídá ANO nebo NE na otázku, zda je daný výrok v dané teorii dokazatelný. Takový algoritmus lze snadno rozšířit na formální algoritmus pro hledání důkazů (za podmínky ověřené „obvyklými“ teoriemi, že být axiomem je rozhodnutelné): jakmile víme, že výrok je dokazatelný, stačí vyjmenovat všechny dobře formulované důkazy, dokud nenajdeme důkaz daného výroku. Tento vyhledávací algoritmus je samozřejmě zajímavý pouze teoreticky, s výjimkou obzvláště jednoduchých případů, kdy je aplikovatelný. I když je teorie rozhodnutelná, algoritmická složitost získání rozhodnutí může zapříčinit jeho nedosažitelnost.

Příklady rozhodnutelných teorií:

• Teorie uzavřených reálných těles je rozhodnutelná, s algoritmy založenými na eliminaci kvantifikátorů, které na základě daného výroku vytvoří ekvivalentní výrok bez kvantifikátorů ∀ nebo ∃; výroky teorie bez kvantifikátorů jsou triviálně rozhodnutelné; složitost známých algoritmů je vysoká a umožňuje rozhodování výroků pouze ve velmi jednoduchých případech.
• Presburgerova aritmetika (celočíselná aritmetika se sčítáním, ale bez násobení, nebo, což je totéž, s násobením omezeným na případ, kdy jeden z operandů je konstanta) je rozhodnutelná.^[7]

Logická a algoritmická rozhodnutelnost

Oba pojmy rozhodnutelnosti interpretují intuitivní pojem rozhodnutí každý v jasně odlišných významech. Jsou však propojeny. V matematice se má za to, že důkaz, i pokud je obtížné ho najít, musí být „snadno“ ověřitelný, a to ve velmi neformálním (a diskutabilním – ale to není předmětem tohoto článku) smyslu. Když formalizujeme, interpretujeme tak s požadavkem, aby problém rozpoznání, zda skupina vět je formálním důkazem, byl rozhodnutelný. Aby to bylo správné, musíme předpokládat, že skupina axiomů teorie je rozhodnutelná, což, jak již bylo zmíněno, je velmi přirozené. Za tohoto předpokladu se skupina vět teorie stává rekurzivně spočetnou. Taková teorie, pokud je úplná, je pak rozhodnutelná (viz článek axiomatická teorie pro další zdůvodnění a podrobnosti).

Na druhou stranu, rozhodnutelná teorie nemusí být nutně úplná. Teorie algebraicky uzavřených těles tedy není úplná, protože charakteristika není specifikována: tak výrok prvního řádu 1 + 1 = 0 není důsledkem teorie, protože existují algebraicky uzavřená tělesa charakteristiky jiné než 2, a výrok prvního řádu 1 + 1 ≠ 0 také není důsledkem teorie, protože existují algebraicky uzavřená tělesa charakteristiky 2. Toto je logika prvního řádu. Pro každé prvočíslo p platí, že těleso má charakteristiku p, prvního řádu danou jediným axiomem tvaru 1 + … + 1 = 0. Pro charakteristiku 0 je vyžadováno nekonečno axiomů (všechny negace předchozích).

Teorie algebraicky uzavřených těles je však rozhodnutelná.^[8] Teorie algebraicky uzavřených těles dané charakteristiky je úplná^[9] a rozhodnutelná.

Pravda a rozhodnutelnost

Abychom mohli tyto dva pojmy užitečně porovnat, musíme mít striktní definici pojmu pravdivosti; tu formuloval Alfred Tarski. V logice (prvního řádu) říkáme, že výrok je pravdivý v daném modelu teorie, pokud je to splněno (v technickém, ale poměrně intuitivním smyslu) objekty tohoto modelu; prokázaný výrok je zjevně pravdivý v jakémkoli modelu, a pro konzistentní teorii platí opak: tím je Gödelova věta o úplnosti. Situace je mnohem složitější u nerozhodnutých výroků: existují (pokud vezmeme v úvahu opak předchozího výsledku) modely, ve kterých jsou pravdivé, a modely, ve kterých jsou nepravdivé (prokázání takových modelů je navíc jedním z klasických způsobů dokazování nerozhodnutelnosti) a většinou neexistuje argument, který by umožňoval upřednostnit jeden případ před druhým; to je například v geometrii případ axiomu rovnoběžek. Aritmetické výroky však mají zvláštní status: výrok ve tvaru „pro všech n celých čísel je P(n) pravdivý“ (například „ n > 5 je součet tří prvočísel“), pokud je nerozhodnutelný, je nutně pravdivý (v množině „přirozených“ celých čísel, často nazývaných standardní celá čísla), protože jinak by protipříklad poskytl účinnou demonstraci jeho negace. Na základě tohoto pozorování vyvinul Stephen Cole Kleene celou delikátní logickou teorii aritmetické hierarchie.

Rozhodnutelnost v exaktních hrách

Některé exaktní hry byly klasifikovány podle jejich rozhodnutelnosti:

• Mat v n v nekonečném šachu (s neomezenou šachovnicí, omezeními pravidel a herních figurek) je rozhodnutelný.^[10][11]
• Existují však pozice (s konečným počtem figurek), které jsou vynucenými výhrami, ale ne mat v n pro žádné konečné n.^[12]
• Některé týmové hry s neúplnými informacemi na konečné desce (ale s neomezeným časem) jsou nerozhodnutelné.^[13]

Příklady

Důsledky nerozhodnutelnosti Robinsonovy aritmetiky

Robinsonova aritmetika je nerozhodnutelná teorie. Dokonce každé bezesporné rozšíření Robinsonovy aritmetiky je nerozhodnutelné. Tato dvě tvrzení mají mnoho důsledků:

• Protože je Robinsonova aritmetika konečně axiomatizovatelná, je nerozhodnutelná také prázdná teorie v jazyce aritmetiky.
• Peanova aritmetika je nerozhodnutelná a protože je rekurzivně axiomatizovatelná, je neúplná.
• Standardní model aritmetiky (struktura přirozených čísel) je silně nerozhodnutelná struktura.
• Teorie standardního modelu (jejími axiomy jsou všechny formule platné ve standardním modelu) je nerozhodnutelná, protože je však úplná, nemůže být rekurzivně axiomatizovatelná.
• Protože jsou přirozená čísla definovatelná v celých (např. pomocí Lagrangeovy věty o čtyřech čtvercích) a celá v racionálních, jsou struktury celých a racionálních čísel také silně nerozhodnutelné struktury. Odtud dále plyne:
  • Teorie okruhů, komutativních okruhů, oborů integrity, těles, komutativních těles či těles charakteristiky 0, jsou nerozhodnutelné.

Rozhodnutelné teorie

Následující teorie jsou rozhodnutelné:

• teorie hustých lineárních uspořádání
• teorie abelovských grup
• teorie booleových algeber
• teorie algebraicky uzavřených těles
• Presburgerova aritmetika