Диагональная лемма

Возьмём множество натуральных чисел ${\displaystyle \mathbb {N} }$. На арифметическом языке логика первого порядка ${\displaystyle T}$ представляет^[4] собой вычислимую функцию ${\displaystyle f:\mathbb {N} \rightarrow \mathbb {N} }$, если существует формула графа ${\displaystyle {\mathcal {G}}_{f}(x,y)}$ такая, что для каждого ${\displaystyle n\in \mathbb {N} }$:

${\displaystyle \vdash _{T}\,(\forall y)[(^{\circ }f(n)=y)\Leftrightarrow {\mathcal {G}}_{f}(^{\circ }n,\,y)]}$.

Здесь ${\displaystyle {}^{\circ }n}$ — это число, соответствующее натуральному числу ${\displaystyle n}$ нулевому, согласно логике ${\displaystyle T}$.

Диагональная лемма также требует, чтобы существовал систематический способ присвоения каждой формуле ${\displaystyle {\mathcal {A}}}$ натурального числа ${\displaystyle \#({\mathcal {A}})}$ (также записывают как ${\displaystyle \#_{\mathcal {A}}}$), называемый нумерацией Гёделя. Тогда формула по логике ${\displaystyle T}$ представлена числами, соответствующими номерам Гёделя. Например, формула ${\displaystyle {\mathcal {A}}}$ выглядит как ${\displaystyle ^{\circ }\#_{\mathcal {A}}}$.

Диагональная лемма относится к теориям, способным представлять примитивно-рекурсивные функции. К таким теориям также относятся арифметика Пеано и более слабая арифметика Робинсона. Общая формулировка леммы, приведённая ниже, подтверждает, что эта теория может определять все вычислимые функции, хотя все вышеупомянутые теории обладают такой же способностью.

Пусть ${\displaystyle T}$ — логика первого порядка на языке арифметики, способна представлять все вычислимые функции, к тому же ${\displaystyle {\mathcal {F}}(y)}$ — формула одного аргумента в ${\displaystyle T}$. Тогда существует высказывание ${\displaystyle {\mathcal {C}}}$ такое, что ${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}({}^{\circ }\#_{\mathcal {C}})}$^[5].

Интуитивно понятно, что ${\displaystyle {\mathcal {C}}}$ является самореферентным высказыванием: ${\displaystyle {\mathcal {C}}}$ утверждает, что ${\displaystyle {\mathcal {C}}}$ имеет свойство ${\displaystyle {\mathcal {F}}}$. Высказывание ${\displaystyle {\mathcal {C}}}$ можно рассматривать как неподвижную точку, которая присваивает классу эквивалентности данного высказывания ${\displaystyle {\mathcal {A}}}$, класс эквивалентности высказывания ${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {A}})}$. Высказывание ${\displaystyle {\mathcal {C}}}$, построенное в доказательстве, не является буквально ${\displaystyle {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$, но доказуемо эквивалентно ему в теории ${\displaystyle T}$.

Пусть ${\displaystyle f:\mathbb {N} \to \mathbb {N} }$ функция задана:

${\displaystyle f(\#_{\mathcal {A}})=\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})]}$,

для каждой формулы ${\displaystyle {\mathcal {A}}(x)}$ с одной переменной ${\displaystyle x}$ в логике ${\displaystyle T}$, и ${\displaystyle f(n)=0}$ в противном случае. Здесь ${\displaystyle \#_{\mathcal {A}}=\#({\mathcal {A}}(x))}$ обозначает нумерацию Гёделя формулы ${\displaystyle {\mathcal {A}}(x)}$. Функция ${\displaystyle f}$ вычислима (что является допущением о схеме нумерации Гёделя), тогда формула ${\displaystyle {\mathcal {G}}_{f}(x,\,y)}$ representing ${\displaystyle f}$ in ${\displaystyle T}$.

А именно

${\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }f(\#_{\mathcal {A}})]\}}$

то есть

${\displaystyle \vdash _{T}\,(\forall y)\{{\mathcal {G}}_{f}(^{\circ }\#_{\mathcal {A}},\,y)\Leftrightarrow [y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\}}$.

Далее, рассматривая произвольную формулу ${\displaystyle {\mathcal {F}}(y)}$ с одной переменной ${\displaystyle y}$, запишем формулу ${\displaystyle {\mathcal {B}}(z)}$ как:

${\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}$

Тогда для всех ${\displaystyle {\mathcal {A}}(x)}$ с одной переменной:

${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}}$, которое утверждает ${\displaystyle \vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])}$

Заменяя ${\displaystyle {\mathcal {A}}}$ на ${\displaystyle {\mathcal {B}}}$, и определяя высказывание ${\displaystyle {\mathcal {C}}}$ как:

${\displaystyle {\mathcal {C}}:={\mathcal {B}}(^{\circ }\#_{\mathcal {B}})}$

Запишем предыдущую строку как:

${\displaystyle \vdash _{T}\,{\mathcal {C}}\Leftrightarrow {\mathcal {F}}(^{\circ }\#_{\mathcal {C}})}$

что и требовалось доказать.

Рудольф Карнап (1934) первым доказал общую самореферентную лемму^[6], которая гласит, что для любой формулы F в логике T, удовлетворяющей определённым условиям, существует формула ψ такая, что ψ ↔  F (°#( ψ )) доказуемо в Т. Работа Карнапа была сформулирована для альтернативного языка, поскольку концепция вычислимых функций ещё не была разработана в 1934 году. Мендельсон считает, что Карнап был первым, кто заявил, что нечто вроде диагональной леммы подразумевалось в рассуждениях Гёделя. Гёдель был знаком с работой Карнапа к 1937 году^[7].

Диагональная лемма тесно связана с теоремой Клини о рекурсии в теории вычислимости, и их доказательства аналогичны.