Matematické Fórum

Ahoj,
následující text se týká oblasti formální logiky, formálních důkazů a trochu Godelových vět o neúplnosti. (Zatím sem psát definice jednotlivých pojmů nebudu, předpokládám, že je čtenář zná, ale případně je upřesním.)

Jak známo z Godelových vět o neúplnosti, v dostečně "silném" systému existují tvrzení T, pro která platí, že ani T ani nonT (tj. negace T) nejsou dokazatelné. Označme Dok(X) "meta"tvrzení, že formule X je donazatelná. Označme S1(T):="Dok(T) nebo Dok(nonT)". Tedy S1 není tvrzení, ale "meta"tvrzení - ale dle mého se tvrzením může stát - pokud jej formalizujeme v dané teorii - podobně jako Godel ro provedl Godel při svém důkazu (viz Godelova čísla). (Tady se nabízí prostor na spekulace, zda to lze takto vždy provést..) Godelova věta o neúplnosti říká, že existuje formule T taková, že neplatí S1(T).

Nechť stojíme před úkolem: pro danou formuli T ukázat, že platí S1(T) a nebo že platí nonS1(T). S1 vlastně znamená, že chceme T dokázat nebo "vyvrátit" a nonS1 znamená, že to není možné, tj. že T je "nezávislá" na axiomech dané teorie. Otázka zní - je vždy možné dokázat S1(T) a nebo dokázat nonS1(T)? Formálně označíme-li S2(T):="lze dokázat S1(T) nebo lze dokázat nonS1(T)", platí potom vždy S2(T) pro každou T? Např. je-li T tzv. hypotéza kontinua, pak neplatí S1(T), ale platí S1(T).

Pokud ne, lze postupovat induktivně dále - a položit S3(T):="lze dokázat S2(T) nebo lze dokázat nonS2(T)". Otázka zní - lze pro nějaké i dokázat Si(T)? Je to vlastně zobecnění (iterace) neúplnosti...

S výše uvedeným ještě souvisí - pokud chceme dokázat, že v teorii S není dokazatelná formule T, tak stačí ukázat, že S, ke které přidáme nonT jako axiom, má model. Lze však - pokud tento model existuje - vždy dokázat, že je tomu tak, tj. že ten model opravdu existuje? Protože "existence" a "důkaz existence" jsou dvě různé věci... Tedy obecně - má-li daná teorie model, lze toto i dokázat? Ale tento odstavec již není hlavním tématem tohoto vlákna, nicméne s ním souvisí, a tak jsem ho uvedl.

Díky za názory k tomuto tématu.