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

Эта статья о понятии математической логики. Он назван в честь диагонального аргумента Кантора в теории множеств и чисел. См. Диагонализация (значения) для получения информации о нескольких несвязанных между собой значениях этого термина в математике.

В математической логике диагональная лемма (также известная как лемма о диагонализации , лемма о самореференции) или теорема о неподвижной точке ) устанавливает существование самореферентных предложений в некоторых формальных теориях натуральных чисел — особенно в тех теориях, которые достаточно сильны, чтобы представлять все вычислимые функции . Предложения, существование которых обеспечивается диагональной леммой, могут затем, в свою очередь, использоваться для доказательства фундаментальных ограничительных результатов, таких как теоремы Гёделя о неполноте и теорема неопределимости Тарского .

Фон

Позволять $\mathbb {N}$ быть набором натуральных чисел . первого порядка Теория $T$ на языке арифметики представляет собой вычислимая функция $f:\mathbb {N} \rightarrow \mathbb {N}$ если существует формула «графика» ${\mathcal {G}}_{f}(x,y)$ на языке $T$ — то есть формула такая, что для каждого $n\in \mathbb {N}$

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

Здесь ${}^{\circ }n$ число, соответствующее натуральному числу $n$, который определяется как $n$преемник предполагаемой первой цифры $0$ в $T$.

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

Диагональная лемма применима к теориям, способным представить все примитивно-рекурсивные функции . Такие теории включают арифметику Пеано первого порядка и более слабую арифметику Робинсона и даже гораздо более слабую теорию, известную как R. Общая формулировка леммы (как указано ниже) делает более сильное предположение, что теория может представлять все вычислимые функции , но все упомянутые теории также обладают такой способностью.

Утверждение леммы

Лемма - Позволять $T$ быть теорией первого порядка на языке арифметики и способной представлять все вычислимые функции , и ${\mathcal {F}}(y)$ быть формулой в $T$ с одной свободной переменной. Тогда существует предложение ${\mathcal {C}}$ такой, что

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

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

Доказательство

Позволять $f:\mathbb {N} \to \mathbb {N}$ быть функцией, определяемой:

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

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

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

то есть

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

Теперь по произвольной формуле ${\mathcal {F}}(y)$ с одной свободной переменной $y$, определим формулу ${\mathcal {B}}(z)$ как:

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

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

$\vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow (\forall y)\{[y={}^{\circ }\#({\mathcal {A}}(^{\circ }\#_{\mathcal {A}}))]\Rightarrow {\mathcal {F}}(y)\}$

то есть

$\vdash _{T}\,{\mathcal {B}}(^{\circ }\#_{\mathcal {A}})\Leftrightarrow {\mathcal {F}}(^{\circ }\#[{\mathcal {A}}(^{\circ }\#_{\mathcal {A}})])$

Теперь замените ${\mathcal {A}}$ с ${\mathcal {B}}$, и определите предложение ${\mathcal {C}}$ как:

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

Тогда предыдущую строку можно переписать как

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

что является желаемым результатом.

(Тот же аргумент в других терминах приведен в [Раатикайнен (2015a)].)

История

Лемма называется «диагональной», поскольку она имеет некоторое сходство с диагональным аргументом Кантора . Термины «диагональная лемма» или «неподвижная точка» не встречаются ни в Курта Гёделя 1931 года статье , ни в Альфреда Тарского 1936 года статье .

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

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

См. также

• Косвенная ссылка на самого себя
• Список теорем о неподвижной точке
• Примитивная рекурсивная арифметика
• Самоссылка
• Самореферентные парадоксы

Ссылки

• Джордж Булос и Ричард Джеффри , 1989. Вычислимость и логика , 3-е изд. Издательство Кембриджского университета. ISBN   0-521-38026-X ISBN   0-521-38923-2
• Рудольф Карнап , 1934. Logische Syntax der Sprache . (Английский перевод: 2003. Логический синтаксис языка . Издательство Open Court.)
• Хаим Гайфман , 2006. « Именование и диагонализация: от Кантора до Гёделя и Клини ». Логический журнал IGPL, 14: 709–728.
• Хинман, Питер, 2005. Основы математической логики . АК Петерс. ISBN   1-56881-262-0
• Мендельсон, Эллиотт , 1997. Введение в математическую логику , 4-е изд. Чепмен и Холл.
• Пану Раатикайнен, 2015а. Лемма о диагонализации . В Стэнфордской энциклопедии философии под ред. Из Залты. Приложение к Раатикайнен (2015b).
• Пану Раатикайнен, 2015б. Теоремы Гёделя о неполноте . В Стэнфордской энциклопедии философии под ред. Залта.
• Раймонд Смалльян , 1991. Теоремы Гёделя о неполноте . Оксфордский университет. Нажимать.
• Раймонд Смалльян, 1994. Диагонализация и самореференция . Оксфордский университет. Нажимать.
• Альфред Тарский (1936). «Понятие истины в формализованных языках» (PDF) . Студия Философия . 1 :261-405. Архивировано из оригинала (PDF) 9 января 2014 года . Проверено 26 июня 2013 г.
  • Альфред Тарский , тр. Дж. Х. Вуджер, 1983. «Понятие истины в формализованных языках». Английский перевод статьи Тарского 1936 года . В книге А. Тарского под ред. Дж. Коркоран, 1983, Логика, семантика, метаматематика , Хакетт.