![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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.
Несколько лет назад Харви Фридман придумал новое, очень простое и красивое доказательство второй теоремы о неполноте Геделя. Напомню, что первая теорема о неполноте утверждает, что достаточно мощная формальная система 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.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2008-12-09 06:19 pm (UTC)минимализм
Date: 2008-12-09 06:31 pm (UTC)no subject
Date: 2008-12-09 07:07 pm (UTC)P.S.
Date: 2008-12-09 07:10 pm (UTC)no subject
Date: 2008-12-09 09:40 pm (UTC)Re: P.S.
Date: 2008-12-10 12:07 am (UTC)no subject
Date: 2008-12-10 12:08 am (UTC)Re: минимализм
Date: 2008-12-10 12:09 am (UTC)no subject
Date: 2008-12-10 03:47 am (UTC)> "... одно из условий, накладываемых на T для второй теоремы о неполноте (которые я опустил) выглядит так: если T доказывает X, то T доказывает "Т доказывает X".
По-моему это условие необходимо даже для первой теоремы Геделя. Без него из T|-G не следует противоречивость. А для второй теоремы необходимо еще чтобы сама импликация 'если T доказывает X, то T доказывает "Т доказывает X"' была теоремой Т.
Вроде бы известно, что это условие можно нарушить, выбрав хитрую арифметизацию доказуемости.
no subject
Date: 2008-12-10 11:25 am (UTC)no subject
Date: 2008-12-10 11:41 am (UTC)Переводить все на язык вычислимости - это, конечно, хорошо, но сильно нивелирует результаты о неполноте, например.
no subject
Date: 2008-12-10 12:49 pm (UTC)Да, вы правы, спасибо, это сразу следует из репрезентативности предиката доказательности в T.
Не знаю насчет хитрой арифметизации. Ясно, что арифметизация должна быть "удобной" (сигма_1, скажем), чтобы док-во Геделя работало. Если выбрать извращенную арифметизацию, которая сложнее, то док-во Геделя не пройдет, хотя неконструктивное док-во для корректных систем через неопределимость истины все равно будет работать. Вы это имеете в виду или что-то другое?
no subject
Date: 2008-12-10 03:31 pm (UTC)А "если T доказывает собственную непротиворечивость, то она противоречива" хорошо применять в философских спорах :)
no subject
Date: 2008-12-10 06:58 pm (UTC)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.
Не доказательство.
Date: 2008-12-12 10:41 am (UTC)Всё рассуждение софизм типа «сможет ли бог сделать камень который не сможет поднять».
Re: Не доказательство.
Date: 2008-12-12 03:27 pm (UTC)Для данной теоремы это просто строка символов, а вовсе не утверждение.
Как-то так.
Re: Не доказательство.
Date: 2008-12-12 09:12 pm (UTC)Теперь мы описываем машину TM, которая … проверяя каждую из них (из строк), не является ли она формальным доказательством, внутри T, утверждения "машина, кодируемая числом X, не останавливается на входных данных X". Если TM находит такое формальное доказательство, она останавливается.
Т.е. машина которую мы рассматриваем не находится в множестве машин которые она анализирует.
no subject
Date: 2008-12-14 12:35 pm (UTC)Но краткость изложения радует глаз.
no subject
Date: 2008-12-15 09:19 pm (UTC)Правда я не специалист в области логики, но все очень понятно.
Если я правильно понимаю, то в доказательстве используется классическая логика, так ведь? А если посмотреть на эту проблему с точки зрения многозначной логики, ваше мнение, что произойдет?
Еще раз спасибо.
no subject
Date: 2008-12-15 09:21 pm (UTC)no subject
Date: 2008-12-15 09:22 pm (UTC)no subject
Date: 2008-12-15 09:38 pm (UTC)Вот существует нечеткая логика, она разбивается(как я понял из Википедии) на три вида:
1. Логика Гёделя
2. Логика Лукасевича
3. Вероятностная логика
(еще я слышал про Квантовую логику)
но вот в чем отличие этих логик я не смог понять.
Если можно в двух словах опишите пожалуйста.
Спасибо.
no subject
Date: 2008-12-15 09:40 pm (UTC)(по крайней мере, я слышал, что Квантовая логика может решать подобные проблемы)
no subject
Date: 2008-12-15 10:37 pm (UTC)Мне кажется, здесь стоит говорить об истинности в какой-то мере каждого из высказываний.
Эти высказывания, похожи на границу формальной системы, так же как границу в видимом мире между двумя объетами. Ведь эта граница на очень маленьких масштабах очень размыта и очень вероятностна.
Одновременность непротеворечивости и полноты, аксиоматический аппарат - все это границы формальной системы, за их рамки выйти нельзя. Но нельзя сказать, что эта граница очень четкая, что вот допустим здесь все кончается и начинается уже другая формальная система.
Если бы мы жили на плоскости и были плоскими(как в романе Flatlandia(Плоская страна)), то линия перпендикулярная плоскости, казалась бы нам точкой, в то же время она была бы линией.
Факт противоречия, на мой взгляд, это факт двумерности формальной логики в ее классическом виде.
Написал вот много, но думаю, что все можно разом перечеркнуть, если сказать, что теорема Геделя как раз об этом и говорит, в плане того, что формальные системы с аппаратом классической логики не могут быть одновременно непротиворечивы и полны.
Спасибо.
no subject
Date: 2008-12-16 04:07 pm (UTC)Некоторый скепсис вызывает то, что классическая логика может быть погружена в многозначную. Мы можем считать, что утверждение доказуемо, если оно доказуемо с уверенностью 1, например.
Первая теорема Гёделя о неполноте говорит, что никакая достаточно сложная система не может быть полной, то есть отвечать на все вопросы. Но если мы построим формальную систему в многозначной логике, которая на любой вопрос сможет дать ответ "да" с уверенностью 1 или "нет" с уверенностью 1, то мы сможем извлечь из неё этот классический кусочек, и получить противоречие с теоремой Гёделя. То есть скорее всего ничего не получится.
no subject
Date: 2008-12-16 05:15 pm (UTC)На счет многозначной логики, я имел в виду, что двоичная логика ограничивает круг возможностей - либо неполна и непротиворечива, либо полна и тогда противоречива. В то время как в многозначной логике, на мой взгляд, возможно существование двух противоположностей одновременно(но тогда действительно, какой от этого толк).
Чуть ниже я описал общую идею.
Еще раз спасибо за ответ.
квантовый обед
Date: 2008-12-21 09:48 am (UTC)Медленно движется толпа, и мы, наконец, видим, как Сократ исчезает в створе ворот... "Следовательно, Сократ смертен".
То есть мы просто "прокрутили" в голове некий "фильм" и пересказали его основное содержание. Требуемый вывод мы не по правилам получили, а просто увидели. То есть не было тут никакой "логики" -- ни двузначной, ни многозначной. Тут как у "акына": "что вижу, о том и пою" :)
Однако "двузначность" всплывает в другом месте. Мы не только рассуждаем, изрекая некие "истины", но ещё и "изучаем" их, ибо таков предмет математической логики. И вот тут "от природы" возникает такой феномен: мы что-то хотим знать, то есть хотим уметь убедиться в истинности некого утверждения, будь то факт уровня 2*2=4 или проблема Гольдбаха -- Эйлера в теории чисел. И на этот предмет мы рассчитывам, что нам как-то могут помочь машины.
И вот отсюда всплывает "двузначность". Это не потому, что мы в рассуждении какие-то не те средства используем, а потому что у нас такой "заказ" был. Нас спросил "заказчег": конечно или бесконечно множество простых чисел-"близнецов"? Ему нужен ответ "да" или "нет", а нас он "нанял" с какой-то своей целью. Может, он просто любознательный такой, а может у него "бизнес" собственный от этого зависит. Мы же всего лишь "исполнители", и у нас нет выбора. "Да" или "нет", "терциум нон датур". При этом мы можем сколь угодно долго пытаться выйти за рамки, вспоминать об интуиционизме без "закона исключённого третьего", о квантовой механике, о "нечёткой логике", вызывать "духи" Брауэра, Гейзенберга, Лотфи Заде -- ситуация от этого не изменится. Мы получили "Заказ", и мы знаем, что ответ в "квантовой" или "нечёткой" форме нам не оплатят. Или оплатят, но в таком же виде, но когда я пойду кушать, то меня не радует перспектива съесть "квантовый обед" на "квантовые евро" :)
В это обстоятельство, похоже, всё и упирается.