Теорема Гёделя о полноте - это фундаментальная теорема математической логики, которая устанавливает соответствие между семантической истинностью и синтаксической доказуемостью в логике первого порядка .
Теорема о полноте применима к любой теории первого порядка : если T - такая теория, а φ - предложение (на том же языке) и любая модель T является моделью φ, то существует доказательство (первого порядка) φ, используя утверждения T в качестве аксиом. Иногда говорят, что «все, что истинно, можно доказать».
Он устанавливает тесную связь между теорией моделей, которая имеет дело с тем, что истинно в различных моделях, и теорией доказательства , изучающей то, что может быть формально доказано в конкретных формальных системах .
Впервые это было доказано Куртом Гёделем в 1929 году. Затем оно было упрощено в 1947 году, когда Леон Хенкин в своей докторской диссертации заметил . тезис о том, что сложная часть доказательства может быть представлена как модельная теорема существования (опубликована в 1949 г.). Доказательство Хенкина было упрощено Гисбертом Хазенджегером в 1953 году.
Предварительные мероприятия
Существует множество дедуктивных систем для логики первого порядка, включая системы естественного вывода и системы гильбертова . Общим для всех дедуктивных систем является понятие формальной дедукции . Это последовательность (или, в некоторых случаях, конечное дерево ) формул со специально обозначенным выводом . Определение дедукции таково, что она конечна и что можно алгоритмически (с помощью компьютера , например, или вручную) проверить, что данная последовательность (или дерево) формул действительно является дедукцией.
Формула первого порядка называется логически действительной, если она верна в любой структуре языка формулы (т. Е. Для любого присвоения значений переменным формулы). Чтобы формально сформулировать, а затем доказать теорему о полноте, необходимо также определить дедуктивную систему. Дедуктивная система называется полной, если каждая логически действительная формула является выводом некоторого формального вывода, а теорема о полноте для конкретной дедуктивной системы является теоремой о ее полноте в этом смысле. Таким образом, в некотором смысле для каждой дедуктивной системы существует своя теорема о полноте. Обратным к полноте является разумность , то есть тот факт, что только логически верные формулы доказуемы в дедуктивной системе.
Если какая-то конкретная дедуктивная система логики первого порядка является надежной и полной, то она «идеальна» (формула доказуема тогда и только тогда, когда она логически верна), что эквивалентно любой другой дедуктивной системе того же качества (любое доказательство в одной системе можно преобразовать в другую).
Заявление
Сначала мы зафиксируем дедуктивную систему исчисления предикатов первого порядка, выбрав любую из хорошо известных эквивалентных систем. Первоначальное доказательство Гёделя предполагало систему доказательств Гильберта-Аккермана.
Оригинальная формулировка Гёделя
Теорема о полноте говорит, что если формула логически верна, то существует конечный вывод (формальное доказательство) формулы.
Таким образом, дедуктивная система является «полной» в том смысле, что никаких дополнительных правил вывода не требуется для доказательства всех логически правильных формул. Обратным к полноте является разумность , то есть тот факт, что только логически верные формулы доказуемы в дедуктивной системе. Вместе с обоснованностью (которую легко проверить) эта теорема означает, что формула логически верна тогда и только тогда, когда она является выводом формального вывода.
Более общая форма
Теорема может быть выражена в более общем виде с точки зрения логического следствия . Мы говорим, что предложение s является синтаксическим следствием теории T , обозначаемой, если s доказуемо из T в нашей дедуктивной системе. Будем говорить , что s является семантическое следствие из Т , обозначаемый, Если ы держит в каждой модели из T . Теорема о полноте говорит, что для любой теории первого порядка T с хорошо упорядочиваемым языком и любого предложения s на языке T ,
- если , тогда .
Поскольку верно и обратное (правильность), отсюда следует, что если и только если , и, таким образом, синтаксические и семантические последствия для логики первого порядка эквивалентны.
Эта более общая теорема используется неявно, например, когда предложение доказуемо на основе аксиом теории групп , рассматривая произвольную группу и показывая, что предложение удовлетворяется этой группой.
Исходная формулировка Гёделя выводится из частного случая теории без какой-либо аксиомы.
Теорема существования модели
Теорема о полноте также может быть понята с точки зрения согласованности , как следствие теоремы о существовании модели Хенкина . Будем говорить , что теория T является синтаксически непротиворечива , если нет приговора s такое , что оба s и его отрицание ¬ s доказуемы из T в нашей дедуктивной системе. Теорема существования модели гласит, что для любой теории первого порядка T с хорошо упорядочиваемым языком
- если синтаксически непротиворечиво, то есть модель.
Другая версия, связанная с теоремой Левенхайма – Сколема , гласит:
- Каждая синтаксически последовательная счетная теория первого порядка имеет конечную или счетную модель.
Учитывая теорему Хенкина, теорему о полноте можно доказать следующим образом: если , тогда нет моделей. По контрасту теоремы Хенкина, тогдасинтаксически несогласован. Итак, противоречие () доказуемо из в дедуктивной системе. Следовательно, а затем по свойствам дедуктивной системы .
Как теорема арифметики
Теорема существования модели и ее доказательство могут быть формализованы в рамках арифметики Пеано . Точнее, мы можем систематически определять модель любой непротиворечивой эффективной теории первого порядка T в арифметике Пеано, интерпретируя каждый символ T с помощью арифметической формулы, свободные переменные которой являются аргументами символа. (Во многих случаях нам нужно будет предположить в качестве гипотезы конструкции, что T непротиворечиво, поскольку арифметика Пеано не может доказать этот факт.) Однако определение, выраженное этой формулой, не является рекурсивным (но, в общем, является , Δ 2 ).
Последствия
Важным следствием теоремы о полноте является то, что можно рекурсивно перечислить семантические следствия любой эффективной теории первого порядка, перечислив все возможные формальные выводы из аксиом теории, и использовать это для получения перечисления своих выводов. .
Это контрастирует с прямым значением понятия семантического следствия, которое дает количественную оценку по всем структурам на конкретном языке, что явно не является рекурсивным определением.
Кроме того, это делает концепцию «доказуемости» и, следовательно, «теоремы» четкой концепцией, которая зависит только от выбранной системы аксиом теории, а не от выбора системы доказательств.
Связь с теоремами о неполноте
Теоремы Гёделя о неполноте показывают, что существуют внутренние ограничения тому, что может быть доказано в рамках любой данной теории первого порядка в математике. «Неполнота» в их названии относится к другому значению полного (см. Теорию моделей - Использование теорем о компактности и полноте ): Теория является полным (или разрешимым), если каждое предложение на языке либо доказуемо () или опровергнутый ().
Первая теорема о неполноте утверждает, что любое который является непротиворечивым , эффективным и содержит арифметику Робинсона (" Q "), должен быть неполным в этом смысле за счет явного построения предложения который нельзя доказать или опровергнуть в рамках . Вторая теорема о неполноте расширяет этот результат, показывая, что можно выбрать так, чтобы он выражал последовательность сам.
С не может быть опровергнуто в , из теоремы о полноте следует существование модели в котором ложно. По факту,является Π 1 предложение , то есть в нем говорится , что некоторые finitistic свойство верно для всех натуральных чисел; так что если оно ложно, то контрпримером является некоторое натуральное число. Если бы этот контрпример существовал в рамках стандартных натуральных чисел, его существование опровергло бы в ; но теорема о неполноте показала, что это невозможно, поэтому контрпример не должен быть стандартным числом, и, следовательно, любая модель в котором ложно, должны включать нестандартные числа.
Фактически, модель любой теории, содержащей Q, полученная систематическим построением теоремы о существовании арифметической модели, всегда нестандартна с неэквивалентным предикатом доказуемости и неэквивалентным способом интерпретации своей собственной конструкции, так что эта конструкция нерекурсивен (поскольку рекурсивные определения были бы однозначными).
Кроме того, если хотя бы немного сильнее Q (например, если он включает индукцию для ограниченных экзистенциальных формул), то теорема Тенненбаума показывает, что у него нет рекурсивных нестандартных моделей.
Связь с теоремой компактности
Теорема полноты и теорема компактности - два краеугольных камня логики первого порядка. Хотя ни одна из этих теорем не может быть доказана полностью эффективно , каждая из них может быть эффективно получена из другой.
Теорема компактности утверждает, что если формула φ является логическим следствием (возможно, бесконечного) множества формул Γ, то она является логическим следствием конечного подмножества Γ. Это является непосредственным следствием теоремы о полноте, потому что только конечное число аксиом из Γ может быть упомянуто при формальном выводе φ, и тогда из правильности дедуктивной системы следует, что φ является логическим следствием этого конечного множества. Это доказательство теоремы компактности первоначально принадлежит Гёделю.
И наоборот, для многих дедуктивных систем можно доказать теорему о полноте как эффективное следствие теоремы о компактности.
Неэффективность теоремы о полноте можно измерить с помощью обратной математики . При рассмотрении над счетным языком теоремы о полноте и компактности эквивалентны друг другу и эквивалентны слабой форме выбора, известной как слабая лемма Кенига , с эквивалентностью, доказуемой в RCA 0 (вариант второго порядка арифметики Пеано, ограниченный индукцией по Σ 0 1 формулам). Лемма Слабого Кенига доказуема в ZF, системе теории множеств Цермело – Френкеля без аксиомы выбора, и, таким образом, теоремы о полноте и компактности для счетных языков доказуемы в ZF. Однако ситуация иная, когда язык имеет произвольно большую мощность, с тех пор, хотя теоремы о полноте и компактности остаются доказуемо эквивалентными друг другу в ZF, они также доказуемо эквивалентны слабой форме аксиомы выбора, известной как лемма об ультрафильтрации . В частности, никакая теория, расширяющая ZF, не может доказать теоремы о полноте или компактности над произвольными (возможно, несчетными) языками без доказательства леммы об ультрафильтре на множестве той же мощности.
Полнота в другой логике
Теорема о полноте - это центральное свойство логики первого порядка, которое справедливо не для всех логик. Логика второго порядка , например, не имеет теоремы о полноте для своей стандартной семантики (но имеет свойство полноты для семантики Хенкина ), а набор логически действительных формул в логике второго порядка не является рекурсивно перечислимым. То же верно для всех логик более высокого порядка. Можно создать здоровые дедуктивные системы для логики более высокого порядка, но никакая такая система не может быть полной.
Теорема Линдстрема утверждает, что логика первого порядка является самой сильной (с некоторыми ограничениями) логикой, удовлетворяющей как компактности, так и полноте.
Теорема полноты может быть доказана для модальной логики или интуиционистской логики относительно семантики Крипке .
Доказательства
Первоначальное доказательство теоремы Гёделем сводилось к тому, что проблема сводилась к частному случаю формул в определенной синтаксической форме, а затем обрабатывалась эта форма с помощью специального аргумента.
В современных текстах по логике теорема Гёделя о полноте обычно доказывается с помощью доказательства Хенкина , а не с помощью оригинального доказательства Гёделя. Доказательство Хенкина напрямую строит термальную модель для любой непротиворечивой теории первого порядка. Джеймс Маргетсон (2004) разработал компьютеризированное формальное доказательство, используя средство доказательства теорем Изабель . [1] Известны и другие доказательства.
Смотрите также
- Теоремы Гёделя о неполноте
- Оригинальное доказательство теоремы Гёделя о полноте
дальнейшее чтение
- Гёдель, K (1929). "Über die Vollständigkeit des Logikkalküls" . Докторская диссертация. Венский университет. Цитировать журнал требует
|journal=
( помощь ) Первое доказательство теоремы о полноте. - Гёдель, К. (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik (на немецком языке). 37 (1): 349–360. DOI : 10.1007 / BF01696781 . JFM 56.0046.04 . S2CID 123343522 . Тот же материал, что и диссертация, за исключением более коротких доказательств, более сжатых объяснений и исключения длинного введения.
- ^ Джеймс Маргетсон (сентябрь 2004 г.). Доказательство теоремы о полноте в Isabelle / HOL (PDF) (Технический отчет).
Внешние ссылки
- Стэнфордская энциклопедия философии : « Курт Гёдель » - Джульетта Кеннеди .
- Биография MacTutor: Курт Гёдель.
- Детловс, Вилнис, и Подниекс, Карлис, " Введение в математическую логику ".