Gödel-nummerering er en funktion g , der tildeler hvert objekt på et formelt sprog dets nummer. Det kan bruges til eksplicit at opregne følgende sprogobjekter: variabler, objektkonstanter, funktionssymboler, prædikatsymboler og formler bygget ud fra dem. Konstruktionen af Gödel-nummerering for objekter i en teori kaldes aritmetisering af en teori - det giver dig mulighed for at oversætte udsagn, aksiomer, teoremer, teorier til aritmetiske objekter . Det kræves, at opregningen g kan beregnes effektivt, og for ethvert naturligt tal er det muligt at bestemme, om det er et tal eller ej, og hvis det er det, så konstruer det tilsvarende objekt for sproget. Gödel-nummerering minder meget om tegn-for-tegn- kodning af strenge med tal, med den forskel, at sammenkædningen af tal af samme længde ikke bruges til at kode sekvenser af bogstavtal, men aritmetikkens grundlæggende sætning .
Gödel nummerering blev anvendt af Gödel som et værktøj til at bevise ufuldstændigheden af formel aritmetik .
Lade være en første ordens teori indeholdende variabler , objektkonstanter , funktionssymboler og prædikatsymboler , hvor er tallet og er ariteten af det funktionelle eller prædikatsymbol.
Hvert symbol i en vilkårlig førsteordensteori er forbundet med dets Gödel-nummer som følger: [1]
Gödelnummer for en vilkårlig sekvens af udtryk er defineret som følger: .
Der er også andre Gödel-nummereringer af formel aritmetik.
Generelt kaldes opregningen af et sæt en overalt defineret surjektiv mapping . Hvis , så kaldes nummeret på objektet . Særlige tilfælde - sprog og teorier.