Вычислительная полнота влечет неразрешимость
Как я уже говорил, в [1] утверждается, что именно вычислительная полнота Tutorial D делает его неразрешимым. Вот расширенный вариант выдержки, которая приводилась в начале предыдущего раздела:
Проблема попросту состоит в следующем: Если некоторый язык включает логику предикатов и является вычислительно полным, то логическим следствием является то, что в набор синтаксически правильных выражений этого языка будут входить самоссылающиеся выражения, и некоторые из них будут неразрешимыми. Это именно то, что показал Гедель в процессе построения своей первой теоремы о неполноте… Значит, если Tutorial D является вычислительно полным, то набор синтаксически правильных выражений Tutorial D включает самоссылающиеся неразрешимые выражения. Я просто применяю теорему Геделя к Tutorial D.
Автор [1] аппелирует и ко второй теореме Геделя. Вот расширенный вариант выдержки, которая приводилась в аннотации к данной статье:
Придание вычислительной полноты языку Tutorial D является ошибочным решением, поскольку это приводит к созданию языка, логические выражения которого могут быть неразрешимыми, – хотя для любого логического выражения должен существовать алгоритм, позволяющий его вычислить (см. вторую теорему Геделя о неполноте). Имеется ли в Tutorial D пример, более убедительный, чем доказанная теорема? Кодд предусмотрительно избежал этой ловушки, а Третий Манифест – нет!
Я вернусь к вопросу о том, «избежал» ли Кодд «этой ловушки» в следующем разделе. Однако сначала позвольте мне сформулировать две теоремы Геделя. Замечание: В действительности эти теоремы могут формулироваться во многих разных видах; приводимые здесь варианты являются несколько упрощенными – на самом деле, чрезмерно упрощенными, – но в данной ситуации этого достаточно. Заметим также, что в целях данного обсуждения я считаю термины выражение и утверждение взаимозаменяемыми, хотя они обычно не считаются таковыми в контексте традиционных языков программирования.
- Первая теорема Геделя о неполноте: Пусть S – это непротиворечивая формальная система, являющаяся не менее мощной, чем элементарная арифметика; тогда система S является неполной в том смысле, что в S существуют утверждения, которые являются истинными, но это невозможно доказать, оставаясь внутри S.
- Вторая теорема Геделя о неполноте: Пусть – это непротиворечивая формальная система, являющаяся не менее мощной, чем элементарная арифметика; тогда непротиворечивость системы S невозможно доказать, оставаясь внутри S.
Признаюсь, что я не вижу непосредственной связи второй теоремы с аргументами, приводимыми в [1], но очевидно, что первая теорема поддерживает эти аргументы. Более того, поскольку доказательство Геделя своей первой теоремы (a) включает явное построение самоссылающегося утверждения – в сущности, арифметического аналога утверждения «Данное утверждение невозможно доказать в S», а затем доказывает, что это утверждение невозможно доказать в S (и, следовательно, данное утверждение является истинным!), из этого следует, что множество неразрешимых выражений в S включает некоторые самоссылающиеся выражения. И поэтому, если язык Tutorial D вычислительно полон, то он является неразрешимым в том смысле, что в число его выражений входят самоссылающиеся и неразрешимые выражения.
