оригинальное доказательство второй теоремы неполноты

[avva]

(эта запись может быть интересна тем, кому нравятся математика, логика, теоремы о неполноте)

Несколько лет назад Харви Фридман придумал новое, очень простое и красивое доказательство второй теоремы о неполноте Геделя. Напомню, что первая теорема о неполноте утверждает, что достаточно мощная формальная система T обязательно неполна, т.е. есть утверждения о натуральных числах, которые она не может ни доказать ни опровергнуть (и из этого следует сразу, что есть истинные утверждения, которые она не может доказать). Вторая теорема о неполноте утверждает, что достаточно мощная (в несколько другом смысле) T не может доказать собственную непротиворечивость, если она действительно непротиворечива (если система противоречива, то она может доказать вообще все, что угодно, включая собственную непротиворечивость).

Вот доказательство Фридмана (многие технические подробности я опускаю). Главная идея его похожа на доказательство нерешаемости теоремы об остановке машин Тьюринга, где, напоминаю, строится определенная машина, которой в качестве входа дается ее собственное описание. Несколько технических объяснений я вынес в сноски в конце записи.

Мы начинаем с формальной системы T. Мы предполагаем, что T достаточно мощна, чтобы уметь доказывать все истинные утверждения вида "машина [M] останавливается на входных данных X" [1].

Теперь мы описываем машину TM, которая делает следующую хитрую штуку: получив на входе число X, она перебирает все возможные строки символов одну за другой, в порядке возрастания длины, проверяя каждую из них, не является ли она формальным доказательством, внутри T, утверждения "машина, кодируемая числом X, не останавливается на входных данных X". Если TM находит такое формальное доказательство, она останавливается. Пока не находит - работает и пытается найти.

Запустим машину TM, дав ей на вход число [TM], описывающее ее самое.

Возможны два случая:

1. T доказывает "ТМ не останавливается, если дать ей [TM]". Раз такое доказательство существует, то TM, занимающаяся его поиском, его найдет и остановится. Следовательно (см. абзац про исходные предположения) Т сможет доказать этот факт, т.е. Т доказывает "ТМ останавливается, если дать ей [TM]". Значит, Т противоречива.

2. Т не доказывает "ТМ не останавливается, если дать ей [TM]". Раз такого доказательства нет, то машина TM никогда не остановится, если дать ей [TM] - ведь она ищет именно такое доказательство.

Первый вывод. Если Т непротиворечива, то первый случай невозможен, и поэтому верен второй: во-первых, TМ никогда не остановится на входных данных [TM], во-вторых, T бессильна доказать этот факт. Мы доказали вариант первой теоремы о неполноте Геделя, а именно: предполагая, что T непротиворечива, нашли истинное утверждение, которое Т не может доказать. Это не самый сильный вариант первой теоремы, но все равно неплохо.

Второй вывод. Предыдущие рассуждения, включая "первый вывод", легко формализовать внутри T, если она достаточно мощна (здесь я опускаю много технических деталей). Следовательно, T + Con(T), где Con(T) обозначает "Т непротиворечива", доказывает два формализованных утверждения:

a) "TM не остановится на [TM]", и
b) "T не доказывает, что TM не остановится на [TM]".

Дополнительное предположение Con(T) тут соответствует фразе "Если Т непротиворечива" в "первом выводе".

Предположим теперь, что T доказывает собственную непротиворечивость, т.е. утверждение Con(T). Тогда из предыдущего абзаца следует, что T сама по себе, без дополнительных предположений, доказывает a) и b).
Однако тогда из a) также следует, что Т доказывает

c) "Т доказывает, что ТМ не остановится на [TM]" [2],

что прямо противоречит b). Следовательно, если T доказывает собственную непротиворечивость, то она противоречива; иными словами, если в Т нет противоречия, то она не может это доказать. Q.E.D.

Сноски:

