Точка зрения вычислимости теоремы Гёделя/Россера о неполноте

Здесь я представлю очень простые основанные на вычислимости доказательства теоремы Гёделя/Россера о неполноте, которые требуют лишь базовых знаний о программах. Я чувствую, что эти доказательства малоизвестны, несмотря на то, что они дают очень общую форму теорем о неполноте, а также их легко сделать строгими, даже не полагаясь на большие базовые знания в логике. Типичные доказательства используют что-то вроде леммы о фиксированной точке, которая, по сути, представляет собой комбинатор фиксированной точки, «примененный» к доказуемости, но его гораздо сложнее понять и доказать строго, чем неразрешимость проблемы остановки. Достаточно сказать, что все доказательства так или иначе используют диагонализацию.

Возьмите любой практический язык программирования L, на котором программы могут выполнять основные операции со строковыми/целочисленными переменными и условными переходами (или циклами while). С этого момента все программы , на которые мы будем ссылаться, являются программами на языке L. Для удобства мы также будем считать каждую строку программой. Если это обычно недопустимая программа, мы будем считать, что она представляет собой программу, которая просто выполняет бесконечный цикл. (Любой интерпретатор L может быть легко модифицирован для реализации этого.)

Сначала я покажу, как неразрешимость проблемы остановки по существу влечет за собой (первую) теорему Гёделя о неполноте.

Проблема с остановкой

Определим проблему остановки следующим образом:
  Для данной программы P и входных данных X:
    если P останавливается на X, то ответ «верный».
    Если P не останавливается на X, то ответ «ложь».

Нетрудно доказать, что не существует программы, решающей проблему остановки. Чтобы программа могла решить проблему остановки, она должна останавливаться при каждом вводе (P, X), а также должна выводить правильный ответ, как указано в задаче. Если вы еще не знаете доказательства, попробуйте, прежде чем смотреть на доказательство ниже!

Для любой программы H:
  пусть C будет программой, которая выполняет следующие действия на входе P:
    если H(P,P) = "false", то выводит "ха-ха" (и останавливается), в противном случае - бесконечный цикл (без остановки).
  Если H решает проблему остановки:
    H(C,C) останавливается и, следовательно, C(C) останавливается тогда и только тогда, когда H(C,C) = «ложь» по определению C.
    Противоречие с определением H.
  Таким образом, H не решает проблема остановки.

Ключевые определения формальных систем

Возьмем любую формальную систему T. Мы говорим, что V является верификатором доказательств для T тогда и только тогда, когда выполняются все следующие условия:
  V является программой.
  Для любого предложения φ над T и доказательства x:
    V(φ,x) решает (останавливается и отвечает), является ли x доказательством φ.
Мы говорим, что T может рассуждать о программах тогда и только тогда, когда:
  Для каждой программы P, которая останавливается на входе X и выдает Y:
    T может доказать следующее для любой строки Z, отличной от Y:
      «Программа P останавливается на входе X».
      «Программа P останавливается на входе X и выводит Y».
      «Неверно, что программа P останавливается на входе X и выдает Z».
      (Здесь P,X,Y,Z вставлены как закодированные строки, но вы должны уловить идею.)
Мы говорим, что T непротиворечиво , если и только если:
  не существует предложения φ о программах, такого, что T доказывает как φ, так и его отрицание.
Мы говорим, что T является полным тогда и только тогда, когда:
  Для каждого предложения φ о программах мы имеем, что T доказывает либо φ, либо его отрицание.
Мы говорим, что Т правильно для остановки программы, если и только если:
  Если Т доказывает, что программа останавливается на входе, то она действительно останавливается.

Теорема Геделя о неполноте через проблему остановки

Возьмем любую формальную систему T с верификатором доказательств V, которая может рассуждать о программах.
Пусть H будет следующей программой на входе (P,X):
  Для каждой строки s в лексикографическом порядке длины:
    Если V("Программа P останавливается на входе X." , s ), то выведите "true".
    Если V ("Программа P не останавливается на входе X." , s ), то выведите "false".
