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

редактировать

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

Содержание

1 Предпосылки
2 Формулировка леммы
3 Доказательство
4 История
5 См. Также
6 Примечания
7 Ссылки

Предпосылки

Пусть $N { \ displaystyle \ mathbb {N}}$ $\ mathbb {N}$ - набор натуральных чисел. A теория T представляет вычислимую функцию $f: N → N {\ displaystyle f: \ mathbb {N} \ rightarrow \ mathbb {N}}$ ${\ displaystyle f: \ mathbb {N} \ rightarrow \ mathbb {N}}$ , если существует " граф "предикат $Γ е (x, y) {\ displaystyle \ Gamma _ {f} (x, y)}$ ${\ displaystyle \ Gamma _ {f} (x, y)}$ на языке T такой, что для каждого $x ∈ N { \ displaystyle x \ in \ mathbb {N}}$ ${\ displaystyle x \ in \ mathbb {N}}$ , T доказывает

∀ y (∘ f (x) = y ⇔ Γ f (∘ x, y)) {\ displaystyle \ forall y \ quad \ left ({} ^ {\ circ} f (x) = y \ Leftrightarrow \ Gamma _ {f} ({} ^ {\ circ} x, y) \ right)}

{\ displaystyle \ forall y \ quad \ left ({} ^ {\ circ} f (x) = y \ Leftrightarrow \ Gamma _ {f} ({} ^ {\ circ} x, y) \ right)}

Здесь $∘ x {\ displaystyle {} ^ {\ circ} x}$ ${\ displaystyle {} ^ {\ circ} x}$ - это число, соответствующее натуральному числу $x {\ displaystyle x}$ $x$ , которое определяется как закрытый термин 1+ ··· +1 ( $x {\ displaystyle x}$ $x$ единиц) и $∘ f (x) {\ displaystyle {} ^ {\ circ} f (x)}$ ${\ displaystyle {} ^ {\ circ} f (x)}$ - это число, соответствующее $f (x) {\ displaystyle f (x)}$ $f(x)$ .

Диагональная лемма также требует, чтобы существовал систематический способ присвоения каждой формуле θ натурального числа # (θ) назвал свое число Гёделя. Формулы затем могут быть представлены в рамках теории цифрами, соответствующими их числам Гёделя. Например, θ представлен как ° # (θ)

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

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

Пусть T первого порядка теория на языке арифметики и способна представить все вычислимые функции. Пусть F - формула языка с одной свободной переменной, тогда:

Лемма - существует предложение $ψ {\ displaystyle \ psi}$ $\ psi$ такое, что $ψ ⟺ F (∘ # (ψ)) {\ displaystyle \ psi \ iff F (^ {\ circ} \ # (\ psi))}$ ${\ displaystyle \ psi \ iff F (^ {\ circ} \ # (\ psi))}$ доказуемо в T.

Интуитивно $ψ {\ displaystyle \ psi}$ $\ psi$ - это референциальное предложение, в котором говорится, что $ψ {\ displaystyle \ psi}$ $\ psi$ имеет свойство F. Предложение $ψ {\ displaystyle \ psi}$ $\ psi$ также можно рассматривать как фиксированную точку операции, присваиваемой каждой формуле $θ {\ displaystyle \ theta}$ $\ theta$ предложение $F (∘ # (θ)) {\ displaystyle F (^ {\ circ} \ # (\ theta))}$ ${\ displaystyle F (^ {\ circ} \ # (\ theta))}$ . Выражение $ψ {\ displaystyle \ psi}$ $\ psi$ , построенное в доказательстве, не совсем то же самое, что $F (∘ # (ψ)) {\ displaystyle F (^ {\ circ} \ # (\ psi))}$ ${\ displaystyle F (^ {\ circ} \ # (\ psi))}$ , но доказуемо эквивалентен ему в теории T.
Доказательство
Пусть f: N→N- функция, определяемая:
f (# (θ)) = # (θ (° # (θ)))
для каждой T-формулы θ в одной свободной переменной, и f (n) = 0 в противном случае. Функция f вычислима, поэтому существует формула Γ f, представляющая f в T. Таким образом, для каждой формулы θ, T доказывает
(∀y) [Γ f (° # (θ), y) ↔ y = ° f (# (θ))],
то есть
(∀y) [Γ f (° # (θ), y) ↔ y = ° # (θ (° # (θ)))].
Теперь определим формулу β (z) как:
β (z) = (∀y) [Γ f (z, y) → F (y)].
Тогда T доказывает, что
β (° # (θ)) ↔ (∀y) [y = ° # (θ (° # (θ))) → F (y)],
то есть
β (° # (θ)) ↔ F (° # (θ (° # (θ)))).
Теперь возьмем θ = β и ψ = β (° # (β)), а предыдущее предложение переписывается в ψ ↔ F (° # (ψ)), что является желаемым результатом.

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

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

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