In de formele getaltheorie is een Gödelnummering een functie die aan elk symbool en elke formule van een formele taal een uniek natuurlijk getal toekent, dat een Gödelgetal (GN) wordt genoemd. Het concept werd voor het eerst gebruikt door Kurt Gödel voor het bewijs van zijn onvolledigheidstheorema.

Een Gödel-nummering kan worden opgevat als een codering waarbij aan elk symbool van een wiskundige notatie een getal wordt toegekend, en een stroom van natuurlijke getallen kan dan een of andere vorm of functie voorstellen. Een nummering van de verzameling berekenbare functies kan dan worden voorgesteld door een stroom Gödel-nummers (ook wel effectieve getallen genoemd). De gelijkwaardigheidstheorem van Rogers stelt criteria op grond waarvan die nummeringen van de verzameling berekenbare functies Gödel-nummeringen zijn.

Definitie en hoofdlijnen

Een Gödelnummering is kort gezegd een effectieve (meestal rekencbare) injectieve toekenning van natuurlijke getallen aan de symbolen en syntactische objecten (termen, formules, bewijzen) van een formele taal. Belangrijke eigenschappen zijn:

  • Uniciteit: elk syntactisch object krijgt precies één natuurlijk getal.
  • Effectiviteit: er bestaat een algoritme dat gegeven een object het bijbehorende Gödelgetal berekent, en vaak ook een algoritme dat gegeven een Gödelgetal het corresponderende object teruggeeft.
  • Representativiteit: syntactische bewerkingen (zoals concatenatie, het vormen van een formule uit symbolen) moeten door rekencbare bewerkingen op de Gödelgetallen te beschrijven zijn.

Gebruikelijke codering: priemfactorisatie

Het meest gebruikte en klassieke voorbeeld van een Gödelnummering gebruikt priemfactorisatie. Het idee is:

  1. Ken elk basis-symbool s van de taal een natuurlijk getal g(s) toe (bijv. een kleine index).
  2. Neem de opeenvolgende priemgetallen p1, p2, p3, ... (2, 3, 5, 7, ...).
  3. Voor een finite sequentie van symbolen s1, s2, ..., sn definieer het Gödelgetal als
    GN(s1 s2 ... sn) = p1^{g(s1)} · p2^{g(s2)} · ... · pn^{g(sn)}.

Door de unieke priemfactorisatie van natuurlijke getallen volgt dat de codering injectief is: elk getal heeft precies één ontbinding in priemfactoren, waardoor de oorspronkelijke sequentie te reconstrueren is uit het GN.

Voorbeeld (vereenvoudigd): stel g('0') = 1, g('S') = 2, g('+') = 3 en we coderen de sequentie "S 0 + 0" dan zou

GN = 2^{2} · 3^{1} · 5^{3} · 7^{1} = 4 · 3 · 125 · 7 = 10500.

Door priemfactorisatie van 10500 kan men de exponenten 2,1,3,1 aflezen en zo teruggaan naar de symbolen.

Codering van formules, bewijzen en verzamelingen

Met basiscoderingen zoals hierboven kan men complexere objecten coderen:

  • Formules en termen: gezien als sequenties van symbolen, krijgen ze een GN via de priemmethode of via pairing-functies.
  • Bewerkingen en structuur: boomstructuren (bijv. parse-bomen) worden doorgaans genummerd door geneste coderingen of door op specifieke wijze koppelingen te coderen met behulp van koppelfuncties (pairing functions).
  • Bewijzen: een bewijs (een eindige rij formules volgens afleidingsregels) kan als sequentie van Gödelgetallen worden gecodeerd, en daaruit volgt dat eigenschappen als "x is een bewijs van y" arithmetisch (door een formule van de getaltheorie) uitgedrukt kunnen worden.

Effectiviteit, inverse en equivalentie

Belangrijk voor wiskundige toepassingen is dat de toewijzing effectief is: er bestaat een berekenbare functie f zodat f(object) = GN(object), en vaak ook een berekenbare inverse g zodat g(GN) = object wanneer GN daadwerkelijk uit de codering komt. Verschillende Gödelnummeringen zijn mogelijk; het wezenlijke punt is dat ze onderling "efficiënt equivalent" zijn in de zin van de theorie van rekencodeerbaarheid. De stelling van Rogers (de gelijkwaardigheidstheorem van Rogers) geeft criterium wanneer twee nummeringen van de berekenbare functies als gelijkwaardig beschouwd kunnen worden—meer concreet: bestaan er rekencbare permutaties die de ene nummering in de andere omzetten.

Toepassingen en waarom het belangrijk is

  • Gödel's onvolledigheidstheorema: Gödel gebruikte nummering om syntactische beweringen over formules en bewijzen te vertalen naar beweringen over natuurlijke getallen. Daarmee kon hij een aritmische zin construeren die zegt "dit getal komt overeen met geen bewijs van mij", wat leidt tot de onvolledigheid van voldoende rijke consistente formele systemen.
  • Recursietheorie en computability: Gödelnummering maakt het mogelijk om partiële en totale berekenbare functies te nummeren en te bestuderen: men kan praten over "de n-de berekenbare functie".
  • Metamathematica en automatische bewijscontrole: coderingen van bewijzen en formules zijn de basis voor geautomatiseerde bewijssystemen en formalisatie van wiskunde.
  • Diagonaliserings- en fixed-point-verbindingen: via de nummering kan men formele versies van diagonaalargumenten en het fixed-point (vervangings)lemma formuleren en bewijzen binnen arithmetische systemen.

Beperkingen en praktische opmerkingen

  • Gödelnummeringen zijn in de praktijk vaak onhandig (ze leiden tot zeer grote getallen); hun belang is vooral theoretisch en conceptueel.
  • De codering is niet uniek: verschillende keuzes (anders toekennen van getallen aan symbolen, andere pairingfuncties) geven verschillende Gödelgetallen, maar de verschillende nummeringen zijn in veel opzichten equivalent door berekenbare transformaties.
  • In moderne bronnen gebruikt men vaak korte notaties zoals ⌜φ⌝ voor het Gödelgetal van een formule φ, en men spreekt van "arithmetiseren van de syntaxis".

Samengevat: een Gödelnummering is een systematische, rekencbare manier om syntactische objecten van een formele taal als natuurlijke getallen te representeren. Deze representatie maakt het mogelijk om meta-wiskundige en computability-vragen binnen de normale taal van de getaltheorie te formuleren en te analyseren, en vormt zo een kerninstrument in de logica en theoretische informatica.