Если T является полным, непротиворечивым и обоснованным для остановки программы:
  Для любой программы P и входных данных X:
    T доказывает ровно одно из следующих предложений:
      A = «Программа P останавливается на входных данных X».
      B = «Программа P не останавливается на входе X».
    Таким образом, H останавливается на входе (P,X), потому что s в конечном итоге будет доказательством A или B.

      T может доказать A, так как T может рассуждать о программах, и, следовательно, H(P,X) = «истинно».
    Если P не останавливается на X:
      T не доказывает A по обоснованности остановки программы.
      Таким образом, T доказывает B, и, следовательно, H (P, X) = «ложно».
    Следовательно, H(P,X) является правильным ответом на вопрос, останавливается ли P на X.
  Следовательно, H решает проблему остановки.
  Противоречие с неразрешимостью проблемы остановки.
Следовательно, T либо неполный, либо непоследовательный, либо непригодный для остановки программы.

Усиление Россером теоремы Гёделя о неполноте

После того, как теорема Геделя была опубликована, Россер придумал трюк, чтобы усилить ее, и я наткнулся на запись в блоге Скотта Ааронсона, которая показывает, что если мы используем что-то, называемое проблемой угадывания нуля, вместо проблемы остановки, мы можем получить то самое укрепление! В частности, мы можем затем отказаться от условия надежности для остановки программы. Я приведу упрощенную автономную версию проблемы угадывания нуля и доказательство теоремы Россера о неполноте, в точности аналогично тому, как неразрешимость проблемы остановки влечет за собой теорему Гёделя о неполноте. Если вам нужна задача, вы можете сначала прочитать определение задачи с угадыванием нуля, а затем попытаться найти доказательство самостоятельно, следуя идеям предыдущего доказательства.

Проблема с нулевым угадыванием

Определим задачу угадывания нуля следующим образом:
  Для данной программы P и входных данных X:
    если P останавливается на X, то ответ равен 0, если P(X) = 0, и равен 1 в противном случае.
    (Если P не останавливается на X, то подходит любой ответ.)

Чтобы программа могла решить задачу угадывания нуля, она должна останавливаться на каждом входе (P, X), а также должна выводить правильный ответ, как указано в задаче. Это означает, что решателю разрешено выводить произвольную ерунду, если P не останавливается на X. Как и проблема остановки, проблема угадывания нуля не может быть решена программой. Попробуйте доказать это, прежде чем смотреть на доказательство ниже!

Для любой программы G:
  пусть D будет программой, которая выполняет следующие действия на входе P:
    если G(P,P) = 0, то выводит 1, иначе выводит 0.
  Если G решает задачу угадывания нуля:
    G(D,D) останавливается , и, следовательно, D (D) ≠ 0 тогда и только тогда, когда G (D, D) = 0, по определению D.
    Противоречие с определением G.
  Следовательно, G не решает проблему угадывания нуля.

Обратите внимание, что выбор 0 и 1 действительно произволен. Вы можете предположить, что 0 и 1 обозначают любые фиксированные отдельные строки, которые вам нравятся.

Теорема Россера о неполноте через задачу угадывания нуля

Возьмем любую формальную систему T с верификатором доказательств V, которая может рассуждать о программах.
Пусть G будет следующей программой на входе (P,X): Для каждой строки     s
  в лексикографическом порядке длины     : «Неверно, что программа P останавливается на вводе X и выводит 0». , s ), то выведите 1. Если T является полным и непротиворечивым:   Для любой программы P и ввода X:     T доказывает ровно одно из следующих предложений:       A = "Программа P останавливается на входе X и выводит 0."       B = «Неверно, что программа P останавливается на входе X и на выходе 0».     Таким образом, G останавливается на входе (P,X), потому что s в конечном итоге будет доказательством A или B.








    Если P останавливается на X:
      Вспомните, что T может доказать правильный вывод P на X.
      Если P(X) = 0, то T может доказать A и, следовательно, G(P,X) = 0.
      Если P(X) ≠ 0 , то T может доказать B и, следовательно, G(P,X) = 1.
  Следовательно, G решает проблему угадывания нуля.
  Противоречие с неразрешимостью задачи нулевого угадывания.
Следовательно, T либо неполно, либо несовместно.

Явно независимое предложение

В приведенных выше доказательствах мы использовали неразрешимость некоторой проблемы вычислимости в качестве черного ящика, чтобы показать, что T неполно. В обоих случаях мы можем фактически объединить доказательство неразрешимости с доказательством неполноты, чтобы получить явные предложения, независимые над T, а это означает, что T не может доказать ни его, ни его отрицание.

