теорема о неполноте через машины тьюринга
Jun. 20th, 2013 03:40 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avva(эта запись может быть интересна тем, кто интересуется логикой и компьютерными науками)
В книге Скотта Ааронсона, которую я продолжаю читать, мне понравилось описание хорошего доказательства теоремы Геделя о неполноте с помощью машин Тьюринга. Подробно это доказательство описывалось в блоге Ааронсона пару лет назад, но тогда, я видимо, упустил его или не обратил внимания.
Теорема о неполноте утверждает, как известно, что любая непротиворечивая формальная система аксиом T, способная выражать утверждения о натуральных числах, и достаточно мощная, чтобы доказать определенные простые арифметические факты, обязательно неполна - есть такие утверждения о натуральных числах, которые она не может доказать, ни опровергнуть.
Один из самых простых подходов к доказательству теоремы о неполноте сводит ее к невозможности решения проблемы остановки машин Тьюринга. Проблема остановки формулируется так: даны машина Тьюринга (т.е. алгоритм, иными словами) и входные данные для нее; определить, остановится она когда-либо, если ее запустить на этих данных, или нет. Довольно простой аргумент показывает, что не существует алгоритма, способного решить проблему остановки.
Предположим, что формальная система T, кроме указанных выше условий, еще и корректна - т.е. она доказывает только истинные утверждения о натуральных числах. Тогда мы можем доказать, что T неполна, с помощью проблемы остановки. Действительно, предположим, что T полна, т.е. любое утверждение она либо доказывает, либо опровергает (доказывает его отрицание). Построим алгоритм решения проблемы остановки следующим образом. Если нам дана машина M и входные данные X, мы можем сформулировать и записать на языке арифметики утверждение P = "машина M рано или поздно остановится, если запустить ее с данными X" (нам для этого нужно придумать способ представлять описание машины M и данных X в виде натуральных чисел, но это легко - и в курсе теории вычислимости, когда изучают машины Тьюринга, и так делается). Будем перебирать все возможные доказательства в системе T, по возрастанию длины, ища доказательство или опровержение P. Согласно предположению о полноте, рано или поздно мы одно из них найдем. Но поскольку T доказывает только истинные факты, то ее доказательство (или опровержение) P означает, что M действительно останавливается (или не останавливается) на X, т.е. наш алгоритм решил проблему остановки.
Это один из самых простых и элегантных способов доказать теорему Геделя о неполноте (особенно для студентов, уже знающих про машины Тьюринга), но у него есть один серьезный недостаток: он требует условия корректности T. Хотя обычные системы аксиом арифметики, как, например, аксиомы Пеано, несомненно корректны, теорема Геделя в общей ее формулировке требует лишь непротиворечивости T, гораздо более слабого условия, и это бывает весьма полезным. Я думал, что в таком подходе к доказательству теоремы Геделя - через машины Тьюринга - это ограничение неизбежно, а запись Ааронсона показывает, что это совсем не так, и что довольно просто перекроить доказательство так, чтобы оно не требовало корректности T. Вот краткое описание этого доказательства.
Мы будем рассматривать машины Тьюринга, которые, останавливаясь, дают результат "да" или "нет" (а также могут никогда не остановиться, конечно). Вместо корректности в доказательстве Ааронсона нам нужны от системы аксиом T лишь непротиворечивость, а также достаточная мощность, чтобы не просто иметь возможность формулировать утверждения о машинах Тьюринга, но и доказывать все истинные утверждения вида "машина M останавливается на входных данных X за Y шагов и говорит да", или "... и говорит нет". Это очень слабое требование, потому что если это утверждение истинно, т.е. это действительно так, она останавливается за Y шагов, то можно выписать последовательные состояния машины после каждого шага, и написать длинное утверждение, которое проверяет, что эта последовательность шагов действительно описывает запуск машины M, действительно останавливается в конце, действительно говорит да. Все это будут простые арифметические отношения между конкретными числами (кодами машин и состояний), поэтому достаточно мощная система T - такой мощи, какая обычно требуется для теоремы о неполноте в любом случае - сможет их доказать.
Из этого условия также следует, что T доказывает любое истинное утверждение вида "M останавливается на X и говорит да/нет", потому что если оно истинно, то есть какое-то число шагов Y, за которые она останавливается, и T доказывает утверждение про конкретное число шагов Y, а более общее сразу из него следует. Если P - истинное утверждение такого вида, то T доказывает P, и следовательно не может доказать не-P, потому что T непротиворечива (но заметим, что хотя не-P - пример ложного утверждения, которое T не доказывает, у нас нет общего ограничения корректности: T может доказывать всякие другие ложные утверждения других видов).
Теперь сформулируем проблему "угадай ответ", похожую на проблему остановки. Это следующая задача: пусть нам дают описание машины M, и входных данных X. Мы обязуемся всегда остановиться за конечное время, и если M на X отвечает да, то мы обязуемся ответить да; если М на X отвечает нет, то мы обязуемся ответить нет; а если M на X не останавливается, мы можем сказать хоть да, хоть нет (но остановиться и что-то сказать обязаны!).
Хотя эта проблема кажется менее полезной, чем проблема остановки, легко видеть, что она тоже не поддается решению; доказательство очень похоже на доказательство неразрешимости проблемы остановки, см. подробности в записи Ааронсона.
Осталось описать, как с помощью формальной системы T, если она полна, решить проблему "угадай ответ". Нам дают M и X; мы перебираем все возможные доказательства в T, ища доказательство или опровержение утверждения P = "М останавливается на X и говорит да". Если находит доказательство, отвечает "да", если опровержение, "нет". Поскольку T полна, либо доказательство, либо опровержение мы найдем, так что наш алгоритм всегда остановится. Если M на самом деле останавливается на X и говорит да, то T доказывает это истинное утверждение, согласно нашему условию, и не может его опровергать (ввиду непротиворечивости), поэтому мы остановимся и скажем "да". Если M на самом деле останавливается на X и говорит нет, то утверждение "М останаливается на X и говорит да" ложно, и T не может доказать ложное утверждение такого вида, поэтому наш алгоритм неизбежно ответит "нет". Ну а если M не останавливается, то я не знаю, что мы ответим, но мне неважно, главное, что сами точно остановимся из-за полноты T. Вот мы и решили проблему "угадай ответ", в точности по ее определению.
В книге Скотта Ааронсона, которую я продолжаю читать, мне понравилось описание хорошего доказательства теоремы Геделя о неполноте с помощью машин Тьюринга. Подробно это доказательство описывалось в блоге Ааронсона пару лет назад, но тогда, я видимо, упустил его или не обратил внимания.
Теорема о неполноте утверждает, как известно, что любая непротиворечивая формальная система аксиом T, способная выражать утверждения о натуральных числах, и достаточно мощная, чтобы доказать определенные простые арифметические факты, обязательно неполна - есть такие утверждения о натуральных числах, которые она не может доказать, ни опровергнуть.
Один из самых простых подходов к доказательству теоремы о неполноте сводит ее к невозможности решения проблемы остановки машин Тьюринга. Проблема остановки формулируется так: даны машина Тьюринга (т.е. алгоритм, иными словами) и входные данные для нее; определить, остановится она когда-либо, если ее запустить на этих данных, или нет. Довольно простой аргумент показывает, что не существует алгоритма, способного решить проблему остановки.
Предположим, что формальная система T, кроме указанных выше условий, еще и корректна - т.е. она доказывает только истинные утверждения о натуральных числах. Тогда мы можем доказать, что T неполна, с помощью проблемы остановки. Действительно, предположим, что T полна, т.е. любое утверждение она либо доказывает, либо опровергает (доказывает его отрицание). Построим алгоритм решения проблемы остановки следующим образом. Если нам дана машина M и входные данные X, мы можем сформулировать и записать на языке арифметики утверждение P = "машина M рано или поздно остановится, если запустить ее с данными X" (нам для этого нужно придумать способ представлять описание машины M и данных X в виде натуральных чисел, но это легко - и в курсе теории вычислимости, когда изучают машины Тьюринга, и так делается). Будем перебирать все возможные доказательства в системе T, по возрастанию длины, ища доказательство или опровержение P. Согласно предположению о полноте, рано или поздно мы одно из них найдем. Но поскольку T доказывает только истинные факты, то ее доказательство (или опровержение) P означает, что M действительно останавливается (или не останавливается) на X, т.е. наш алгоритм решил проблему остановки.
Это один из самых простых и элегантных способов доказать теорему Геделя о неполноте (особенно для студентов, уже знающих про машины Тьюринга), но у него есть один серьезный недостаток: он требует условия корректности T. Хотя обычные системы аксиом арифметики, как, например, аксиомы Пеано, несомненно корректны, теорема Геделя в общей ее формулировке требует лишь непротиворечивости T, гораздо более слабого условия, и это бывает весьма полезным. Я думал, что в таком подходе к доказательству теоремы Геделя - через машины Тьюринга - это ограничение неизбежно, а запись Ааронсона показывает, что это совсем не так, и что довольно просто перекроить доказательство так, чтобы оно не требовало корректности T. Вот краткое описание этого доказательства.
Мы будем рассматривать машины Тьюринга, которые, останавливаясь, дают результат "да" или "нет" (а также могут никогда не остановиться, конечно). Вместо корректности в доказательстве Ааронсона нам нужны от системы аксиом T лишь непротиворечивость, а также достаточная мощность, чтобы не просто иметь возможность формулировать утверждения о машинах Тьюринга, но и доказывать все истинные утверждения вида "машина M останавливается на входных данных X за Y шагов и говорит да", или "... и говорит нет". Это очень слабое требование, потому что если это утверждение истинно, т.е. это действительно так, она останавливается за Y шагов, то можно выписать последовательные состояния машины после каждого шага, и написать длинное утверждение, которое проверяет, что эта последовательность шагов действительно описывает запуск машины M, действительно останавливается в конце, действительно говорит да. Все это будут простые арифметические отношения между конкретными числами (кодами машин и состояний), поэтому достаточно мощная система T - такой мощи, какая обычно требуется для теоремы о неполноте в любом случае - сможет их доказать.
Из этого условия также следует, что T доказывает любое истинное утверждение вида "M останавливается на X и говорит да/нет", потому что если оно истинно, то есть какое-то число шагов Y, за которые она останавливается, и T доказывает утверждение про конкретное число шагов Y, а более общее сразу из него следует. Если P - истинное утверждение такого вида, то T доказывает P, и следовательно не может доказать не-P, потому что T непротиворечива (но заметим, что хотя не-P - пример ложного утверждения, которое T не доказывает, у нас нет общего ограничения корректности: T может доказывать всякие другие ложные утверждения других видов).
Теперь сформулируем проблему "угадай ответ", похожую на проблему остановки. Это следующая задача: пусть нам дают описание машины M, и входных данных X. Мы обязуемся всегда остановиться за конечное время, и если M на X отвечает да, то мы обязуемся ответить да; если М на X отвечает нет, то мы обязуемся ответить нет; а если M на X не останавливается, мы можем сказать хоть да, хоть нет (но остановиться и что-то сказать обязаны!).
Хотя эта проблема кажется менее полезной, чем проблема остановки, легко видеть, что она тоже не поддается решению; доказательство очень похоже на доказательство неразрешимости проблемы остановки, см. подробности в записи Ааронсона.
Осталось описать, как с помощью формальной системы T, если она полна, решить проблему "угадай ответ". Нам дают M и X; мы перебираем все возможные доказательства в T, ища доказательство или опровержение утверждения P = "М останавливается на X и говорит да". Если находит доказательство, отвечает "да", если опровержение, "нет". Поскольку T полна, либо доказательство, либо опровержение мы найдем, так что наш алгоритм всегда остановится. Если M на самом деле останавливается на X и говорит да, то T доказывает это истинное утверждение, согласно нашему условию, и не может его опровергать (ввиду непротиворечивости), поэтому мы остановимся и скажем "да". Если M на самом деле останавливается на X и говорит нет, то утверждение "М останаливается на X и говорит да" ложно, и T не может доказать ложное утверждение такого вида, поэтому наш алгоритм неизбежно ответит "нет". Ну а если M не останавливается, то я не знаю, что мы ответим, но мне неважно, главное, что сами точно остановимся из-за полноты T. Вот мы и решили проблему "угадай ответ", в точности по ее определению.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-06-20 01:55 am (UTC)Есть ряд очень тонких моментов, таких как "не корректность, а сигма_1-корректность" и "не омега-противоречивость, а 1-противоречивость".
В этом многие путаются.
Несмотря на все эти "не-чисто-синтаксические" доказательства, доказательство Геделя вроде бы единственное, которое полностью выразимо в арифметике (иными словами, эквивалентность геделевского утверждения и непротиворечивости арифметики есть теорема арифметики) и поэтому из него как следствие (хотя не тривиальное, как его излагают популярные источники) получается Вторая Теорема Геделя.
И оригинальная первая теорема Геделя таки требует омега-непротиворечивость (из которой следует сигма_1-корректность в семантическом мире). Популяризация Россеровского ослабления привела к тому, что люди путаются в необходимых условиях для Второй Теоремы - считают, что они тоже автоматически ослаблены. Это не так.
Вот, просто решил предостеречь читателей, чтоб не расслаблялись :)
no subject
Date: 2013-06-20 03:13 am (UTC)Есть два фундаментально разных подхода к док-ву теоремы о неполноте:
1. Доказываем для определенного удобного множества X, связанного с доказуемостью в T, что оно представимо в нашей системе, т.е. есть phi(x) так что T|-phi(x) <--> x in X. Далее мы используем диагональную лемму и строим эксплицитное геделево утверждение для T, которое демонстрирует его неполноту.
В доказательстве Геделя X - множество номеров доказуемых в T утверждений, и омега-непротиворечивость нужна, чтобы доказать его представимость. В доказательстве Россера X более сложная штука, это множество, "разделяющее" множество доказуемых и множество опровержимых в T утверждений: оно включает в себя первое, но не пересекается со вторым. "Утверждение Россера" помогает построить X, и простой непротиворечивости оказывается достаточно, чтобы доказать его представимость.
Если известно, что T корректна, то можно срезать несколько углов, вместо "слабо представимо" используя "определимо в языке" (definable); тогда доказательство семантическое и пользуется истинностью геделева утверждения.
2. Нам дают в руки уже готовое перечислимое (r.e.), но не разрешимое (recursive) множество X, представимое в T. Это решает вопрос, потому что если бы T была полной, то любое представимое в ней множество должно быть разрешимым. Мы не строим тут никакого утверждения, ни по Геделю, ни по Россеру; за нас в некотором смысле кто-то это уже сделал, доказав неразрешимость множества X (видимо, пользуясь диагональностью и вытекающим из нее парадоксом в том или ином виде).
Именно так выглядят простые док-ва через машины Тьюринга: множество X тут, например, "все такие пары (M,X), что М останавливается на входных X". Неразрешимость проблемы остановки означает, что X неразрешимое множество. Нам еще нужно доказать, что X представимо в T, причем разрешается предположить, что T полна. Это совсем легко сделать, если T корректна: ввиду полноты T либо докажет, либо опровергнет "М останавливается на Х", ввиду корректности она даст правильный ответ. Сигма_1-корректности тут, кажется, недостаточно: нам нужно знать, что если М останавливается, T не может взять да и доказать неверное пи_1 утверждение "М не останавливается".
Ааронсон показывает, что корректность не нужна, достаточно непротиворечивости и умения доказать все истинные сигма_1-утверждения (это легко). Для этого он выбирает другое неразрешимое множество X, для которого оба интересующих нас исхода (останавливается и говорит да/нет) оказываются сигма_1-утверждениями, и этого хватает. Но это не значит, по-моему, что X воплощает в каком-то смысле "трюк Россера" или является аналогом док-ва Россера, перенесенным на машины Тьюринга.
no subject
Date: 2013-06-20 04:09 am (UTC)Сигма_1-корректность это семантический эквивалент так называемой 1-consistency (omega-consistency для разрешимых формул).
Кажется, это достаточное условие для Первой (в оригинальной формулировке) и Второй теорем Геделя. Или нет?
no subject
Date: 2013-06-20 07:19 am (UTC)Ой, как мне это не нравится. Истинность, по-моему, гораздо более хитрая и сложная вещь, чем доказуемость. То есть, сразу нужно кучу всего оговаривать.
no subject
Date: 2013-06-20 12:40 pm (UTC)no subject
Date: 2013-06-20 12:44 pm (UTC)> т.е. она доказывает только истинные утверждения о натуральных числах
При работе с формальными системами есть понятие выводимости утверждений, и оно является базовым, но что такое истинность, требует отдельного пояснения. Насколько я понимаю, если мы работаем в рамках одной формальной системы, то истинность совпадает с выводимостью, а если мы, изучая одну ФС X, апеллируем к другой «каноничной» ФС Y, то можно утверждения, выразимые в обеих системах, называть истинными, если они выводятся в Y. При этом Y обычно не называется, а подразумевается.
no subject
Date: 2013-06-20 04:32 pm (UTC)Народ чего-то не любит точно формулировать теорему. Гёдель, насколько я в курсе, интересовался логическими теориями, т.е. множествами предложений Исчисления предикатов. Соответственно, и теорема формулировалась для них, и там есть важное условие алгоритмической перечислимости множества аксиом.
Дело в том, что любое непротиворечивое множество предложений, например, множество аксиом арифметики Пеано, всегда можно расширить до полного непротиворечивого множества предложений. В результате мы получим контрпример к теореме Гёделя, если не упомянем про перечислимость аксиом. Между тем непонятно, почему бы этому контрпримеру не подходить под понятие "формальной системы".