Уловка Россерса - Rossers trick

По поводу теоремы о разреженности простых чисел см. Теорема Россера. Общее введение в теоремы о неполноте см. Теоремы Гёделя о неполноте.

В математическая логика, Уловка Россера это метод доказательства Теоремы Гёделя о неполноте без предположения, что рассматриваемая теория ω-согласованный (Сморинский, 1977, с. 840; Мендельсон, 1977, с. 160). Этот метод был введен Дж. Баркли Россер в 1936 году как усовершенствование оригинального доказательства теорем о неполноте Гёделя, опубликованного в 1931 году.

В то время как первоначальное доказательство Гёделя использует предложение, которое гласит (неофициально) «Это предложение недоказуемо», уловка Россера использует формулу, которая гласит: «Если это предложение доказуемо, существует более короткое доказательство его отрицания».

Фон

Уловка Россера начинается с предположений теоремы Гёделя о неполноте. Теория Т выбран такой, который является эффективным, последовательным и включает в себя достаточный фрагмент элементарной арифметики.

Доказательство Гёделя показывает, что для любой такой теории существует формула Доказательство_Т(Икс,у), который имеет предполагаемое значение, что у является кодом натурального числа (числом Гёделя) формулы и Икс число Гёделя для доказательства из аксиом Т, формулы, закодированной у. (В остальной части этой статьи не делается различия между числом у и формула в кодировке у, а число, кодирующее формулу φ, обозначается # φ). Кроме того, формула Pvbl_Т(у) определяется как ∃Икс Доказательство_Т(Икс,у). Он предназначен для определения набора формул, выводимых из Т.

Предположения о Т также показывают, что он может определить функцию отрицания neg (у) со свойством, что если у код для формулы φ, то neg (у) является кодом формулы ¬φ. Функция отрицания может принимать любое значение для входных данных, не являющихся кодами формул.

Гёделевское предложение теорииТ - формула φ, иногда обозначаемая G_Т такой, что Т доказывает φ ↔ ¬Pvbl_Т(# φ). Доказательство Гёделя показывает, что если Т непротиворечиво, то не может доказать свое предложение Гёделя; но для того, чтобы показать, что отрицание предложения Гёделя также не доказуемо, необходимо добавить более сильное предположение, что теория ω-согласованный, а не просто последовательный. Например, теория T = PA + ¬G_PA доказывает ¬G_Т. Россер (1936) построил другое самореферентное предложение, которое можно использовать для замены предложения Гёделя в доказательстве Гёделя, устраняя необходимость предполагать ω-непротиворечивость.

Приговор Россеру

Для фиксированной арифметической теории Т, пусть Доказательство_Т(Икс,у) и нег (Икс) - связанный предикат доказательства и функция отрицания.

Модифицированный предикат доказательства Доказательство^р_Т(Икс,у) определяется как:

${\displaystyle \mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))],}$

что обозначает

${\displaystyle \lnot \mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))].}$

Этот модифицированный предикат доказательства используется для определения модифицированного предиката доказуемости Pvbl^р_Т(у):

${\displaystyle \mathrm {Pvbl} _{T}^{R}(y)\equiv \exists x\mathrm {Proof} _{T}^{R}(x,y).}$

Неофициально, Pvbl^р_Т(у) - это утверждение, что у доказуемо с помощью некоторого закодированного доказательства Икс такое, что не существует меньшего закодированного доказательства отрицания у. В предположении, что Т непротиворечиво, для каждой формулы φ формула Pvbl^р_Т(# φ) будет выполняться тогда и только тогда, когда Pvbl_Т(# φ) выполняется, потому что если существует код для доказательства φ, то (следуя согласованности Т) кода для доказательства ¬φ нет. Однако Pvbl_Т и Pvbl^р_Т обладают разными свойствами с точки зрения доказуемости в Т.

Непосредственным следствием определения является то, что если Т включает в себя достаточно арифметики, то можно доказать, что для любой формулы φ, Pvbl^р_Т(φ) следует ¬Pvbl^р_Т(отр (φ)). Это потому, что в противном случае есть два числа п,м, кодирование доказательств φ и ¬φ соответственно, удовлетворяющих обоим п<м и м<п. (Фактически Т нужно только доказать, что такая ситуация не может иметь место ни для каких двух чисел, а также включить некоторую логику первого порядка)

С использованием диагональная лемма, пусть ρ - формула такая, что Т доказывает ρ ↔ ¬ Pvbl^р_Т(# ρ). Формула ρ - это Приговор Россера теории Т.

Теорема Россера

Позволять Т быть эффективной, последовательной теорией, включающей в себя достаточное количество арифметики, с предложением Россера ρ. Тогда справедливо следующее (Mendelson 1977, p. 160):

1. Т не доказывает ρ
2. Т не доказывает ¬ρ.

Чтобы доказать это, сначала покажем, что для формулы y и числа е, если Доказательство^р_Т(e, y) выполняется, то Т доказывает доказательство^р_Т(е, у). Это показано аналогично тому, как это сделано в доказательстве Гёделя первой теоремы о неполноте: Т доказывает доказательство_Т(e, y), отношение между двумя конкретными натуральными числами; затем перебирают все натуральные числа z меньше чем е один за другим и для каждого z, Т доказывает ¬ Доказательство_Т(z, neg (y)), опять же, связь между двумя конкретными числами.

Предположение, что Т включает в себя достаточное количество арифметики (фактически, требуется базовая логика первого порядка), чтобы гарантировать, что Т также доказывает Pvbl^р_Т(y) в этом случае.

Кроме того, если Т непротиворечиво и доказывает φ, то существует число е кодирование для его доказательства в Т, и нет числового кодирования для доказательства отрицания φ в Т. Следовательно, доказательство^р_Т(e, y) выполняется, поэтому Т доказывает Pvbl^р_Т(# φ).

Доказательство (1) аналогично доказательству Гёделя первой теоремы о неполноте: предположим Т доказывает ρ; тогда из предыдущего уточнения следует, что Т доказывает Pvbl^р_Т(# ρ). Таким образом Т также доказывает ¬ρ. Но мы предположили Т доказывает ρ, и это невозможно, если Т согласуется. Мы вынуждены сделать вывод, что Т не доказывает ρ.

Доказательство (2) также использует частную форму доказательства^р_Т. Предполагать Т доказывает ¬ρ; тогда из предыдущего уточнения следует, что Т доказывает Pvbl^р_Т(отр (# ρ)). Но из непосредственного следствия определения предиката доказуемости Россера, упомянутого в предыдущем разделе, следует, что Т доказывает ¬Pvbl^р_Т(# ρ). Таким образом Т также доказывает ρ. Но мы предположили Т доказывает ¬ρ, а это невозможно, если Т согласуется. Мы вынуждены сделать вывод, что Т не доказывает ¬ρ.

Рекомендации

• Мендельсон (1977), Введение в математическую логику
• Сморинский (1977), "Теоремы о неполноте", в Справочник по математической логике, Джон Барвайз / Ред., Северная Голландия, 1982 г., ISBN  0-444-86388-5
• Россер (1936), «Расширения некоторых теорем Гёделя и Чёрча», Журнал символической логики, т. 1, с. 87–91.

внешняя ссылка

• Авигад (2007 г.) "Вычислимость и неполнота ", конспект лекций.