Пусть H — программа, построенная при доказательстве теоремы Гёделя о неполноте.
Пусть C — программа, построенная для доказательства того, что H не решает проблему остановки.
Пусть Q = «Программа C останавливается на входе C.».
Пусть Q' будет отрицанием Q.
Если T непротиворечиво и правильно для остановки программы:
  Если C(C) останавливается:
    T доказывает Q, но не Q', поскольку T может рассуждать о программах.
    Таким образом, H (C, C) = «истинно», и, следовательно, C (C) не останавливается.
    Противоречие.
  Поэтому C(C) не останавливается.
  Таким образом, T не доказывает Q, так как T подходит для остановки программы.
  Если T доказывает Q':
    H(C,C) = «ложь», и, следовательно, C(C) останавливается.
    Противоречие, как указано выше.

  Таким образом, T не доказывает ни Q, ни Q', но Q' действительно истинно.

Пусть G — программа, построенная при доказательстве теоремы Россера о неполноте.
Пусть D — программа, построенная для доказательства того, что G не решает задачу угадывания нуля.
Пусть W = «Программа D останавливается на входе D и выводит 0».
Пусть W' будет отрицанием W.
Если T непротиворечиво:
  Если D(D) останавливается:
    Вспомните, что T может рассуждать о программах.
    Таким образом, T доказывает W, если D(D) = 0, и T доказывает W', если D(D) = 1.
    Таким образом, G(D,D) = D(D) по определению G.
    Но D(D) ≠ G( D,D), по определению D.
    Противоречие.
  Поэтому D(D) не останавливается.
  Если T доказывает W или W':
    G(D,D) останавливается, и, следовательно, D(D) останавливается.
    Противоречие, как указано выше.
  Следовательно, Т не доказывает ни W, ни W', но W' действительно истинно.

С точки зрения вычислимости, хотя T является полным для остановки программы (поскольку он может рассуждать о программах), он неполный для программы без остановки (какая-то программа на некотором входе не остановится, и T не может доказать этот факт).

Нулевое угадывание против остановки

Обратите внимание, что мы избегаем необходимости в том, чтобы T была правильной для остановки программы в приведенных выше доказательствах, основанных на проблеме угадывания нуля, потому что она имеет более слабое требование, чем проблема остановки в случае, когда данная программа P не останавливается на заданном входе. ИКС.

Надежность против постоянства

Принято считать, что T является классическим (для программ), что означает, что T может использовать правила классической логики при выводе предложений о программах. Но приведенные выше доказательства не предполагают, что T является классическим. Обратите внимание, что если T является классическим (или, по крайней мере, имеет принцип взрыва), то корректность T для любого предложения будет подразумевать непротиворечивость T, потому что, если T несовместимо, то T доказывает каждое предложение о программах. Кроме того, если T является классическим, то его надежность для остановки программы сильнее, чем его непротиворечивость, потому что возможно (что мы докажем в следующем абзаце), что T доказывает предложение формы «Программа P останавливается на входе X». и все же P на самом деле не останавливается на входе X в действительности. Заметим также, что для классического Т надежность Т для программы без остановок эквивалентна просто непротиворечивости Т, потому что если программа Р действительно останавливается на вводе X в реальности, то Т может доказать этот факт, и поэтому, если Т доказывает, что программа P не останавливается на входе X». то T также несовместно.

Другой факт для классического T состоит в том, что T непротиворечиво тогда и только тогда, когда Q истинно. Мы уже показали, что если T непротиворечиво, то Q' истинно. Если T противоречиво и классически, то по принципу взрыва T доказывает и Q, и Q', и, таким образом, H(C,C) останавливается, а значит, C(C) не останавливается. Аналогично, если T классический, то T непротиворечив тогда и только тогда, когда D(D) не останавливается.

