Bystroushaak's blog / Czech section / Knihy / Gödel's Proof

Gödel's Proof

Gödelovy věty o neúplnosti patří k věcem, které podobně jako Turingův stroj, nebo Lambda calculus prostupují celým světem počítačů a narazíte na ně dřív nebo později všude. Písmeno ‚G‘ v GEBu je věnované právě Gödelovi, proto jsem byl už delší dobu zvědavý, na to co vlastně objevil, a o tom právě pojednává kniha Gödel's Proof.

Gödel v podstatě ukázal, jak je možné i v omezeném setu axiomů a zdánlivě bezkonfliktním systému vytvořit paradoxy referencováním sebe sama. Kniha se věnuje tomu, jak k tomu došel. Nejde do úplných detailů (ty jsou v samotném důkazu), spíš se snaží čtenáři vysvětlit jednotlivé kroky, postupně v jednotlivých kapitolách za sebou.

Kroky důkazu (a tedy i obsah knihy) postupují ve zkratce asi nějak takto:

Zkoncentrovaný obsah

Gödel vyšel z axiomatického systému definovaného v knize Principia mathematica od Whiteheada a Russela, která se snažila nadefinovat a odvodit celou matematiku pomocí logických axiomů.

V tomto systému vymyslel způsob, jak překládat jednotlivé přípustné symboly axiomů na jejich jednoznačné číselné vyjádření (pomocí násobení prvočísel s exponentem kódujícím daný axiom). Tím je možné převést daný výraz v axiomatickém systému, například „0=0“ na axiomy 2, 6, 2 („2“ kóduje číslo 0, 6 kóduje symbol „=“), které pak převedeme na číslo zmíněným násobením:

Což se rovná číslu 72900. Z tohoto čísla je pak možné metodou faktorizace prvočísel zpětně jednoznačně dostat původní písemný výraz.

Gödel poté dokázal, že takhle je možné vyjádřit nejenom teorémy, ale i jejich důkazy. Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování. Toho dosáhl tím, že se vyjadřoval o „bezvýznamných symbolech“ a umožnil čistě „mechanické“ kontrolování a odvozování podle pravidel axiomatického systému.

Poté sestrojil výraz, který dokazuje pravdivost čísla enkódujícího teorém G, který má stejné vyjádření, jako svůj vlastní důkaz. Konkrétně:

„Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo.“

Pokud však tomuto teorému enkódujícímu konkrétní důkaz předhodíme na vstup sám sebe, tak sám sebe vyvrátí. Jenže když se vyvrátí, tak se nemůže dokázat. Celé to bylo samozřejmě podstatně složitější, ale nemá smysl tady zacházet do detailů, tomu se věnuje zmiňovaná knížka.

Jakmile měl Gödel první paradox, tak poté mohl zkonstruovat nekonečné množství podobných paradoxů, které vedly na výsledky, jako:

„Tento teorém, i jeho negace není platným teorémem.“

Gödel tím dokázal, že axiomatické systémy nemůžou být použity k „vytěžení“ celé matematiky iterací přes platné axiomatické výrazy, protože axiomatické systémy obsahují jednak paradoxy, které jsou nerozhodnutelné, ale také jakési ostrovy platných vět, ke kterým se není možné dostat odvozováním z axiomatických systémů.

V knize je to samozřejmě popsané celé podstatně detailněji, a čitelněji. Určitě jí můžu jen doporučit. Četla se mi docela dobře i jako laikovi a je poměrně tenká.

Gödelův důkaz má poměrně velké důsledky také pro sféru computer science, neboť ukazuje, že statická analýza je ze své podstaty nekompletní. To má své důsledky například při dynamické transformaci programů v lispovském stylu, ale také třeba pro analýzu virů, nebo dokázování korektnosti programu.

Ukázka

Nedá mi to, abych nevložil citaci několika stran, které se sice přímo netýkají důkazu, ale stejně na mě hodně zapůsobily krásnou analogií:

It may be useful, by way of illustration, to compare meta-mathematics as a theory of proof with the theory of chess. Chess is played with 32 pieces of specified design on a square board containing 64 square subdivisions, where the pieces may be moved in accordance with fixed rules. The game can obviously be played without assigning any "interpretation" to the pieces or to their various positions on the board, although such an interpretation could be supplied if desired. For example, we could stipulate that a given pawn is to represent a certain regiment in an army, that a given square is to stand for a certain geographical region, and so on. But such stipulations (or interpretations) are not customary; and neither the pieces, or the squares, nor the positions of the pieces on the board signify anything outside the game. In this sense, the pieces and their configurations on the board are "meaningless", Thus the game is analogous to a formalized mathematical calculus.
The pieces and the squares of the board correspond to the elementary signs of the calculus; the legal positions of pieces on the board, to the formulas of the calculus; the initial positions of pieces on the board, to the axioms or initial formulas of the calculus; the subsequent positions of pieces on the board, to formulas derived from axioms (i.e. to the theorems); and the rules of the game, to the rules of inference (or a derivation) for the calculus.
The parallelism continues. Although configurations of pieces on the board, like the formulas of the calculus, are "meaningless," statements about these configurations, like meta-mathematical statements about formulas, are quite meaningful. A "meta-chess" statement may assert that there are twenty possible opening move for White, or that, given a certain configurations of pieces on the board with White to move, Black is mate in three moves. Moreover, general "meta-chess" theorems can be established whose proof involves only finite number of permissible configurations on the board. The "meta-chess" theorem about the number of possible opening moves for White can be established in this way; and so can the "meta-chess" theorem that if White has only two Knights and the King, and Black has only a King, it is impossible for White to force a mate against Black.
These and other "meta-chess" theorems can, in other words, be proved by finitistic methods of reasoning, that is, by examining in turn each of a finite number of configurations that can occur under stated conditions. The aim of Hilbert's theory of proof, similarly, was to demonstrate by such finitistic methods the impossibility of deriving certain formally contradictory formulas in a given mathematical calculus.

— NAGEL, Ernest a James NEWMAN. Gödel's proof. Rev. ed. New York: New York University Press, 2008, s. 34-37. ISBN 9780814758373.

Become a Patron