Gödel-számozás: definíció, működés és szerepe a befejezetlenségi tételben

Mi a lényeges ötlet?

A Gödel-számozás lényege, hogy a formális nyelv szimbólumait és szintaktikai objektumait (formulákat, bizonyításokat stb.) természetes számokkal kódoljuk úgy, hogy a nyelv szintaktikai relációi (például „x egy jól képzett formula” vagy „x bizonyítja y-t”) számelméleti relációkká váljanak. Így a nyelv és a bizonyítások tulajdonságairól beszélő állítások maguk is természetes számokról és számelméleti relációkról fognak szólni, amely lehetővé teszi, hogy a formális rendszer belső nyelvén reflektáljunk saját metanyelvi állításaira.

Konstrukció (egyszerű, gyakran használt módszer)

Gyakori és szemléletes módszer a következő:

• rendezzük a formális nyelv szimbólumait és minden egyes szimbólumhoz rendeljünk egy természetes számot (például 1, 2, 3, ...);
• egy szimbólumsorozatot (például egy formulát) úgy kódolunk, hogy az i-edik szimbólumhoz tartozó számot a i-edik prímszám kitevőjévé tesszük; azaz ha a formula szimbólumai s1, s2, ..., sn és code(si)=ai, akkor a Gödel-számot definiálhatjuk GN(s1...sn)=2^{a1}·3^{a2}·5^{a3}·...·p_n^{a_n}, ahol p_i az i-edik prímszám.

A kódrendszer injektivitását a természetes számokban érvényes alapfelbontás (a prímtényezős felbontás egyértelműsége) biztosítja: két különböző szimbólumsorozat különböző természetes számokra kerül. Gödeli és későbbi konstruktiókban a hozzárendelés olyan módon választott, hogy a kapott függvény primitív rekurzív, tehát különösen kiszámítható legyen.

Tulajdonságok és technikai részletek

• Kiszámíthatóság: a tipikus Gödel-számozás olyan, hogy a szintaktikai relációk (pl. „x egy formula”, „x egy bizonyítás”, „x beírja y-t a z helyére”) primitív rekurzívek, vagy legalább rekurzívek. Ez lehetővé teszi, hogy ezek a relációk a formális számelméletben reprezentálhatók legyenek.
• Reprezentálhatóság: ha egy reláció primitív rekurzív (vagy rekurzív), akkor a megfelelő aritmetikai rendszerben (például a Peano-aritmetikában) létezik formula, amely azt a relációt „leírja” — vagyis a reláció igazságát a rendszer képes kifejezni.
• Rogers-ekvivalencia: Rogers tétel szerint az ún. elfogadható (acceptable) számozások egymással kiszámítható izomorfizmust adnak: azaz minden két „jó” Gödel-számozás között létezik olyan effektív átfordítás, amelyik egyik számozást a másikká alakítja. Ez azt fejezi ki, hogy a Gödel-számozás részletei lényegtelenek — a fontos az, hogy a számozás hatékony legyen.

Szerepe a befejezetlenségi tételben

A Gödel-számozás kulcsfontosságú a befejezetlenségi tétel bizonyításában, mert lehetővé teszi, hogy a formális rendszer „beszéljen” saját állításairól és bizonyításairól. A fő lépések röviden:

• kódoljuk a formulákat és bizonyításokat természetes számokká (Gödel-számok);
• definiáljuk a provability (bizonyíthatóság) predikátumot Bew(x) vagy Prov(x), amely igaz akkor és csak akkor, ha x egy olyan szám, amely egy bizonyítást reprezentál egy adott formula számára; ez a predikátum aritmetikai formulával reprezentálható a rendszerben;
• diagonalizációval (vagy a fixpont-tétellel) létrehozunk egy olyan formulát G-t, amely intuitíve azt állítja, hogy „G-nek nincs bizonyítása” (formálisan: G ≡ ¬Bew(gn(G)));
• ha a rendszer konzisztens, akkor G nem lehet sem bizonyítható, sem cáfolható a rendszerben — így létezik a rendszerben egy igaz (külső nézőpontból) de belsőleg nem bizonyítható állítás, ami a befejezetlenséget biztosítja.

Ez a gondolatmenet a Gödel-számozás nélkül nem lenne megvalósítható, mert nem tudnánk a metanyelvi fogalmakat a rendszer belső nyelvére fordítani.

Variánsok és modern szemlélet

A konkrét számozás részletei tetszőlegesek lehetnek, amíg a számozás „elfogadható” (hatékony) — ezért a modern irodalom gyakran nem ragaszkodik a prímtényezős módszerhez, hanem bármely olyan konstruktív kódolást használ, amely kielégíti a kiszámíthatósági követelményeket. Fontos tény, hogy minden ésszerű (elfogadható) Gödel-számozás ugyanazokra az elvi következtetésekre vezet: a befejezetlenségi tétel és más metamatematikai eredmények függetlenek a választott konkrét számozástól.

Rövid példa

Egy leegyszerűsített példa: rendelhetjük a szimbólumoknak a következő kódokat — '('→1, ')'→2, '0'→3, 'S'→4, '+'→5, '='→6, változókat külön számmal stb. Egy formula s1 s2 s3 sorozat Gödel-száma lehet GN=2^{code(s1)}·3^{code(s2)}·5^{code(s3)}·... . A Fordítottság és egyértelműség a prímtényezős felbontás alapján adódik: ha ismerjük GN-t, vissza tudjuk állítani a kódolt szimbólumok sorozatát.

Összefoglalás

A Gödel-számozás a formális nyelvek és bizonyítások aritmetizálásának eszköze: egy hatékony, injektív kódolás, amely lehetővé teszi szintaktikai fogalmak aritmetikai reprezentálását. Ez tette lehetővé Gödel számára a fundamentális befejezetlenségi eredmények megfogalmazását és bizonyítását. Bár maga a számozás technikailag tetszőleges lehet, a követelmény, hogy kiszámítható legyen, biztosítja, hogy az elméleti következmények általánosak és rendszerszintűek legyenek.