Чтобы продемонстрировать утверждение из первого абзаца, нам нужно построить формальную систему, которая была бы классической и непротиворечивой, но все же непригодной для остановки программы. Для этого пусть S — формальная система, которая может выполнять просто классические рассуждения о конечных двоичных строках и, следовательно, может рассуждать о программах, поскольку она может рассуждать о выполнении любой программы за любое конечное число шагов. (В следующем разделе мы объясним, как S может это сделать. Конечно, нам нужно перевести предложения о программах в предложения о конечных двоичных строках, но существует естественный вычислимый перевод.) Мы считаем, что S непротиворечива и корректна для конечных двоичных последовательностей. строк, и, следовательно, также подходит для остановки программы. Мы уже видели, что S не доказывает ни Q, ни Q', но Q на самом деле ложно. Пусть теперь S' будет S+Q, а именно, что S' — это формальная система, которая доказывает каждую теорему, которая может быть выведена классическим образом из аксиом S плюс Q. Тогда S' является классической и имеет верификатор доказательства (упражнение для вас) и не годится для остановки программы. Но S' непротиворечиво, потому что в противном случае имеется доказательство противоречия над S+Q, которое может быть преобразовано в доказательство Q' над S. Это последнее утверждение является примеромтеорема дедукции , которая очевидна для естественной дедукции в стиле Fitch .

Исходная теорема Геделя требовала, чтобы T была ω-непротиворечивой , но его доказательство на самом деле требует только, чтобы T была Σ1-правильной . С помощью трюка Геделя, называемого β-леммой, Σ1-корректность по существу эквивалентна корректности остановки программы. Таким образом, в этом точном смысле можно сказать, что более слабая теорема по существу эквивалентна теореме, показанной в оригинальном доказательстве Гёделя. На самом деле правильность остановки программы всегда считается само собой разумеющейся для любой формальной системы, которую мы используем на практике, поскольку мы действительно хотим, чтобы она не доказывала ложных предложений о программах. Но более сильная теорема прекрасна с точки зрения современной CS, поскольку она выявляет серьезные фундаментальные ограничения в любой непротиворечивой формальной системе, которая может рассуждать о конечном выполнении программы, что является очень конкретным понятием в реальном мире!

Кодирование выполнения программы в строке

В этом разделе мы объясним, как выполнение программы может быть выражено в одной конечной двоичной строке, чтобы мы могли использовать предложения над этими строками для описания поведения программы, включая остановку. Во-первых, заметьте, что двоичный код не является серьезным ограничением, и есть много способов обойти его. Самый простой способ — использовать унарные числа (k кодируется как строка из k единиц), разделенные нулями, для представления конечных строк натуральных чисел! Это представление дает однозначное соответствие между конечной двоичной строкой и естественной строкой. Далее обратите внимание, что мы можем представить конечные последовательности натуральных строк, используя одну естественную строку, добавляя единицу к каждому элементу и используя нули в качестве разделителей. Например, последовательность ((3,1,4),(1),(),(5,9)) будет представлена ​​как (4,2,5,0,2,0,0,6,10). Теперь любую программу можно легко представить в виде естественной строки. Кроме того, все состояние любой заданной программы, выполняющейся на данном входе, может быть зафиксировано с помощью пары натуральных строк, представляющих программу и ввод с выделенным «текущим шагом», плюс последовательность пар натуральных строк, где каждая пара (x ,v) означает, что переменная x имеет значение v. Таким образом, все состояние выполнения программы может быть представлено одной естественной строкой. Если язык L достаточно прост, вы должны быть в состоянии представить, как выразить классическим предложением о строках s,t, что s→t является действительным переходом состояния программы, что означает, что после одного шага из состояния s программа будет находиться в состоянии t. . Поскольку конечная последовательность состояний программы может быть представлена ​​в виде одной естественной строки, мы можем выразить классическим предложением о строках p, x, y, что программа p на входе x остановится и выдаст y, что в основном является предложением (Существует конечная последовательность состояний программы, начиная с программы p, имеющей вход x, в которой каждая пара смежных состояний в этой последовательности является допустимым переходом состояния, и заканчивая выходом y. ). Наконец, обратите внимание, что если программа p действительно останавливается на входе x, то любая формальная система S, которая может рассуждать о натуральных цепочках, может доказать каждый шаг выполнения p на x, а затем связать все эти доказательства вместе, чтобы доказать факт остановки. .

