Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Categories:

теорема о неполноте через машины тьюринга

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

В книге Скотта Ааронсона, которую я продолжаю читать, мне понравилось описание хорошего доказательства теоремы Геделя о неполноте с помощью машин Тьюринга. Подробно это доказательство описывалось в блоге Ааронсона пару лет назад, но тогда, я видимо, упустил его или не обратил внимания.

Теорема о неполноте утверждает, как известно, что любая непротиворечивая формальная система аксиом 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. Вот мы и решили проблему "угадай ответ", в точности по ее определению.
Tags: математика
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 7 comments