W formalnej teorii liczb numeracja Gödla jest funkcją, która każdemu symbolowi i formule pewnego języka formalnego przypisuje unikalną liczbę naturalną zwaną liczbą Gödla (GN). Koncepcja ta została po raz pierwszy użyta przez Kurta Gödla do dowodu jego twierdzenia o niezupełności.

Numeracja Gödla może być interpretowana jako kodowanie, w którym każdemu symbolowi notacji matematycznej przyporządkowana jest liczba, a strumień liczb naturalnych może reprezentować pewną formę lub funkcję. Numeracja zbioru funkcji obliczalnych może być wtedy reprezentowana przez strumień liczb Gödla (zwanych też liczbami efektywnymi). Twierdzenie równoważności Rogersa podaje kryteria, dla których te numeracje zbioru funkcji obliczalnych są numeracjami Gödla.

Definicja i konstrukcja

W najczęściej stosowanym schemacie numeracji Gödla każdy symbol języka oznacza się pewną liczbą kodową (np. naturalną), a następnie całą sekwencję symboli (czyli formułę lub dowód) koduje się jako pojedynczą liczbę naturalną dzięki rozkładowi na czynniki pierwsze. Typowa konstrukcja wygląda następująco:

  • przypisz każdemu symbolowi s liczbę kodową kod(s) (np. kolejne liczby naturalne);
  • dla sekwencji symboli s1, s2, ..., sn zdefiniuj numer Gödla jako
    GN(s1...sn) = 2^{kod(s1)} · 3^{kod(s2)} · 5^{kod(s3)} · ... · p_n^{kod(sn)}, gdzie p_k oznacza k–tą liczbę pierwszą;
  • uniwersalność schematu opiera się na zasadzie niezmienności rozkładu na czynniki pierwsze: każdej sekwencji odpowiada inna liczba.

Taki zapis czyni możliwą „aritmetyzację składni” — własności syntaktyczne formuł można opisać i badać w języku arytmetyki poprzez operacje na ich liczbach Gödla.

Przykład

Prosty, ilustracyjny przykład mapowania symboli (przykładowe przypisania):

  • '(' → 1, ')' → 2, '¬' → 3, '→' → 4, '∀' → 5, '∃' → 6, 'P' → 7, 'Q' → 8, 'x' → 9, 'y' → 10

Formuła ∀x (P(x) → ∃y Q(x,y)) przy powyższym przypisaniu i kodowaniu przez potęgi kolejnych liczb pierwszych ma numer Gödla równy:

2^{kod('∀')} · 3^{kod('x')} · 5^{kod('(')} · 7^{kod('P')} · 11^{kod('(')} · ... i tak dalej — konkretny wynik to duża liczba naturalna jednoznacznie reprezentująca tę formułę. Dzięki temu z faktu o tej liczbie można odtworzyć pierwotną sekwencję symboli.

Właściwości i formalna użyteczność

  • Jednoznaczność: konstrukcja oparta na rozkładzie na czynniki pierwsze gwarantuje, że różne sekwencje symboli otrzymają różne liczby Gödla.
  • Efektywność: wiele popularnych schematów numeracji jest obliczalnych (np. funkcje przekształcające sekwencje na GN i odwrotnie są rekurencyjne lub nawet pierwotnie rekurencyjne), co pozwala traktować syntaktyczne operacje jako obliczenia.
  • Aritymetyzacja składni: relacje typu „x jest kodem formuły”, „y jest dowodem formuły o kodzie x” czy „z jest wynikiem podstawienia” można wyrazić jako relacje arytmetyczne nad liczbami naturalnymi.
  • Równoważność schematów: choć konkretna numeracja zależy od wyboru kodów symboli i sposobu kodowania sekwencji, wszystkie naturalne numeracje są równoważne w sensie obliczalności — istnieje obliczalna bijekcja przekształcająca jedną numerację w drugą. To jest istotne w kontekście twierdzenia równoważności Rogersa.

Zastosowania

Numeracja Gödla ma wiele kluczowych zastosowań w logice matematycznej i teorii obliczeń:

  • Dowód twierdzeń o niezupełności: Gödel użył numeracji, by „wewnętrznie” odwołać się w arytmetyce do własnych zdań i dowodów — to umożliwiło skonstruowanie autoodwołujących się formuł typu „to zdanie nie ma dowodu”.
  • Reprezentacja relacji obliczalnych: dzięki numeracji można zdefiniować w arytmetyce predicate opisujące relacje obliczalne (np. relacja „e numeruje funkcję f”), co jest fundamentem teorii rekurencyjnej.
  • Metamatematyka: badanie własności teorii formalnych (np. zupełności, spójności, zdawalności) często opiera się na analizie liczb Gödla dowodów i aksjomatów.
  • Teoria dowodu i automatyczne dowodzenie: w informatyce i weryfikacji formalnej kodowanie dowodów i formuł jako liczb jest używane przy implementacji systemów dowodzących oraz przy analizie złożoności algorytmów sprawdzających poprawność dowodów.
  • Ograniczenia i twierdzenia o nieodwracalności: pojęcia takie jak nierozstrzygalność, twierdzenie Tarskiego o nieokreśloności prawdy w formalnym systemie czy wynik Gödla znajdują tu swoje arytmetyczne sformułowanie.

Warianty i uwagi praktyczne

  • Istnieją różne schematy kodowania: oprócz kodowania przez potęgi kolejnych liczb pierwszych stosuje się np. parowanie Cantora, kodowanie prefiksowe, czy inne efektywne metody. Każdy z nich ma zalety zależne od kontekstu (np. łatwość odczytu, ograniczenie wzrostu liczb itp.).
  • W praktyce większość rezultatów teorii nie zależy od konkretnego wyboru numeracji — ważne, by numeracja była obliczalna; w przeciwnym razie traci się możliwość „przeniesienia” składni do arytmetyki.
  • Numeracje stosowane w analizie funkcji obliczalnych bywają nazywane także numeracjami efektywnymi i są centralnym pojęciem w teorii stopnia obliczalności oraz w rekursywności.

Podsumowując, numeracja Gödla to narzędzie pozwalające zamienić obiekty syntaktyczne (symbole, formuły, dowody) na liczby naturalne tak, aby własności syntaktyczne dały się badać arytmetycznie. Pozwala to na głębokie połączenie logiki, arytmetyki i teorii obliczeń, co leży u podstaw wielu fundamentalnych twierdzeń matematyki współczesnej.