В последней части предыдущего абзаца мы слегка апеллировали к нашей интуиции, что мы можем сделать соответствующий перевод этого предложения, используя любой мыслимый практический язык программирования. Полностью формализовать это не совсем понятно, но это можно сделать разными способами. Один из способов — сделать это только для какой-то конкретной универсальной разновидности машин Тьюринга. Другой - сделать это только для какого-то конкретного языка, подобного ассемблеру. Третий — сделать это для некоторого варианта лямбда-исчисления. Что бы это ни было, оно должно быть эквивалентно машинам Тьюринга. Этот вопрос не является специфическим для этой версии теоремы о неполноте, поскольку исходная теорема касается систем, которые могут рассуждать об основных арифметических действиях, которые оказываются эквивалентными благодаря β-лемме Гёделя. Причина Гёделя Эта теорема касалась арифметики, кажется, потому, что математики того времени считали ее фундаментальной для математики. Основные преимущества доказательства моей версии теоремы заключаются в том, что она позволяет избежать теории чисел в β-лемме Гёделя и концепции примитивной рекурсии, а также показывает, что для доказательства достаточно лишь базовых фактов конкатенации строк (даже не какой-либо формы индукции). явление неполноты, и не требует, чтобы формальная система основывалась на классической логике.

Популярные заблуждения о незавершенности

Когда люди впервые сталкиваются с утверждением о неполноте арифметики Пеано (ПА), многие ошибочно подозревают различные аспекты ПА в качестве «причины».

Это не связано с индукцией и даже не с бесконечным числом аксиом ПА. Причина в том, что PA- достаточно, а PA- имеет конечное число аксиом. PA- плюс индукция дает PA. Точно так же описанная здесь Теория конкатенации (TC) , которая является простым кандидатом для формальной системы S выше, которая может просто рассуждать о конечных двоичных строках, имеет только конечное число аксиом.

Это не связано с каким-либо глубоким теоретико-числовым явлением. Я сам ошибочно думал, что это так, потому что арифметика Пресбургера непротиворечива и полна, пока я не увидел вышеприведенное доказательство, основанное на вычислимости, которое применимо к TC, поскольку TC может рассуждать о программах. Это правда, что TC в некотором смысле эквивалентен PA-, но в TC нет ничего, кроме конкатенации, а аксиомы TC — это всего лишь несколько «очевидных» фактов о цепочках.

Это не связано с классической логикой. Это обычная «критика» теорем о неполноте, но она совершенно необоснованна. Как показано в приведенном выше доказательстве, оно применимо к любой формальной системе, которая имеет верификатор доказательств и может рассуждать о программах, независимо от того, классическая она или нет. Заметьте, я нигде ничего не говорил о синтаксических или дедуктивных правилах, потому что их не должно быть. Формальная система T может быть даже настолько сумасшедшей, что если нам дана произвольная программа, которая останавливается на каком-то входе, то самым простым способом найти доказательство этого факта φ над T будет запуск V(φ,x) для каждой возможной строки x пока не найдете тот, который, по словам Ви, действителен! В качестве тривиального, но релевантного примера рассмотрим формальную систему R (для «бегуна»), чей верификатор доказательств выполняет следующие заданные входные данные (φ, k): сначала он проверяет, имеет ли φ форму « (где фразы в квадратных скобках необязательны), а затем запускает P на X в течение length(k) шагов, а затем отвечает, что доказательство верно, если P остановилось [и его вывод соответствует заявленному], и отвечает, что доказательство во всех остальных случаях недействителен. Вы можете видеть, что R действительно останавливается на каждом входе (φ,k) и подтверждает правильность так называемого доказательства только тогда, когда φ действительно верно и k достаточно длинное. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером. (где фразы в квадратных скобках необязательны), а затем запускает P на X в течение length(k) шагов, а затем отвечает, что доказательство верно, если P остановилось [и его вывод соответствует заявленному], и отвечает, что доказательство во всех остальных случаях недействителен. Вы можете видеть, что R действительно останавливается на каждом входе (φ,k) и подтверждает правильность так называемого доказательства только тогда, когда φ действительно верно и k достаточно длинное. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером. а затем отвечает, что доказательство верно, если P остановился [и его вывод соответствует заявленному], и отвечает, что доказательство неверно во всех остальных случаях. Вы можете видеть, что R действительно останавливается на каждом входе (φ,k) и подтверждает правильность так называемого доказательства только тогда, когда φ действительно верно и k достаточно длинное. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером. а затем отвечает, что доказательство верно, если P остановился [и его вывод соответствует заявленному], и отвечает, что доказательство неверно во всех остальных случаях. Вы можете видеть, что R действительно останавливается на каждом входе (φ,k) и подтверждает правильность так называемого доказательства только тогда, когда φ действительно верно и k достаточно длинное. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером. Вы также можете видеть, что R не подтверждает достоверность какого-либо доказательства, когда φ имеет какую-то другую форму или P не останавливается. Таким образом, R удовлетворяет требованиям приведенной выше теоремы о неполноте. Если хотите, вы можете позволить R* быть замыканием R при интуиционистской дедукции, и тогда R* будет интуиционистским неклассическим примером.

