- По поводу теоремы о разреженности простых чисел см . Теорему Россера . Для общего введения в теоремы о неполноте см. Теоремы Гёделя о неполноте .
В математической логике , трюк россеровский в это метод доказательства неполноты теоремы Геделя без предположения о том , что теория рассматривается является ω-последовательным (Smorynski 1977, стр 840;. Мендельсон 1977, стр 160) . . Этот метод был введен Дж. Баркли Россером в 1936 г. как усовершенствование оригинального доказательства теорем о неполноте Гёделя, опубликованного в 1931 г.
В то время как первоначальное доказательство Гёделя использует предложение, которое гласит (неформально) «Это предложение недоказуемо», уловка Россера использует формулу, которая гласит: «Если это предложение доказуемо, существует более короткое доказательство его отрицания».
Задний план
Уловка Россера начинается с предположений теоремы Гёделя о неполноте. Выбирается теория Т, которая является эффективной, непротиворечивой и включает в себя достаточный фрагмент элементарной арифметики.
Доказательство Гёделя показывает, что для любой такой теории существует формула Доказательство T ( x , y ), которая имеет предполагаемое значение, что y - это натуральный числовой код (число Гёделя) для формулы, а x - это число Гёделя для доказательства, из аксиомы T формулы, закодированной через y . (В оставшейся части этой статьи не делается различия между числом y и формулой, кодируемой y , а число, кодирующее формулу φ, обозначается # φ). Кроме того, формула Pvbl T ( y ) определяется как ∃ x Proof T ( x , y ). Он предназначен для определения набора формул доказуемого из T .
Предположения относительно T также показывают, что он может определить функцию отрицания neg ( y ), обладающую тем свойством, что если y - это код для формулы φ, то neg ( y ) - это код для формулы ¬φ. Функция отрицания может принимать любое значение для входных данных, не являющихся кодами формул.
Гёделевское предложение теории T - это формула φ, иногда обозначаемая G T, такая, что T доказывает φ ↔ ¬Pvbl T (# φ). Доказательство Гёделя показывает, что если T непротиворечиво, то оно не может доказать свое предложение Гёделя; но чтобы показать, что отрицание предложения Гёделя также не доказуемо, необходимо добавить более сильное предположение, что теория является ω-непротиворечивой , а не просто непротиворечивой. Например, теория T = PA + ¬G PA доказывает ¬G T . Россер (1936) построил другое самореферентное предложение, которое можно использовать для замены предложения Гёделя в доказательстве Гёделя, устраняя необходимость предполагать ω-непротиворечивость.
Приговор Россеру
Для фиксированной арифметической теории T , пусть Доказательство T ( x , y ) и neg ( x ) будет ассоциированным предикатом доказательства и функцией отрицания.
Модифицированный предикат доказательства ДоказательствоR
T( x , y ) определяется как:
что обозначает
Этот модифицированный предикат доказательства используется для определения модифицированного предиката доказуемости PvblR
T( y ):
Неофициально, PvblR
T( y ) - это утверждение, что y доказуемо с помощью некоторого закодированного доказательства x, такого что не существует закодированного доказательства отрицания y . В предположении непротиворечивости T для каждой формулы φ формула PvblR
T(# φ) будет выполняться тогда и только тогда, когда выполняется Pvbl T (# φ), потому что если существует код для доказательства φ, то (следуя согласованности T ) кода для доказательства ¬φ не существует. Однако Pvbl T и PvblR
Tимеют различные свойства с точки зрения доказуемости в Т .
Непосредственным следствием определения является то, что если T включает в себя достаточно арифметических действий, то оно может доказать, что для любой формулы φ PvblR
T(φ) следует ¬PvblR
T(отр (φ)). Это потому, что в противном случае есть два числа n , m , кодирующие доказательства φ и ¬φ, соответственно, удовлетворяющие как n < m, так и m < n . (На самом деле T нужно только доказать, что такая ситуация не может иметь место ни для каких двух чисел, а также включить некоторую логику первого порядка)
Используя диагональную лемму , пусть ρ - такая формула, что T доказывает, что ρ ↔ ¬ PvblR
T(# ρ). Формула ρ представляет собой Россер предложение теории T .
Теорема Россера
Пусть T - эффективная, последовательная теория, включающая в себя достаточное количество арифметики, с предложением Россера ρ. Тогда верно следующее (Mendelson 1977, p. 160):
- T не доказывает, что ρ
- T не доказывает ¬ρ.
Чтобы доказать это, сначала покажем, что для формулы y и числа e , если ДоказательствоR
T(e, y) выполняется, то T доказывает ДоказательствоR
T(е, у). Это показано аналогично тому, как это делается в доказательстве Гёделя первой теоремы о неполноте: T доказывает доказательство T (e, y), отношения между двумя конкретными натуральными числами; один затем переходит все натуральные числа г меньше е по одному, так и для каждого г , Т доказывает ¬Proof Т (г, отр (у)), опять же , отношение между двумя числами бетона.
Предположение, что T включает в себя достаточно арифметических действий (фактически, требуется базовая логика первого порядка), гарантирует, что T также доказывает PvblR
T(y) в этом случае.
Кроме того, если Т соответствует и доказывает ф, то существует число е кодирования для ее доказательства в T , и не существует никакого числа кодирования для доказательства отрицания ф в Т . Следовательно, доказательствоR
T(e, y) выполняется, и, таким образом, T доказывает, что PvblR
T(# φ).
Доказательство (1) аналогично доказательству Гёделя первой теоремы о неполноте: предположим, что T доказывает ρ; то из предыдущего уточнения следует, что T доказывает PvblR
T(# ρ). Таким образом, T также доказывает ¬ρ. Но мы предположили, что T доказывает ρ, а это невозможно, если T согласован. Мы вынуждены заключить, что T не доказывает ρ.
Доказательство (2) также использует частную форму доказательстваR
T. Предположим, что T доказывает ¬ρ; то из предыдущего уточнения следует, что T доказывает PvblR
T(отр (# ρ)). Но из непосредственного следствия определения предиката доказуемости Россера, упомянутого в предыдущем разделе, следует, что T доказывает ¬PvblR
T(# ρ). Таким образом, T также доказывает ρ. Но мы предположили, что T доказывает ¬ρ, а это невозможно, если T согласован. Мы вынуждены заключить, что T не доказывает ¬ρ.
Рекомендации
- Мендельсон (1977), Введение в математическую логику
- Smorynski (1977), "Теорема о неполноте", в Руководстве по математической логике , Джон Барвиз , Ed., Северной Голландия, 1982, ISBN 0-444-86388-5
- Баркли Россер (сентябрь 1936 г.). «Расширения некоторых теорем Гёделя и Черча» . Журнал символической логики . 1 (3): 87–91. JSTOR 2269028 .
Внешние ссылки
- Авигад (2007), « Вычислимость и неполнота », конспекты лекций.