Простое доказательство теоремы Геделя

gala05

на пальцах рассказывается основная идея, даже все понятно
написано для программистов
http://arxiv.org/pdf/1409.5944.pdf

shpanenoc

Неплохо. Я вот только не понял домашнее задание №1: почему важен порядок выдачи программы P?

blackout

Ну это просто:

shpanenoc

Ни фига. Ты не прочитал вопрос там. Вопрос такой: можно ли убрать требование, что P генерирует фразы в порядке возрастания их длины, и заменить на более слабое требование, что P генерирует *все* фразы (в каком-то произвольном порядке)?

blackout

Для доказательства достаточно, чтобы P генерировала любую строку за конечное время. В более слабом требовании этого нет.

iri3955

Потому что если не сортировать по длине, то очередной верный результат выдачи P может не оказаться следствием предыдущих, и будет пропущен P' (P его исключит из списка формальных доказателсьтв). Я так понял.

blackout

Нет. Как я понял, P генерит строки из символов алфавита. Каждая такая строка сама по себе это законченный формальный вывод (если повезет).
Программа P' принимает строку и проверяет, является ли она сама по себе 1) грамматически корректной строкой 2) формально верным выводом 3) выводом Sf(x).

blackout

Кстати, как мне кажется, в этом доказательстве пропущена сложность в том месте где утверждается, что высказывание Sf(x) можно сформулировать.

iri3955

> That is, P can mechanically check whether each line is an axiom, or follows from the previous lines by an application of some
deduction rule(s).
Может, я неправильно эту фразу понял? Там может быть опечатка, и данной проверкой занимается P', но сути это не меняет
upd. Да, кажется, там имеется ввиду строки доказательства, а не строки выдачи P. И скорее всего, там P'

blackout

Там может быть опечатка, и данной проверкой занимается P'
Думаю это опечатка и в этом абзаце (3.2 абзац 2) везде вместо P надо читать P'. В конце концов что делает P уже написано в прошлом абзаце. На это также намекает
Therefore, given a statement S, and a string s that might be a
formal derivation of S, program P′ can check (in a purely mechanical way, and in
finite time) whether string s is a formal derivation of statement S in 

но сути это не меняет

Это не меняет сути доказательства. Но меняет суть вопроса 1 из homewrok.

shpanenoc

Кстати, как мне кажется, в этом доказательстве пропущена сложность в том месте где утверждается, что высказывание Sf(x) можно сформулировать.
Вроде как, они там говорят, что rich-enough язык - это тот, который допускает формулирование любого утверждения о целых числах. Sf(x) - это утверждение о целом числе x.

blackout

Sf(x) - это утверждение о целом числе x.
Не только. Это утверждение про целое число x и про функцию \bar{f}. Мне не очевидно как написать конечное определение функции \bar{f}.
Оставить комментарий
Имя или ник:
Комментарий: