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

Высказывание в математической логике

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

Фон

Пусть — множество натуральных чисел . Теория первого порядка на языке арифметики представляет ^[3] вычислимую функцию , если существует «графовая» формула на языке — то есть формула такая, что для каждого ${\displaystyle \mathbb {N} }$ ${\displaystyle T}$ ${\displaystyle f:\mathbb {N} \rightarrow \mathbb {N} }$ ${\displaystyle {\mathcal {G}}_{f}(x,y)}$ ${\displaystyle T}$ ${\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 n}$ ${\displaystyle 0}$ ${\displaystyle T}$

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

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

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

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

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

Интуитивно понятно, что является самореферентным предложением: говорит, что имеет свойство . Предложение также можно рассматривать как фиксированную точку операции, которая присваивает классу эквивалентности данного предложения класс эквивалентности предложения (класс эквивалентности предложения — это множество всех предложений, которым оно доказуемо эквивалентно в теории ). Предложение, построенное в доказательстве, не является буквально тем же самым, что , но доказуемо эквивалентно ему в теории . ${\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 T}$ ${\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)}$ ${\displaystyle f}$ ${\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}})}$

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

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

История

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

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

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

Смотрите также

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

Примечания

1. Гаек, Петр ; Пудлак, Павел (1998) [первое издание 1993]. Метаматематика арифметики первого порядка . Перспективы математической логики (1-е изд.). Springer. ISBN 3-540-63648-X. ISSN  0172-6641. В современных текстах эти результаты доказываются с помощью известной леммы о диагонализации (или самореференции), которая уже подразумевается в доказательстве Гёделя.
2. См. Булос и Джеффри (2002, раздел 15) и Мендельсон (1997, Предложение 3.37 и Поправление 3.44).
3. Подробнее о представимости см. Hinman 2005, стр. 316.
4. Smullyan (1991, 1994) — стандартные специализированные ссылки. Лемма — это Prop. 3.34 в Mendelson (1997), и она рассматривается во многих текстах по базовой математической логике, таких как Boolos and Jeffrey (1989, sec. 15) и Hinman (2005).
5. См., например, Гайфман (2006).
6. Курт Гёдель , Собрание сочинений, Том I: Публикации 1929–1936 , Oxford University Press, 1986, стр. 339.
7. См. Собрание сочинений Гёделя , т. 1 , Oxford University Press, 1986, стр. 363, прим. 23.

Ссылки

• Джордж Булос и Ричард Джеффри , 1989. Вычислимость и логика , 3-е изд. Cambridge University Press. ISBN 0-521-38026-X ISBN 0-521-38923-2   
• Рудольф Карнап , 1934. Logische Syntax der Sprache . (Перевод на английский: 2003. Логический синтаксис языка . Open Court Publishing.)
• Хаим Гайфман , 2006. «Именование и диагонализация: от Кантора к Гёделю и Клини». Logic Journal of the IGPL, 14: 709–728.
• Хинман, Питер, 2005. Основы математической логики . AK Peters. ISBN 1-56881-262-0 
• Мендельсон, Эллиотт , 1997. Введение в математическую логику , 4-е изд. Chapman & Hall.
• Пану Раатикайнен, 2015а. Лемма о диагонализации. В Стэнфордской энциклопедии философии под ред. Залта. Приложение к Раатикайнен (2015b).
• Panu Raatikainen, 2015b. Теоремы Гёделя о неполноте. В Стэнфордской энциклопедии философии , под ред. Zalta.
• Рэймонд Смаллиан , 1991. Теоремы Гёделя о неполноте , Oxford Univ. Press.
• Рэймонд Смаллиан, 1994. Диагонализация и самореференция . Oxford Univ. Press.
• Альфред Тарский (1936). «Der Wahrheitsbegriff in den formalisierten Sprachen» (PDF) . Студия Философия . 1 : 261–405. Архивировано из оригинала (PDF) 9 января 2014 года . Проверено 26 июня 2013 г.
  • Альфред Тарский , пер. JH Woodger, 1983. "The Concept of Truth in Formalized Languages". Английский перевод статьи Тарского 1936 года. В A. Tarski, ред. J. Corcoran, 1983, Logic, Semantics, Metamathematics , Hackett.