En Gödelnumrering är en metod för att ge varje symbol, varje formel och ibland även hela bevis en unik kod i form av ett naturligt tal. I formell talteori används sådana kodningar för att göra syntax till ett objekt som kan behandlas med aritmetik. En sådan kodning är i grunden ett systematiskt sätt att tilldela tecken och uttryck talvärden i ett formellt språk.
Idén kallas ofta arithmetisering av syntax. När en sats, ett teckenföljd eller en regel kan översättas till ett tal blir det möjligt att tala om formella uttryck med hjälp av själva talen. Då kan man beskriva egenskaper hos formler, till exempel om de är välformade, om de följer av en annan sats eller om de förekommer i ett bevis, utan att lämna det aritmetiska ramverket.
Begreppet blev berömt genom Kurt Gödel, som använde en sådan kodning i arbetet som ledde till ofullständighetssatsen. Genom att låta matematiska uttryck representeras av tal kunde han formulera påståenden som i praktiken handlar om sina egna beskrivningar och bevisbarhet. Det var en avgörande innovation i modern logik, eftersom den band samman språk, bevis och talteori på ett ovanligt direkt sätt.
Hur en Gödelnumrering fungerar
Det finns ingen enda obligatorisk Gödelnumrering; många olika kodningar är möjliga. Det viktiga är att varje relevant objekt får ett unikt nummer och att kodningen går att avläsa och hantera på ett effektivt sätt. I praktiken kan man till exempel:
- låta varje enskild symbol få ett eget tal;
- koda en formel som en följd av tal som speglar ordningen i matematisk notation;
- använda primtalsupphöjningar, binära strängar eller andra entydiga kodningsmetoder.
Poängen är inte att talet i sig har någon djup betydelse, utan att det fungerar som en bärare av information. Samma idé används i datavetenskap när text, instruktioner eller strukturer lagras som bitmönster, även om Gödelnumrering har ett särskilt logiskt syfte.
Betydelse i logik och beräkningsteori
Gödelnumreringar spelar en central roll i formell talteori och i studiet av beräkningsbara funktioner. När funktioner och program kan ges nummer blir det möjligt att undersöka dem med matematiska metoder. I teorin om effektiv numrering skiljer man därför mellan godtyckliga kodningar och sådana som verkligen är användbara för beräkning och resonerande.
Rogers ekvivalenssats ger ett klassiskt kriterium för när två sådana numreringar i praktiken är likvärdiga. I grova drag säger den att rimliga och effektiva numreringar av de beräkningsbara funktionerna kan översättas till varandra på ett kontrollerat sätt. Det gör att man kan jämföra olika kodningar utan att låsa sig vid en enda teknisk konstruktion.
I dag används begreppet främst som ett grundläggande verktyg i logik, teoretisk datavetenskap och metamatematik. Det hjälper till att visa hur uttalanden om språk, bevis och algoritmer kan översättas till frågor om tal. Därför är Gödelnumrering inte bara en historisk kuriosa, utan en av de metoder som gjorde modern matematisk logik möjlig.
