Mějme nějaký zcela libovolný problém
P vyřešený počítačovým programem
p se vstupem
a. (Cokoli od hledání smyslu, života a vůbec po rozsvícení žárovky, anebo to může být úkol zaseknout se a nedělat nic.) Mějme počítačový program
q se vstupem
b, který řeší jiný problém. (Nechceme-li vstupy, mohu být příslušná vstupní data tzv.
None. Programátoři vědí. Vstupem programu pochopitelně může být i kód programu.) Zápisem
x značím kód programu a zápisem
x(
c) značím volání programu
x se vstupem
c. Ptejme se nyní: existuje program
r, který má-li na vstupu kód
x a datum
c rozhodne, zda
x(
c) řeší problém
P. Předpokládejme, že program
r existuje. Pak lze napsat program (třeba v pythonu):
def s(d):
if r(d, d):
q(b)
else:
p(a)
Ptejme se nyní, co udělá
s(
s)? Pokud
s(
s) řeší
P, pak jej neřeší, protože se spustí
q(
b). Pokud jej však neřeší, pak jej řeší, protože se spustí
p(
a). V obou případech tedy dostáváme spor, což je další spor, a tedy program
r nemůže existovat.
Pokud je formální systém tak složitý, že může zpracovávat kód jako datum (tzn. ani moc jednoduchý, ani moc složitý), pak není žádný problém rozhodnutelný. Na Halting Problému se to sice dobře ukazuje, ale nemyslím, že by obecný výše uvedený důkaz nějak komplikovaný. Tento důkaz není ani tak podobný Gödelovu/Rosserovu důkazu, protože tam je sebereference, která vede ke sporu s úplností, nikoli s její existencí. V tomto důkazu vede sebereference ke sporu s vlastní existencí. Z epistemického hlediska je tento důkaz podobný spíše diagonálnímu důkazu Cantorovu.
Přímým důsledkem této věty je fakt, že každý řešitelný problém lze řešit nekonečně mnoha navzájem velmi nepodobnými způsoby, jinými slovy, prostor pro kreativitu není omezen.
Matematici tuto větu znají v podobě, která používá Gödelovo výrazivo:
Množina kódů programu řešící nějaký problém je buď prázdná, nebo nerekursivní.
Toto a mnohé jiné se můžete dočíst v připravované knize Michala Černého Výpočty:
http://nb.vse.cz/~cernym/vypocty.pdf.