Теорема Гёделя о полноте - Gödel's completeness theorem

Формула ( x . R ( x , x )) (∀ x y . R ( x , y )) верна во всех структурах (слева показаны только самые простые 8). Согласно результату Гёделя о полноте, он должен иметь естественное доказательство дедукции (показано справа).

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

Теорема о полноте применима к любой теории первого порядка : если T - такая теория, а φ - предложение (на том же языке) и любая модель T является моделью φ, то существует доказательство (первого порядка) φ, используя утверждения T в качестве аксиом. Иногда говорят, что «все, что истинно, можно доказать».

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

Впервые это было доказано Куртом Гёделем в 1929 году. Затем оно было упрощено в 1947 году, когда Леон Хенкин в своей докторской диссертации заметил . тезис о том, что сложная часть доказательства может быть представлена ​​как модельная теорема существования (опубликована в 1949 г.). Доказательство Хенкина было упрощено Гисбертом Хазенджегером в 1953 году.

Предварительные мероприятия

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

Формула первого порядка называется логически действительной, если она верна в любой структуре языка формулы (т. Е. Для любого присвоения значений переменным формулы). Чтобы формально сформулировать, а затем доказать теорему о полноте, необходимо также определить дедуктивную систему. Дедуктивная система называется полной, если каждая логически верная формула является выводом некоторого формального вывода, а теорема о полноте для конкретной дедуктивной системы является теоремой о ее полноте в этом смысле. Таким образом, в некотором смысле для каждой дедуктивной системы существует своя теорема о полноте. Обратным к полноте является разумность , то есть тот факт, что только логически верные формулы доказуемы в дедуктивной системе.

Если какая-то конкретная дедуктивная система логики первого порядка является надежной и полной, то она «идеальна» (формула доказуема тогда и только тогда, когда она логически верна), что эквивалентно любой другой дедуктивной системе того же качества (любое доказательство в одной системе можно преобразовать в другую).

Заявление

Сначала мы зафиксируем дедуктивную систему исчисления предикатов первого порядка, выбрав любую из хорошо известных эквивалентных систем. Первоначальное доказательство Гёделя предполагало систему доказательств Гильберта-Аккермана.

Оригинальная формулировка Гёделя

Теорема о полноте говорит, что если формула логически верна, то существует конечный вывод (формальное доказательство) формулы.

Таким образом, дедуктивная система является «полной» в том смысле, что никаких дополнительных правил вывода не требуется для доказательства всех логически правильных формул. Обратным к полноте является разумность , то есть тот факт, что только логически верные формулы доказуемы в дедуктивной системе. Вместе с обоснованностью (которую легко проверить) эта теорема означает, что формула логически верна тогда и только тогда, когда она является выводом формального вывода.

Более общая форма

Теорема может быть выражена в более общем виде с точки зрения логического следствия . Мы говорим, что предложение s является синтаксическим следствием теории T , обозначаемой , если 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) разработал компьютеризированное формальное доказательство, используя средство доказательства теорем Изабель . Известны и другие доказательства.

Смотрите также

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

  • Гёдель, 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 . Тот же материал, что и диссертация, за исключением более коротких доказательств, более сжатых объяснений и исключения длинного введения.

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