Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

оригинальное доказательство второй теоремы неполноты

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

Несколько лет назад Харви Фридман придумал новое, очень простое и красивое доказательство второй теоремы о неполноте Геделя. Напомню, что первая теорема о неполноте утверждает, что достаточно мощная формальная система 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.
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.
  • 21 comments