Гьоделово номериране: кодиране на формули и доказателства в формални езици

Гьоделово номериране: как кодиране на формули и доказателства в формални езици свързва числа с логика, алгоритми и теорема на Гьодел.

В теорията на формалните числа номерирането на Гьодел е функция, която приписва на всеки символ и на всяка формула от даден формален език уникално естествено число, наречено число на Гьодел (GN). Концепцията е въведена и използвана за първи път от Курт Гьодел при доказването на неговата теорема за непълнота, като позволява „арифметизация“ на синтаксиса — превръщане на изрази, формули и доказателства в числа, които могат да бъдат обработвани от аритметични свойства.

Как работи номерирането

Идеята е проста: на всеки символ от алфавита на формалния език се присвоява кодово естествено число; след това последователност от символи (т.е. формула или доказателство) се кодира чрез еднозначна комбинация от тези числа. Най-често използваният и класически метод е чрез степенуване на простите числа:

• да се фиксира биективно съответствие между символи и естествени числа: symbol -> n;
• да се свърже последователността s1, s2, ..., sk със стойността 2^{n(s1)} * 3^{n(s2)} * 5^{n(s3)} * ... * p_k^{n(sk)}, където p_i е i-тата проста величина и n(si) е кодът на i-тия символ.

Защо този метод е удобен: по Основната теорема на аритметиката факторизацията на едно число в простите е уникална, което позволява от GN(формула) ефективно да се възстанови цялата последователност от символи чрез разглеждане на простите фактори и техните експоненти. Често към кодовете на символите се прибавя 1 (или се използва друга трансформация), за да се избегнат нулеви експоненти.

Алтернативни кодирания и ефективност

Има и други практически и теоретични схеми за номериране — например използване на париращи функции (pairing functions), на β-функцията на Гьодел или приложения на Китайската теорема за остатъци. Важните изисквания за едно добро номериране са:

• бьективност или поне еднозначно кодиране на валидните синтактични обекти;
• ефективност: функциите, които преобразуват символи и последователности към числа и обратно, трябва да са изчислими (често примитивно рекурсивни или рекурсивни);
• поддържане на структури: например трябва да можем ефективно да разпознаем дали дадено число кодира коректна формула или доказателство.

Приложения в логиката и теорията на изчислимостта

Номерирането на Гьодел е централно при:

• теоремата за непълнота: чрез номериране се конструира аритметическо твърдение, което формално „говори“ за собствената си недоказуемост — класически пример за диагонализация и самоприсвояване;
• аритметизация на синтаксиса: свойства като „x е доказателство за формулата y“ могат да бъдат представени като предикати в аритметиката;
• кодиране на доказателства и доказателствени системи: множество от доказуеми формули става рекурсивно изброимо множество от естествени числа;
• връзка с изчислими функции: номерирането на множеството от изчислими функции често се представя чрез индекси или потоци от числа на Гьодел (наричани още ефективни числа); това улеснява дефинирането на понятия като рекурсивност, частична рекурсивност и др.

Теорема на Роджърс и еквивалентност на номерирания

Теоремата за еквивалентност на Роджърс формулира критерии, по които различни номерирания на множеството от изчислими функции могат да се считат „еквивалентни“ като номерирания на Гьодел. Информално: две приемливи (acceptable) номерирания са взаимно пресичаеми чрез изчислима биекция — съществува компютируемо преобразуване, което превежда индексите по едно номериране в индекси по другото. Това гарантира, че основните понятия от теорията на изчислимостта не зависят от конкретния избор на номериране.

Свойства и ограничения

Номерирането само по себе си не решава проблеми за доказуемост или решимост — то предоставя средство да формулираме синтактични въпроси в аритметични термини. Много от естествените предикати за синтаксични свойства са рекурсивно изброими, но често не са решими. Именно това дава възможност за конструкция на формули, които не са разрешими в дадена формална система, демонстрирайки границите на формалните теории.

Кратък пример

• Допускаме азбука: {“0”, “S”, “+”, “×”, “=”, “(”, “)”, “¬”, “→”, “∀”, “x”, “y”, ...} и ѝ придаваме кодове: 0→1, S→2, +→3 и т.н.
• Формулата S(0)=0 може да се представи като последователност от кодове n1,n2,...,nk, която след това се кодира чрез произведение на степени на прости числа: GN = 2^{n1}·3^{n2}·5^{n3}·... .
• Чрез разлагане на GN по прости фактори лесно възстановяваме оригиналната формула.

В заключение, номерирането на Гьодел е фундаментален инструмент в логиката и теорията на изчислимите структури — то позволява да се „направи аритметика“ от синтаксиса на формални езици и така да се формулират и докажат дълбоки резултати за границите на формалните системи и механичната изчислимост.

Въпроси и отговори

Въпрос: Какво представлява номерацията на Гьодел?

Въпрос: Кой пръв използва концепцията за номерация на Гьодел?

В: Как можем да тълкуваме номерацията на Гьодел?

Въпрос: Как наричаме естествените числа, присвоени от номерирането на Гьодел?

В: Какво гласи теоремата за еквивалентност на Роджърс?

В: Какво представлява потокът от числа на Гьодел?

В: Защо номерирането на Гьодел е важно във формалната теория на числата?

Търсене по буква