[1] Здесь и далее [M] обозначает число, описывающее устройство машины M. Названное требование на самом деле очень слабо, потому что доказать утверждение "[М] останавливается на входных данных X", если оно истинно, очень легко: оно записывается как что-то вроде "существует число, описывающее последовательность конфигураций, каждая из которых содержит описание ленты, положение считывающей головки, и состояние машины, причем в первой из них на ленте написано X, в последней машина находится в состоянии остановки, и переход между каждыми соседними конфигурациями совершается согласно правилам перехода машины [M]". Все эти условия легко записать простыми формулами, и доказать внутри формальной системы, умеющей всего лишь доказывать основные свойства арифметических действий.

[2] Это верно потому, что одно из условий, накладываемых на T для второй теоремы о неполноте (которые я опустил) выглядит так: если T доказывает X, то T доказывает "Т доказывает X". Полностью список из трех условий называется Hilbert-Lob derivability conditions.

Comments

[cema.livejournal.com]

Ага, спасибо.

минимализм

[falcao.livejournal.com]

Прекрасно изложено! Очень понятное рассуждение как само по себе, так и на уровне "техники". Особенно приятно то, что оно является "минималистским", то есть использует минимум необходимых средств.

Re: минимализм

[avva.livejournal.com]

Спасибо!

[alexeybobkov]

Хорошо, да. Предположив, что система содержит доказательство собственной непротиворечивости, мы вполне конструктивно строим противоречивое утверждение.

P.S.

[alexeybobkov]

Оригинального гёделевского доказательства я не знаю, вполне вероятно, что оно также конструктивное. Но тут-то совсем всё просто.

Re: P.S.

[avva.livejournal.com]

Тоже конструктивное. Но здесь действительно проще проследить, за счет того, что значительная часть конструкция прячется в интуитивно понятных Тьюринг-машинах.

[(Anonymous)]

вы уверены, что это новое доказательство? по-моему, фольклор бородатый. я до всех этих идей сам когда-то додумался и даже не очень огорчился, когда узнал, что не первый, настолько все лежит на поверхности. конечно, очень возможно, что я ошибаюсь, надо погуглить.

[avva.livejournal.com]

Оно действительно походит на фольклор, но Фридман спросил на проф. рассылке, когда его придумал - никто не вспомнил предшественников. Идея простая и в каком-то смысле напрашивающаяся, не спорю, но непохоже, чтобы кто-то именно ее до того формулировал.

[kirenenko.livejournal.com]

Спасибо.

> "... одно из условий, накладываемых на T для второй теоремы о неполноте (которые я опустил) выглядит так: если T доказывает X, то T доказывает "Т доказывает X".

По-моему это условие необходимо даже для первой теоремы Геделя. Без него из T|-G не следует противоречивость. А для второй теоремы необходимо еще чтобы сама импликация 'если T доказывает X, то T доказывает "Т доказывает X"' была теоремой Т.
Вроде бы известно, что это условие можно нарушить, выбрав хитрую арифметизацию доказуемости.

[avva.livejournal.com]

По-моему это условие необходимо даже для первой теоремы Геделя.

Да, вы правы, спасибо, это сразу следует из репрезентативности предиката доказательности в T.

Не знаю насчет хитрой арифметизации. Ясно, что арифметизация должна быть "удобной" (сигма_1, скажем), чтобы док-во Геделя работало. Если выбрать извращенную арифметизацию, которая сложнее, то док-во Геделя не пройдет, хотя неконструктивное док-во для корректных систем через неопределимость истины все равно будет работать. Вы это имеете в виду или что-то другое?

[kirenenko.livejournal.com]

I was talking only about the second theorem and was referring to Feferman's "arithmetization in a general setting".
Here is my (very limited) understanding of it:
It is possible to come up with some very tricky arithmetization of provability (and consistency). In that arithmetization, all important properties of provability are preserved, but T cannot express (or prove?) (T|-X -> T|-(Provable(X))) (although it's true). That makes it impossible to formally prove the second theorem. Moreover (if I'm not mistaken) with the new "definitions" of provability and consistency the second theorem is actually false: T can "prove" its "consistency".

And about non-syntactic, model-theoretic proofs. Doesn't the second theorem become a trivial implication of the first one when you assume correctness and do away with all syntactic rigor?

Sorry if I'm not making sense: I haven't been exposed to logic in a while.
And sorry for my bad English. I don't have a Russian keyboard here.

