Суть формулы Геделя состоит в том, что она выдает результат иной, чем результат проверки доказательства. Доказательство доказуемости окажется доказательством недоказуемости и наоборот.
Какой бы сложной ни была теория, всегда можно построить чуть более сложную конструкцию, которая будет поступать вопреки предсказаниям данной теории. У любой теории есть область интерпретации и всегда можно построить нечто такое, что находится не просто вне этой области, но в чем-то противоположно этой области.
В достаточно выразительной теории можно написать не только формулу G, поступающую наоборот по отношению к теории T, но в отношении любого наперед заданного метода проверки N можно написать формулу GN, поступающую наоборот по отношению к предсказанию N (в том числе наоборот относительно того предсказания, которое N делает про GN). Поэтому для любого заранее заданного метода проверки N в достаточно выразительной теории можно подобрать такие формулы GN, про которые данный метод проверки не может сказать ни "доказуема", ни "недоказуема". Поэтому достаточно выразительная теория неразрешима вообще, ни для какой теории она не является вполне понятной.
Замечу, что со стороны можно доказать G. Найдется Теория T2, в которой G будет просто аксиомой и никаких противоречий не возникнет. Ведь тексты доказательств в теории T2 отличны от текстов доказательств теории T, а формула G сформулирована именно для текстов доказательств теории T и именно в силу этого доказательство G создает противоречие в T, но не в T2. Но для теории T2 в теории T все равно найдутся непостижимые (с точки зрения доказуемости/недоказуемости) утверждения. И можно построить иную теорию T3, которая понимает что-то, непонятное для T2, и все равно в T остаются еще какие-то неразрешимые для новой проверки утверждения...
Гедель обнародовал свою теорему в 1931 г. А в 1936 г. Черч доказал теорему о неразрешимости достаточно выразительных теорий. Конечно, результат Черча шире, чем у Геделя, но самый трудный шаг сделал Гедель. К тому же, вопрос о возможности доказать непротиворечивость теории силами самой теории является наиболее принципиальным, о чем было сказано в разделе I "Понятие "недоказуемость" - в быту и математике" этой главы.
Современному человеку, на мой взгляд, трудно смириться с теоремой Геделя в силу того, что господствующая пока в мире идеология Запада требует все предвидеть, и считает возможным все предвидеть. Воспитанному в такой идеологии человеку трудно признать, что какой бы сложной ни была система (человек, например), но всегда может быть создана вторая система, более сложная. И первая система не сможет предсказать поведение 2ой, но, напротив, 2я система сможет предвидеть шаги первой системы и поступать вопреки этим шагам. Но и 2я система не всесильна и тоже может возникнуть превосходящая ее, и опровергающая ее прогнозы 3я система, и т.д.
В достаточно выразительной теории можно сформулировать утверждения, непостижимые для данной теории. Про такие утверждения теория не может сказать, принадлежат они ей (доказуемы в ней), или не принадлежат (не доказуемы). В этом и проявляется способность достаточно выразительной теории выразить принцип расширяемости теории. Вопрос о расширении теории оказывается более сложным, чем сама теория. Теория может быть расширена и в одну сторону, и в прямо противоположную. Но этот вопрос не может быть решен внутри самой теории. Ведь в ответ на любое ее внутреннее "да" всегда найдется внешнее "нет", а в ответ на любое ее внутреннее "нет" всегда найдется внешнее "да".
Я приведу одну свою дискуссию из Интернета на тему непостижимой для заданной системы задачи. Берлиоз и Аннушка в этой дискуссии появились из "Мастера и Маргариты" Булгакова. Берлиоз в споре с Воландом утверждал, что человек может все предвидеть, и считал нелепым предсказание Воланда, что ему (Берлиозу) отрежет голову девушка, комсомолка. Но Аннушка пролила свое масло, Берлиоз упал под трамвай, который вела девушка-комсомолка, и предсказание сбылось.
Заранее поясню, откуда берется равенство Б(АБ*А) = (~Б*(АБ*А)). Алгоритм АБ*А построен так, что он поступает наоборот, чем предсказывает его поведение алгоритм Б*. Результат предсказания Б* в отношении алгоритма АБ*А обозначен как Б*(АБ*А). Алгоритм Б, по условию, правильно предсказывает поведение АБ*А. Результат предсказания Б в отношении алгоритма АБ*А обозначен как Б(АБ*А). Поскольку алгоритм Б предсказывает правильно, а алгоритм Б* предсказывает неправильно, то результат Б* противоположен (значок "~") результату Б. Отсюда и получается искомое равенство.
Гиперссылка, приведенная в дискуссии, уже не работает. Оставляю ее для "истории". По этой ссылке я в свое время разместил сформулированный мной парадокс (по сути, я упростил парадокс из главы 5 "Неразрешимость в контексте диагонализации" книги "Вычислимость и логика" Дж. Булоса и Р. Джеффри.). Этот парадокс и обсуждается ниже. Текст дискуссии - до конца текущего раздела.
[mrhru] 12.04.2002 - 06:31 К Dmitgu: Берлиоз и Аннушка, универсальные алгоритмы...
в
http://www.computerra.ru/online/forums/ctonline/thread43399_43400.html#43400
приводится доказательство того, что не существует универсального алгоритма, "Берлиоз" (Б)
"который по тексту другого (произвольного) алгоритма может всегда точно сказать:
"не зациклится" или "зациклится"".
Доказательство, или опровержение (О), вкратце, следующее:
Пусть алгоритм Б существует. Тогда существует алгоритм "Аннушка" (А), опровергающий Б. Алгоритм А устроен следующим образом:
Внутри А находится алгоритм Б. При запуске А, вызывается Б как подпрограмма, на вход которой подается текст алгоритма А (естественно с включенным текстом алгоритма Б).
Когда внутренний алгоритм Б завершит свою работу, он вернет результат: "зациклится" или "не зациклится" алгоритм А. После получения результата от внутреннего алгоритма Б, алгоритм A выполняет действие, противоположное предсказанному.
Следовательно алгоритм Б работает неправильно, и универсального алгоритма предсказывающего "конечность" произвольного алгоритма не существует.
*****************************************
Мне представляется, что опровержение "Аннушка" неверно. Это не означает, что алгоритм "Берлиоз" существует.
Попробую доказать это.
Без потери общности примем:
1) компьютером, на котором выполняются алгоритмы, является машина Тьюринга
2) все тексты алгоритмов синтаксически правильные, т.е. компьютер никогда не будет "ругаться", и аварийно завершать свою работу. (Кстати в теории машин Тьюринга это и не упоминается)
Рассмотрим алгоритм Б.
Как и любой другой "конечный" алгоритм, в алгоритме Б в конце должна находиться команда стоп. Естественно, как же тогда алгоритм будет "конечным".
Машина Тьюринга может останавливаться и тогда, когда два последних ее состояния идентичны - но часть программы, реализующая такое, фактически и есть команда останова.
Переходим к алгоритму А.
Согласно опровержению О, внутри алгоритма А находится алгоритм Б, после работы которого управление передается в А.
Как мы можем "поместить" алгоритм Б внутрь А?
Первый способ состоит в удалении команды стоп в конце Б. Тогда работа А будет именно такая, как это описано в опровержении О.
Второй способ: оставляем алгоритм Б без изменений, "как есть". Тогда алгоритм А никогда не получит управление после завершения алгоритма Б, так как команда стоп в конце Б остановит работу алгоритма А. Следовательно, алгоритм Аннушка не является опровержением Б
Теперь скажите, разве удаление команды стоп в конце алгоритма Б - это не есть его модификация?
Можем ли мы утверждать, что мы имеем дело по прежнему с универсальным алгоритмом Б?
[Dmitgu] 12.04.2002 - 09:23 Но мы все таки опровергли, утверждение "Нет программы, неподконтрольной Б"?
Мы создали программу А. С включением в нее алгоритма Б - слегка модифицированного (согласен). И мы добились главного - результат работы А противоположен результату исходного (не модифицированного!) Б. Это делает невозможным завершение Б на А с корректным результатом.
А последнее доказывает, что алгоритм Б не универсален в решении проблемы остановки.
Что и требовалось доказать.
[mrhru] 12.04.2002 - 10:00 Счас, попробую сформулировать более точно
(не исключено, что спор из-за терминов)
Давайте обозначать Аннушку А со встроенным алгоритмом Х так: АХА - т.е. управление сначала берет А, затем Х, затем снова А.
В случае с модифицированным алгоритмом Б* - выглядит как АБ*А.
С не модифицированным - АБА.
Что ответит Б, если подать на него А
1) Б(АБА) - 1, т.е. алгоритм АБА остановится из-за остановки Б внутри.
Б(АБ*А) - что-то выдаст, зависящее от А и Б*.
Кстати Б*(Х) - ничего не выдаст - потому что в конце нет команды остановки.
Поэтому я считаю что Б и Б* - это разные алгоритмы. С учетом того смысла, который я вкладываю в используемые понятия. Если вы не согласны с приведенными рассуждениями, значит проблема в разном понимании каких-то терминов.
Хотя я тоже считаю, что Б не может существовать.
[Dmitgu] 12.04.2002 - 17:27 А что такое Б*? Подпрограмма. Нормальная подпрограмма ведь "завершается" передачей управления (и результата)?
И если сравнивать результат обработки текста АБ*А подпрограммой (подфункцией) Б* с результатом такой же обработки программой Б, то по построению АБ*А будет:
Б(АБ*А) = (~Б*(АБ*А))
При этом Б и Б* возвращают одинаковые результаты (первая - как программа, вторая - как подпрограмма) при одних и тех же начальных данных (по построению Б*). Значит верно и:
Б(АБ*А) = Б*(АБ*А)
Из свойства транзитивности равенства и из 2х предыдущих равенств имеем:
Б*(АБ*А) = (~Б*(АБ*А))
В то же время мы сразу положили в основу работу Б (и Б*, следовательно) различимость (не тождественность, не равенство) результата "остановится" от не остановится. То есть:
Б*(АБ*А) <> (~Б*(АБ*А))
А последнее неравенство и означает
~( Б*(АБ*А) = (~Б*(АБ*А)) )
что противоречит (является отрицанием) полученному выше утверждению
Б*(АБ*А) = (~Б*(АБ*А))
Все это имеет место при остановке, конечно. Значит, при остановке возникает ошибка.
Я немного вольно смешивал равенство (применяемого для объектов) и значок отрицания (для истинности-ложности), но вроде идея понятна? Строже надо было бы вводить функцию "инверсии" преобразующую значение "останавливается" в значение "не останавливается" и обратно. Но идея осталась бы той же.
И опять таки, приведенные рассуждения просто более формализованные и подробные, но те же, по сути, что привели вы при изложении парадокса в топике.
[mrhru] 12.04.2002 - 19:09 Ответ: А что такое Б*? Подпрограмма. Нормальная подпрограмма ведь "завершается" передачей управления (и результата)?
Мои возражения, в конечном счете сводится к следующим:
- алгоритм Б нельзя использовать в качестве подпрограммы, т.е. модификация Б меняет алгоритм на другой Б*. Как он работает, что возвращает - уже не имеет никакого значения.
Скорее всего в теории МТ - такие возражения не принимаются, потому что всегда (в теории МТ) можно передавать результат работы одного алгоритма как исходные данные для другого!
(Вот я сам для себя и сформулировал!)
Смущает же меня вот что:
По теории - можно создать программу Аннушка, опровергающую универсальный алгоритм Берлиоз. И с вашими выкладками я полностью согласен!
А на практике - Берлиоз практически всегда сможет обмануть Аннушку - остановив вычислительную среду и не передав управление Аннушке. Т.е. на практике - можно ли создать Берлиоза - неизвестно, но Аннушка его опровергнуть не сможет.
На попытки Аннушки запускать Берлиоза на другой машине или ещё что-нибудь, всегда можно сказать (в лицензионном соглашении :-))) ): "какие либо попытки продолжения работы вычислительной среды после завершения работы Берлиоза - являются нарушением работы алгоритма, и за последствия Берлиоз не отвечает". :-))))))
Т.е. что то вроде - функцию sin(x) вычислить можно, а передать результат в другую функцию уже нет. :-)
Или я опять что-нибудь напутал?
[Dmitgu] 12.04.2002 - 19:40 Но есть правильная страна - Россия,
где в ответ на буржуйские заморочки типа "лицензионное соглашение" всегда можно сказать. "Ах, так вы против Тьюринга!?".
Да и кроме Тьюринга всегда можно найти пару-другую бородатых иностранцев, против кого направлены эти гадкие нам буржуйские происки :-)
[Могучий Пожизненный Шеф] 12.04.2002 - 21:49 Да можно и алгоритмы Маркова использовать, патриотичней будет :)) (-)