Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

теорема о неполноте и проблема остановки

Наткнулся пару дней назад на интересную страницу на математическом stackexchange:

Computability viewpoint of Godel/Rosser's incompleteness theorem

Хорошо известно, что можно доказать теорему о неполноте Гёделя с помощью неразрешимости проблемы остановки, доказанной Тьюрингом (исторически это было в обратном порядке: теорема о неполноте в 1931-м, неразрешимость проблемы остановки в 1940-х).

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

Классическое доказательства Геделя накладывало дополнительное требование на формальную систему (так называемая омега-непротиворечивость); несколько лет спустя Россер нашел трюк, который позволил убрать его, и от системы кроме описанных выше условий требовалось только непротиворечивость. Я не знал, что есть естественный способ перевести трюк Россера на язык вычислимости. Стандартное доказательство Геделя использует предикат доказуемости, а его вычислительная версия использует проблему остановки. Доказательство Россера немного изменяет предикат доказуемости, а его вычислительная версия использует проблему угадывания, в которой требуется, при наличии программы P и входных данных X, угадать, какой ответ выводит P на X, если останавливается, но зато если не останавливается, можно ответить что угодно. Проблема угадывания тоже неразрешима. Это все подробно объясняется по ссылке выше.

Автор страницы полагает (вслед, например, за Скоттом Ааронсоном), что доказательство через вычислимость и проблему остановки является в некотором смысле наиболее естественным док-вом теоремы Геделя, потому что автореферентность, на которой основаны ее доказательства, наиболее естественным образом проявляется в вычислимости. Для того, чтобы доказать свою теорему, Геделю пришлось придумать, как логические утверждения о числах могут говорить "о самих себе", и это было и остается крайне неинтуитивной (и технически нелегкой) частью доказательства. Но когда речь идет о машинах Тьюринга (компьютерах), то факт, что компьютерная программа может в качестве входных данных получить собственный исходный код, и в частности симулировать работу самой себя, не удивляет никакого программиста, знающего, что такое интерпретатор, например.

Не уверен, что я вполне с этим согласен. Попробую немного развернуть эту мысль. В традиционном доказательств теоремы Геделя у нас есть формальная система, которая умеет доказывать утверждения о натуральных числах. Мы вводим "арифметизацию синтаксиса": кодирование числами переменных, логических символов, формул и наконец доказательств - и в результате этого технического процесса мы научили нашу формальную систему доказывать в некотором смысле "утверждения об утверждениях", и отсюда прямая дорога к автоферерентности.

Что происходит в доказательстве через вычислимость? Мы переходим из области логических утверждений в область алгоритмов. Вместо того, чтобы научить утверждения "говорить" об утверждениях, и найти автореферентное противоречие в виде логического утверждения (говорящего о себе), мы идем в обход:

1. учим утверждения говорить об алгоритмах (это та часть, что по ссылке называется "can reason about programs")
2. учим алгоритмы говорить об алгоритмах (это универсальная машина Тьюринга, например)
3. учим алгоритмы говорить об утверждениях (это та часть доказательства, где мы строим программу, перебирающую все возможные формальные доказательства).

Вместо одного обучения у нас три! Почему же это кажется более легким и естественным? Потому что 2 и 3 интуитивно верны для людей, знакомых с алгоритмами и интерпретаторами, и хотя формально говоря они требуют технических решений - как именно кодировать программу в виде последовательности символов? как именно кодировать утверждение в виде последовательности символов? - это ощущается (возможно, что справедливо) как мелкие и не очень важные подробности. А главная часть доказательства - автореферентное утверждение - полностью относится к алгоритмам, и там оно выглядит проще и понятнее, чем в применении к утверждениям (диагональная лемма Геделя итп.).

С другой стороны, все же надо отметить, что остается первое обучение - формальную систему надо научить доказывать и опровергать утверждения типа "вот вычисление, показывающее, что данный алгоритм останавливается при таких-то входных данных и дает такой-то результат". По ссылке выше это спрятано под невинно выглядящее название "can reason about programs", но по сути для любой конкретной формальной системы это не тяжелее и не проще, полагаю, чем научить ее арифметизации синтаксиса в первоначальной версии доказательства Геделя. По сути это одно и то же, только вместо "доказательства" мы рассматриваем "вычисление" итд. Так действительно ли это проще, доказывать через алгоритмы? Наверное, нет, если настаивать на полном строгом доказательстве, то то же самое или даже больше работы. Действительно ли это естественнее? Возможно, да - главный аргумент изолирован в области алгоритмов, где он кажется особенно простым и естественным. Но я не знаю, насколько верно, и даже осмысленно, говорить о том, что там его "настоящее место".
Tags: математика, философия
Subscribe

  • нейронные сети имени козьмы пруткова

    В компании OpenAI создали новую модель (нейронную сеть) для распознавания образов, очень крутую, которая в частности сама научилась сопоставлять…

  • череда банальностей

    Понравилось ( из твиттера), метко схвачено: "Kогда понимаешь какую-то важную истину, жутко раздражает, что пробуешь объяснить ее словами и выходит…

  • о фальшивом учителе

    Поучительная история случилась в Австралии. Там обнаружили, что директор школы, а в прошлом много лет учитель, обманывал все четыре школы, в…

  • 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.
  • 50 comments

  • нейронные сети имени козьмы пруткова

    В компании OpenAI создали новую модель (нейронную сеть) для распознавания образов, очень крутую, которая в частности сама научилась сопоставлять…

  • череда банальностей

    Понравилось ( из твиттера), метко схвачено: "Kогда понимаешь какую-то важную истину, жутко раздражает, что пробуешь объяснить ее словами и выходит…

  • о фальшивом учителе

    Поучительная история случилась в Австралии. Там обнаружили, что директор школы, а в прошлом много лет учитель, обманывал все четыре школы, в…