[cousin-it.livejournal.com]

Мне это казалось очевидным, но хорошо, что есть формализация. Вообще предпочитаю не думать про аксиомы, неполноту etc., а все переводить на язык вычислимости. Вы, кстати, читали PHYS771 (http://www.scottaaronson.com/democritus/default.html) Скотта Ааронсона? Очень весело.

[avva.livejournal.com]

Я отложил его на потом, но собираюсь в принципе прочесть.

Переводить все на язык вычислимости - это, конечно, хорошо, но сильно нивелирует результаты о неполноте, например.

[nine_k]

Краса.
А "если T доказывает собственную непротиворечивость, то она противоречива" хорошо применять в философских спорах :)

Не доказательство.

[mozgglaz.livejournal.com]

Поскольку «Если TM находит такое формальное доказательство, она останавливается», то утверждение «ТМ не останавливается, если дать ей [TM]» заведомо противоречащее и не канает для доказательства от обратного.

Всё рассуждение софизм типа «сможет ли бог сделать камень который не сможет поднять».

Re: Не доказательство.

[zelych.livejournal.com]

«ТМ не останавливается, если дать ей [TM]» -- это утверждение в теории Т.
Для данной теоремы это просто строка символов, а вовсе не утверждение.

Как-то так.

Re: Не доказательство.

[mozgglaz.livejournal.com]

Нет, не в теории, а в условии:
Теперь мы описываем машину TM, которая … проверяя каждую из них (из строк), не является ли она формальным доказательством, внутри T, утверждения "машина, кодируемая числом X, не останавливается на входных данных X". Если TM находит такое формальное доказательство, она останавливается.

Т.е. машина которую мы рассматриваем не находится в множестве машин которые она анализирует.

[alaev.livejournal.com]

Теоремы Гёделя, будучи очень широко известными, постоянно обдумываются и обсуждаются большим числом людей. Например, преподавателями логики. Я думаю, что такого сорта доказательства действительно являются широко известными, и тут очень трудно сказать что-то новое. Идея доказательства именно в этом.

Но краткость изложения радует глаз.

[eugeni-timofeev.livejournal.com]

Спасибо автору за столь красивое доказательство.
Правда я не специалист в области логики, но все очень понятно.

Если я правильно понимаю, то в доказательстве используется классическая логика, так ведь? А если посмотреть на эту проблему с точки зрения многозначной логики, ваше мнение, что произойдет?

Еще раз спасибо.

[avva.livejournal.com]

Классическая логика, да. Не знаю, как здесь многозначная логика что-либо изменит и зачем она здесь нужна, извините.

[eugeni-timofeev.livejournal.com]

Я сам, если честно говорить, не сильно понимаю, что она сможет изменить, но на уровне интуиции, мне думается, что она снимает противоречие.
(по крайней мере, я слышал, что Квантовая логика может решать подобные проблемы)

[alaev.livejournal.com]

Как я понял, Вы хотели спросить не меня, но попробую ответить. Может быть, из этой идеи и можно что-то извлечь, я не знаю.

Некоторый скепсис вызывает то, что классическая логика может быть погружена в многозначную. Мы можем считать, что утверждение доказуемо, если оно доказуемо с уверенностью 1, например.

Первая теорема Гёделя о неполноте говорит, что никакая достаточно сложная система не может быть полной, то есть отвечать на все вопросы. Но если мы построим формальную систему в многозначной логике, которая на любой вопрос сможет дать ответ "да" с уверенностью 1 или "нет" с уверенностью 1, то мы сможем извлечь из неё этот классический кусочек, и получить противоречие с теоремой Гёделя. То есть скорее всего ничего не получится.

[eugeni-timofeev.livejournal.com]

Спасибо за ответ.
На счет многозначной логики, я имел в виду, что двоичная логика ограничивает круг возможностей - либо неполна и непротиворечива, либо полна и тогда противоречива. В то время как в многозначной логике, на мой взгляд, возможно существование двух противоположностей одновременно(но тогда действительно, какой от этого толк).
Чуть ниже я описал общую идею.

Еще раз спасибо за ответ.

