Gödel nummerering

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 .

En variant af Gödel-nummereringen af ​​førsteordens formelle teori

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.

Eksempel

Generaliseringer

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.

Noter

  1. Mendelssohn, 1971 , §4. Aritmetisering, Gödel-numre, s. 151-152.

Litteratur

Se også