Rozhodnutelnost

Definice: O teorii $T$ říkáme, že je rozhodnutelná, pokud existuje algoritmus, který pro každou vstupní formuli $\phi$ doběhne a odpoví, zda

$$T\models \phi .$$

a částečně rozhodnutelná, pokud existuje algoritmus, který pro každou vstupní formuli $\phi$:

1. pokud $T\models \phi$, doběhne a odpoví “ano”,
2. pokud $T/\models \phi$, buď nedoběhne, nebo doběhne a odpoví “ne”.

Definice: Teorie $T$ je kompletní, pokud je bezesporná a pro každou uzavřenou formuli $\phi$ platí buď

$$T\models \phi$$

nebo

$$T\models \neg \phi$$

Ekvivalentně to znamená, že neexistuje žádná formule $\phi$, která by byla vůči $T$ nezávislá, tj. pro niž neplatí ani

$$T\models \phi \text{ani}T\models \neg \phi .$$

(Nezávislá formule by byla taková, že její pravdivost vůči $T$ nelze rozhodnout ani v jednom směru.)

Definice: Teorie $T$ je rekurzivně axiomatizovaná, pokud existuje algoritmus, který pro každou vstupní formuli $\phi$ doběhne a odpoví, zda $\phi \in T$.
(tj. množina axiomatických formulí $T$ je rozhodnutelná.)

Tvrzení: Nechť $T$ je rekurzivně axiomatizovaná. Potom:

1. $T$ je částečně rozhodnutelná,
2. je-li $T$ navíc kompletní, potom je rozhodnutelná.

---

1. Diskrétní lineární uspořádání $⟨\mathbb{Z},\le ⟩$
   Axiomatizace obsahuje:

$$\forall x\forall y(x\le y\vee y\le x),\forall x\forall y\forall z(x\le y\wedge y\le z\to x\le z),$$ $$\forall x\exists y(\text{Succ}(x,y))\text{(diskreˊtnost)},$$

kde $\text{Succ}(x,y)$ vyjadřuje, že $y$ je bezprostřední následník $x$. Tato teorie je úplná a umožňuje kvantorové eliminace do kombinací atomických formulí, takže existuje algoritmus na rozhodnutí každé formule v tomto jazyce.

2. Husté lineární uspořádání bez konců $⟨\mathbb{Q},\le ⟩$
   Axiomy zahrnují lineární uspořádání, hustotu:

$$\forall x\forall y(x<y\to \exists z(x<z<y)),$$

a absenci krajů:

$$\forall x\exists y(y<x),\forall x\exists y(x<y).$$

Podle Cantora je to úplná teorie (všechny spočetně nekonečné husté LO bez konců jsou izomorfní) a má kvantorové eliminace, což dává rozhodnutelnost.

4. Presburgerova aritmetika $⟨\mathbb{N},S,+,0⟩$
   Axiomy definují:

$$\forall x\neg (S(x)=0),\forall x\forall y(S(x)=S(y)\to x=y),$$

a vlastnosti sčítání (nuly a následníka). Presburger dokázal, že každá formule v tomto jazyce je ekvivalentní formuli bez kvantifikátorů, což poskytuje efektivní algoritmus na kontrolu její validity, tedy rozhodnutelnost.

5. Teorie reálně uzavřených těles $⟨\mathbb{R},+,-,\cdot ,0,1⟩$
   Tarski ukázal, že teorie reálně uzavřených polí má kvantorovou eliminaci v jazyce uspořádaných těles, a proto je rozhodnutelná — každou formuli lze algoritmicky převést na bezkvantorový tvar a ověřit její pravdivost.

---

1. Platnost formulí prvního řádu
   Churchova–Turingova věta o nerozhodnutelnosti platnosti říká, že neexistuje algoritmus rozhodující, zda je libovolná formule prvního řádu logicky platná ($\models \phi$). Tento problém je nerozhodnutelný.

2. Teorie přirozených čísel $\mathrm{Th}(\mathbb{N})$
   Standardní model aritmetiky

$$⟨\mathbb{N},S,+,\cdot ,0,\le ⟩$$

nemá rekurzivně axiomatizovatelnou teorii, tj. množina všech vět platných v tomto modelu není rozhodnutelná. To plyne z Gödelovy první věty o neúplnosti.

3. Řešitelnost diofantických rovnic (Hilbertův desátý problém)
   Matiyasevičova věta (Davis–Putnam–Robinson–Matiyasevič): neexistuje algoritmus, který by pro danou Diofantickou rovnici

$$p(x_1,\dots ,x_n)=0$$

rozhodl, zda má celočíselné řešení. Problém je tedy nerozhodnutelný.