Трюк Россера

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

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

Фон

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

Доказательство Гёделя показывает, что для любой такой теории существует формула $\operatorname {Proof} _{T}(x,y)$ который имеет предполагаемое значение, что $y$ - это натуральный числовой код (число Гёделя) для формулы и $x$ — число Гёделя для доказательства, исходя из аксиом $T$ , формулы, закодированной $y$ . (В оставшейся части этой статьи не делается никакого различия между количеством $y$ и формула, закодированная $y$ , и число, кодирующее формулу $\phi$ обозначается $\#\phi$ .) Кроме того, формула $\operatorname {Pvbl} _{T}(y)$ определяется как $\exists x\operatorname {Proof} _{T}(x,y)$ . Он предназначен для определения множества формул, доказуемых из $T$ .

Предположения о $T$ также покажите, что он способен определить функцию отрицания ${\text{neg}}(y)$ , со свойством, что если $y$ это код формулы $\phi$ затем ${\text{neg}}(y)$ это код формулы $\neg \phi$ . Функция отрицания может принимать любое значение для входных данных, которые не являются кодами формул.

Предложение Гёделя теории $T$ это формула $\phi$ , иногда обозначаемый $G_{T}$ , такой, что $T$ доказывает $\phi$ ↔ $\neg \operatorname {Pvbl} _{T}(\#\phi )$ . Доказательство Гёделя показывает, что если $T$ непротиворечив, то он не может доказать свое предложение Гёделя; но чтобы показать, что отрицание предложения Гёделя также недоказуемо, необходимо добавить более сильное предположение о том, что теория ω-непротиворечива , а не просто непротиворечива. Например, теория $T={\text{PA}}+\neg {\text{G}}_{PA}$ , в котором PA — аксиомы Пеано , доказывает $\neg G_{T}$ . Россер (1936) построил другое самореферентное предложение, которое можно использовать для замены предложения Гёделя в доказательстве Гёделя, устраняя необходимость предполагать ω-непротиворечивость.

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

Для фиксированной арифметической теории $T$ , позволять $\operatorname {Proof} _{T}(x,y)$ и ${\text{neg}}(x)$ быть связанным предикатом доказательства и функцией отрицания.

Модифицированный предикат доказательства $\operatorname {Proof} _{T}^{R}(x,y)$ определяется как:

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

это означает, что

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

Этот модифицированный предикат доказательства используется для определения модифицированного предиката доказуемости. $\operatorname {Pvbl} _{T}^{R}(y)$ :

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

Неофициально, $\operatorname {Pvbl} _{T}^{R}(y)$ это утверждение, что $y$ доказуемо с помощью некоторого закодированного доказательства $x$ так что не существует меньшего закодированного доказательства отрицания $y$ . В предположении, что $T$ непротиворечиво, для каждой формулы $\phi$ формула $\operatorname {Pvbl} _{T}^{R}(\#\phi )$ будет выполняться тогда и только тогда, когда $\operatorname {Pvbl} _{T}(\#\phi )$ верно, потому что если существует код для доказательства $\phi$ , тогда (следуя непротиворечивости $T$ ) нет кода для доказательства $\neg \phi$ . Однако, $\operatorname {Pvbl} _{T}(\#\phi )$ и $\operatorname {Pvbl} _{T}^{R}(\#\phi )$ обладают разными свойствами с точки зрения доказуемости в $T$ .

Непосредственным следствием определения является то, что если $T$ включает достаточно арифметики, то можно доказать, что для каждой формулы $\phi$ , $\operatorname {Pvbl} _{T}^{R}(\phi )$ подразумевает $\neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))$ . Это потому, что в противном случае есть два числа $n,m$ , кодирование доказательств $\phi$ и $\neg \phi$ соответственно, удовлетворяющие обоим $n<m$ и $m<n$ . (Фактически $T$ нужно только доказать, что такая ситуация не может иметь место ни для каких двух чисел, а также включить некоторую логику первого порядка)

Используя диагональную лемму , пусть $\rho$ быть формулой такой, что $T$ доказать ρ ↔ ¬ Pvbl ^Р
_Т (#р). $\rho$ ↔ $\neg \operatorname {Pvbl} _{T}(\#\rho )$ . Формула $\rho$ это предложение Россера теории $T$ .

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

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

$T$ не доказывает $\rho$
$T$ не доказывает $\neg \rho$

Чтобы доказать это, сначала покажем, что для формулы $y$ и номер $e$ , если $\operatorname {Proof} _{T}^{R}(e,y)$ держится, тогда $T$ доказывает $\operatorname {Proof} _{T}^{R}(e,y)$ . Это показано аналогично тому, что сделано в доказательстве Гёделя первой теоремы о неполноте: $T$ доказывает $\operatorname {Proof} _{T}(e,y)$ , отношение между двумя конкретными натуральными числами; затем перебирают все натуральные числа $z$ меньше, чем $e$ по одному и для каждого $z$ , $T$ доказывает $\neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y))$ , опять же, связь между двумя конкретными числами.

Предположение, что $T$ включает достаточное количество арифметических операций (фактически требуется базовая логика первого порядка) гарантирует, что $T$ также доказывает $\operatorname {Pvbl} _{T}^{R}(y)$ в таком случае.

Кроме того, если $T$ является последовательным и доказывает $\phi$ , то есть число $e$ кодирование для его доказательства в $T$ , и нет числового кодирования для доказательства отрицания $\phi$ в $T$ . Поэтому $\operatorname {Proof} _{T}^{R}(e,y)$ держится, и, таким образом, $T$ доказывает $\operatorname {Pvbl} _{T}^{R}(\#\phi )$ .

Доказательство (1) аналогично доказательству Гёделя первой теоремы о неполноте: предположим, что $T$ доказывает $\rho$ ; тогда из предыдущего уточнения следует, что $T$ доказывает $\operatorname {Pvbl} _{T}^{R}(\#\rho )$ . Таким образом $T$ также доказывает $\neg \rho$ . Но мы предполагали $T$ доказывает $\rho$ , а это невозможно, если $T$ является последовательным. Мы вынуждены заключить, что $T$ не доказывает $\rho$ .

Доказательство (2) также использует конкретную форму $\operatorname {Proof} _{T}^{R}$ . Предполагать $T$ доказывает $\neg \rho$ ; тогда из предыдущего уточнения следует, что $T$ доказывает $\operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))$ . Но из непосредственного следствия определения предиката доказуемости Россера, упомянутого в предыдущем разделе, следует, что $T$ доказывает $\neg \operatorname {Pvbl} _{T}^{R}(\#\rho )$ . Таким образом $T$ также доказывает $\rho$ . Но мы предполагали $T$ доказывает $\neg \rho$ , а это невозможно, если $T$ является последовательным. Мы вынуждены заключить, что $T$ не доказывает $\neg \rho$ .

Ссылки

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

Внешние ссылки

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