[eugeni-timofeev.livejournal.com]

Сильно извиняюсь, оставил комментарий к комментарию, а хотел откомментировать пост.

[eugeni-timofeev.livejournal.com]

И еще вопросик, если можно(просто больше специалистов кроме вас я не знаю).
Вот существует нечеткая логика, она разбивается(как я понял из Википедии) на три вида:
1. Логика Гёделя
2. Логика Лукасевича
3. Вероятностная логика

(еще я слышал про Квантовую логику)

но вот в чем отличие этих логик я не смог понять.
Если можно в двух словах опишите пожалуйста.

Спасибо.

[eugeni-timofeev.livejournal.com]

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

Одновременность непротеворечивости и полноты, аксиоматический аппарат - все это границы формальной системы, за их рамки выйти нельзя. Но нельзя сказать, что эта граница очень четкая, что вот допустим здесь все кончается и начинается уже другая формальная система.

Если бы мы жили на плоскости и были плоскими(как в романе Flatlandia(Плоская страна)), то линия перпендикулярная плоскости, казалась бы нам точкой, в то же время она была бы линией.

Факт противоречия, на мой взгляд, это факт двумерности формальной логики в ее классическом виде.

Написал вот много, но думаю, что все можно разом перечеркнуть, если сказать, что теорема Геделя как раз об этом и говорит, в плане того, что формальные системы с аппаратом классической логики не могут быть одновременно непротиворечивы и полны.

Спасибо.

квантовый обед

[falcao.livejournal.com]

Когда проводятся какие-то содержательные рассуждения, то совершенно неважно, какой вид "логики" используется. Можно считать, что вообще никакой. Мой любимый пример на эту тему такой. Возьмём классический силлогизм о Сократе, но при этом забудем про "учебнеги", про гимназические правила, про "модус" bArbArA и прочее. Вот нам говорят: "все люди смертны". Что мы себе представляем? Большую толпу, медленно и понуру бредущую к воротам с надписью "Смерть". А вот это кто идёт? Ба, да это ж наш старый знакомый Сократ! Он же человек, он идёт среди всех -- даром что знаменитость!

Медленно движется толпа, и мы, наконец, видим, как Сократ исчезает в створе ворот... "Следовательно, Сократ смертен".

То есть мы просто "прокрутили" в голове некий "фильм" и пересказали его основное содержание. Требуемый вывод мы не по правилам получили, а просто увидели. То есть не было тут никакой "логики" -- ни двузначной, ни многозначной. Тут как у "акына": "что вижу, о том и пою" :)

Однако "двузначность" всплывает в другом месте. Мы не только рассуждаем, изрекая некие "истины", но ещё и "изучаем" их, ибо таков предмет математической логики. И вот тут "от природы" возникает такой феномен: мы что-то хотим знать, то есть хотим уметь убедиться в истинности некого утверждения, будь то факт уровня 2*2=4 или проблема Гольдбаха -- Эйлера в теории чисел. И на этот предмет мы рассчитывам, что нам как-то могут помочь машины.

И вот отсюда всплывает "двузначность". Это не потому, что мы в рассуждении какие-то не те средства используем, а потому что у нас такой "заказ" был. Нас спросил "заказчег": конечно или бесконечно множество простых чисел-"близнецов"? Ему нужен ответ "да" или "нет", а нас он "нанял" с какой-то своей целью. Может, он просто любознательный такой, а может у него "бизнес" собственный от этого зависит. Мы же всего лишь "исполнители", и у нас нет выбора. "Да" или "нет", "терциум нон датур". При этом мы можем сколь угодно долго пытаться выйти за рамки, вспоминать об интуиционизме без "закона исключённого третьего", о квантовой механике, о "нечёткой логике", вызывать "духи" Брауэра, Гейзенберга, Лотфи Заде -- ситуация от этого не изменится. Мы получили "Заказ", и мы знаем, что ответ в "квантовой" или "нечёткой" форме нам не оплатят. Или оплатят, но в таком же виде, но когда я пойду кушать, то меня не радует перспектива съесть "квантовый обед" на "квантовые евро" :)

В это обстоятельство, похоже, всё и упирается.