По моему мнению, феномен, на самом деле «ответственный» за неполноту, — это способность рассуждать о программах. Кто-то однажды сказал, что доказательство Гёделя было похоже на построение компилятора в арифметике, только чтобы он мог запускать примитивные рекурсивные программы (те, которые используют только циклы for, счетчик которых не может быть изменен внутри цикла).

Наконец, фундаментальная система, необходимая для доказательства теорем о неполноте, может быть очень слабой. Ключевое предположение состоит в том, что поведение программы четко определено, а именно, что для любой программы P и входных данных X либо P останавливается, либо P не останавливается, а выходные данные, если они есть, уникальны. Это допущение необходимо, иначе даже понятия непротиворечивости и полноты не будут четко определены. Короче говоря, достаточно иметь классическую логику поведения программы. Обратите внимание: поскольку поведение программы может быть закодировано как предложение о строках (как в предыдущем разделе), это означает, что в некотором смысле нам нужно только допустить классическую логику для строк, чтобы иметь возможность доказать теоремы о неполноте в закодированной форме. Если вы хотите доказать это в более естественной форме, вам понадобится базовая система, чтобы изначально поддерживать рассуждения о конечных последовательностях.

Обобщение

Мы можем полностью обобщить теоремы о неполноте, ослабив условие, согласно которому формальная система T имеет всегда останавливающийся верификатор доказательств V. Достаточно потребовать, чтобы V(φ,x) выдавало «да» точно тогда, когда x является доказательством φ, и не имеет значения, не останавливается ли V, когда x не является доказательством φ! Доказательство такое же, за исключением того, что вам просто нужно построить программу для распараллеливания всех вызовов V. На любом разумном языке программирования это можно сделать следующим образом. Каждый вызов V запускает пошаговую симуляцию выполнения V на заданных входных данных параллельно с остальной частью программы, поэтому в любое время может быть несколько (но конечное число) текущих симуляций. Если какая-либо симуляция достигает конца, вся программа завершается, и выходные данные этой симуляции возвращаются как выходные данные всей программы.

Заметим также, что это полное обобщение эквивалентно замене критерия наличия у T верификатора доказательства критерием наличия у T генератора теорем M, который представляет собой программу, которая работает вечно и в конечном итоге выводит каждую теорему T и не выводит ни одной строки, которая является не теорема Т. Тогда программа в доказательстве просто должна смоделировать M и дождаться, пока M сгенерирует A или B, а затем завершить всю программу и вывести соответствующий вывод. В приведенных выше доказательствах я не использовал полное обобщение, потому что не очевидно, какие языки программирования достаточно сильны, чтобы программы на них могли имитировать другие программы, и все практические формальные системы в любом случае имеют верификатор доказательств.

Обобщение на невычислимые формальные системы

Один приятный аспект этой точки зрения, основанной на вычислимости, заключается в том, что она автоматически релятивизирует любой вид класса Ω программ оракула. В частности, это же доказательство приводит к теоремам о неполноте для формальных систем, верификатором доказательств которых является программа в Ω и которая может рассуждать о программах в Ω. Этот результат можно использовать для доказательства того, что арифметическая иерархия не схлопывается ни на какой уровень, как показано в этом посте .

дальнейшее чтение

Сообщение в блоге Скотта Ааронсона, которое вдохновило некоторые из них , цитирует текст Клини по математической логике 1967 года для аналогичного доказательства теоремы Россера (теорема VIII и следствие I на страницах 286–288).

Статья Эмиля Поста 1944 года, в которой набросок доказательства в общих чертах соответствует приведенному выше доказательству с помощью проблемы остановки для формальных систем, пригодных для остановки программы. (Спасибо, Филип Уайт!)

Формальная версия приведенного выше доказательства теоремы Россера для формальных систем, интерпретирующих PA− .

Обсуждение фундаментальных вопросов, касающихся проблемы остановки и теоремы о неполноте .

Объяснение комбинатора фиксированной точки в λ-исчислении, упомянутого во вступительном абзаце .