Наткнулся пару дней назад на интересную страницу на математическом stackexchange:
Computability viewpoint of Godel/Rosser's incompleteness theorem:
https://math.stackexchange.com/questions/2486348/computability-viewpoint-of-godel-rossers-incompleteness-theorem/2486349#2486349Хорошо известно, что можно доказать теорему о неполноте Гёделя с помощью неразрешимости проблемы остановки, доказанной Тьюрингом (исторически это было в обратном порядке: теорема о неполноте в 1931-м, неразрешимость проблемы остановки в 1940-х).
(напомню, что теорема о неполноте Гёделя говорит о границах наших возможностей строго доказывать математические истины: любая достаточно мощная (и подвергающаяся автоматической проверке) формальная система аксиом арифметики неизбежно неполна, т.е. существует утверждение, которое она не доказывает и не опровергает. Проблема остановки состоит в том, чтобы для любой программы и входных данных определить за конечное время, остановится ли эта программа, если дать ей эти входные данные; эта проблему решить невозможно, что доказывается красивым автореферентным аргументом)
Классическое доказательства Геделя накладывало дополнительное требование на формальную систему (так называемая омега-непротиворечивость); несколько лет спустя Россер нашел трюк, который позволил убрать его, и от системы кроме описанных выше условий требовалось только непротиворечивость. Я не знал, что есть естественный способ перевести трюк Россера на язык вычислимости. Стандартное доказательство Геделя использует предикат доказуемости, а его вычислительная версия использует проблему остановки. Доказательство Россера немного изменяет предикат доказуемости, а его вычислительная версия использует проблему угадывания, в которой требуется, при наличии программы P и входных данных X, угадать, какой ответ выводит P на X, если останавливается, но зато если не останавливается, можно ответить что угодно. Проблема угадывания тоже неразрешима. Это все подробно объясняется по ссылке выше.
Автор страницы полагает (вслед, например, за Скоттом Ааронсоном), что доказательство через вычислимость и проблему остановки является в некотором смысле наиболее естественным док-вом теоремы Геделя, потому что автореферентность, на которой основаны ее доказательства, наиболее естественным образом проявляется в вычислимости. Для того, чтобы доказать свою теорему, Геделю пришлось придумать, как логические утверждения о числах могут говорить "о самих себе", и это было и остается крайне неинтуитивной (и технически нелегкой) частью доказательства. Но когда речь идет о машинах Тьюринга (компьютерах), то факт, что компьютерная программа может в качестве входных данных получить собственный исходный код, и в частности симулировать работу самой себя, не удивляет никакого программиста, знающего, что такое интерпретатор, например.
Не уверен, что я вполне с этим согласен. Попробую немного развернуть эту мысль. В традиционном доказательств теоремы Геделя у нас есть формальная система, которая умеет доказывать утверждения о натуральных числах. Мы вводим "арифметизацию синтаксиса": кодирование числами переменных, логических символов, формул и наконец доказательств - и в результате этого технического процесса мы научили нашу формальную систему доказывать в некотором смысле "утверждения об утверждениях", и отсюда прямая дорога к автоферерентности.
Что происходит в доказательстве через вычислимость? Мы переходим из области логических утверждений в область алгоритмов. Вместо того, чтобы научить утверждения "говорить" об утверждениях, и найти автореферентное противоречие в виде логического утверждения (говорящего о себе), мы идем в обход:
1. учим утверждения говорить об алгоритмах (это та часть, что по ссылке называется "can reason about programs")
2. учим алгоритмы говорить об алгоритмах (это универсальная машина Тьюринга, например)
3. учим алгоритмы говорить об утверждениях (это та часть доказательства, где мы строим программу, перебирающую все возможные формальные доказательства).
Вместо одного обучения у нас три! Почему же это кажется более легким и естественным? Потому что 2 и 3 ин
