Теорема Гёделя о полноте — фундаментальная теорема математической логики , устанавливающая соответствие между семантической истинностью и синтаксической доказуемостью в логике первого порядка .
Теорема о полноте применима к любой теории первого порядка : если T — такая теория, а φ — предложение (на том же языке), и каждая модель T — модель φ, то существует доказательство (первого порядка) φ, использующее утверждения T как аксиомы. Иногда это говорят так: «всё истинное во всех моделях доказуемо». (Это не противоречит теореме Гёделя о неполноте , которая касается формулы φ u , которая недоказуема в некоторой теории T, но истинна в «стандартной» модели натуральных чисел: φ u ложна в некоторых других , «нестандартных» моделях T. [1] )
Теорема о полноте устанавливает тесную связь между теорией моделей , которая занимается тем, что является истинным в различных моделях, и теорией доказательств , которая изучает, что может быть формально доказано в конкретных формальных системах .
Впервые это доказал Курт Гёдель в 1929 году. Затем это было упрощено, когда Леон Хенкин заметил в своей докторской диссертации , что трудная часть доказательства может быть представлена в виде теоремы о существовании модели (опубликованной в 1949 году). [2] Доказательство Хенкина было упрощено Гисбертом Хазенйегером в 1953 году. [3]
Существует множество дедуктивных систем для логики первого порядка, включая системы естественной дедукции и системы в стиле Гильберта . Общим для всех дедуктивных систем является понятие формальной дедукции . Это последовательность (или, в некоторых случаях, конечное дерево ) формул со специально обозначенным заключением . Определение дедукции таково, что она конечна и что можно алгоритмически проверить (например, с помощью компьютера или вручную), что данная последовательность (или дерево) формул действительно является выводом.
Формула первого порядка называется логически допустимой , если она истинна в любой структуре для языка формулы (т. е. для любого присвоения значений переменным формулы). Чтобы формально сформулировать, а затем доказать теорему о полноте, необходимо также определить дедуктивную систему. Дедуктивная система называется полной , если каждая логически допустимая формула является заключением некоторой формальной дедукции, а теорема о полноте для конкретной дедуктивной системы является теоремой о том, что она полна в этом смысле. Таким образом, в некотором смысле, для каждой дедуктивной системы существует своя теорема о полноте. Обратным к полноте является обоснованность , тот факт, что в дедуктивной системе доказуемы только логически допустимые формулы.
Если некоторая конкретная дедуктивная система логики первого порядка является обоснованной и полной, то она «совершенна» (формула доказуема тогда и только тогда, когда она логически верна), и, таким образом, эквивалентна любой другой дедуктивной системе с тем же качеством (любое доказательство в одной системе может быть преобразовано в другую).
Сначала мы фиксируем дедуктивную систему исчисления предикатов первого порядка, выбирая любую из известных эквивалентных систем. Первоначальное доказательство Гёделя предполагало систему доказательств Гильберта-Аккермана.
Теорема о полноте гласит, что если формула логически верна, то существует конечный вывод (формальное доказательство) формулы.
Таким образом, дедуктивная система является «полной» в том смысле, что для доказательства всех логически верных формул не требуется никаких дополнительных правил вывода. Обратным к полноте является обоснованность , тот факт, что в дедуктивной системе доказуемы только логически верные формулы. Вместе с обоснованностью (проверка которой проста) эта теорема подразумевает, что формула логически верна тогда и только тогда, когда она является заключением формального вывода.
Теорема может быть выражена более общо в терминах логического следствия . Мы говорим, что предложение s является синтаксическим следствием теории T , обозначаемым , если s доказуемо из T в нашей дедуктивной системе. Мы говорим, что s является семантическим следствием T , обозначаемым , если s выполняется в каждой модели T. Теорема о полноте тогда гласит, что для любой теории первого порядка T с хорошо упорядочиваемым языком и любого предложения s в языке T ,
Поскольку обратное утверждение (корректность) также верно, то отсюда следует, что тогда и только тогда, когда , и, таким образом, синтаксическое и семантическое следствие эквивалентны для логики первого порядка.
Эта более общая теорема используется неявно, например, когда показывается, что предложение доказуемо из аксиом теории групп путем рассмотрения произвольной группы и демонстрации того, что предложение удовлетворяется этой группой.
Первоначальная формулировка Гёделя выведена путем рассмотрения частного случая теории без какой-либо аксиомы.
Теорема о полноте может также пониматься в терминах согласованности , как следствие теоремы Хенкина о существовании модели . Мы говорим, что теория T синтаксически согласована , если не существует предложения s такого, что и s, и его отрицание ¬ s доказуемы из T в нашей дедуктивной системе. Теорема о существовании модели гласит, что для любой теории первого порядка T с хорошо упорядочиваемым языком
Другая версия, связанная с теоремой Лёвенгейма–Скулема , гласит:
Учитывая теорему Хенкина, теорему о полноте можно доказать следующим образом: Если , то не имеет моделей. По контрапозиции теоремы Хенкина, то является синтаксически противоречивым. Таким образом, противоречие ( ) доказуемо из в дедуктивной системе. Следовательно , и тогда по свойствам дедуктивной системы, .
Теорема о существовании модели и ее доказательство могут быть формализованы в рамках арифметики Пеано . Точнее, мы можем систематически определить модель любой непротиворечивой эффективной теории первого порядка T в арифметике Пеано, интерпретируя каждый символ T с помощью арифметической формулы, свободные переменные которой являются аргументами символа. (Во многих случаях нам нужно будет предположить, как гипотезу построения, что T непротиворечива, поскольку арифметика Пеано может не доказать этот факт.) Однако определение, выраженное этой формулой, не является рекурсивным (но, в общем случае, является Δ 2 ).
Важным следствием теоремы о полноте является то, что можно рекурсивно перечислить семантические следствия любой эффективной теории первого порядка, перечислив все возможные формальные выводы из аксиом теории, и использовать это для составления перечисления их заключений.
Это противоречит прямому значению понятия семантического следствия, которое количественно оценивает все структуры в определенном языке, что явно не является рекурсивным определением.
Кроме того, это делает понятие «доказуемости», а следовательно, и «теоремы», ясным понятием, зависящим только от выбранной системы аксиом теории, а не от выбора системы доказательства.
Теоремы Гёделя о неполноте показывают, что существуют неотъемлемые ограничения того, что может быть доказано в рамках любой данной теории первого порядка в математике. «Неполнота» в их названии относится к другому значению полноты (см. теорию моделей – Использование теорем о компактности и полноте ): теория является полной (или разрешимой), если каждое предложение в языке либо доказуемо ( ), либо опровержимо ( ).
Первая теорема о неполноте утверждает, что любое непротиворечивое , эффективное и содержащее арифметику Робинсона (« Q ») должно быть неполным в этом смысле, явно конструируя предложение , которое явно не является ни доказуемым, ни опровергаемым внутри . Вторая теорема о неполноте расширяет этот результат, показывая, что может быть выбрано так, чтобы оно выражало непротиворечивость самого себя.
Так как не может быть доказано в , теорема о полноте подразумевает существование модели в , которая ложна. Фактически, является предложением Π 1 , т.е. оно утверждает, что некоторое финитное свойство истинно для всех натуральных чисел; поэтому, если оно ложно, то некоторое натуральное число является контрпримером. Если бы этот контрпример существовал в пределах стандартных натуральных чисел, его существование было бы опровергнуто в пределах ; но теорема о неполноте показала, что это невозможно, поэтому контрпример не должен быть стандартным числом, и, таким образом, любая модель в , которая ложна, должна включать нестандартные числа .
Фактически, модель любой теории, содержащей Q, полученная путем систематического построения теоремы о существовании арифметической модели, всегда является нестандартной с неэквивалентным предикатом доказуемости и неэквивалентным способом интерпретации собственной конструкции, так что эта конструкция является нерекурсивной (поскольку рекурсивные определения были бы однозначными).
Кроме того, если хотя бы немного сильнее Q (например, если он включает индукцию для ограниченных экзистенциальных формул), то теорема Тенненбаума показывает, что он не имеет рекурсивных нестандартных моделей.
Теорема о полноте и теорема о компактности являются двумя краеугольными камнями логики первого порядка. Хотя ни одна из этих теорем не может быть доказана полностью эффективным образом, каждая из них может быть эффективно получена из другой.
Теорема о компактности гласит, что если формула φ является логическим следствием (возможно бесконечного) множества формул Γ, то она является логическим следствием конечного подмножества Γ. Это является непосредственным следствием теоремы о полноте, поскольку в формальном выводе φ может быть упомянуто только конечное число аксиом из Γ, и тогда обоснованность дедуктивной системы подразумевает, что φ является логическим следствием этого конечного множества. Это доказательство теоремы о компактности изначально принадлежит Гёделю.
Наоборот, для многих дедуктивных систем можно доказать теорему о полноте как эффективное следствие теоремы о компактности.
Неэффективность теоремы о полноте может быть измерена по линиям обратной математики . При рассмотрении над счетным языком теоремы о полноте и компактности эквивалентны друг другу и эквивалентны слабой форме выбора, известной как слабая лемма Кёнига , с эквивалентностью, доказуемой в RCA 0 (вариант второго порядка арифметики Пеано , ограниченный индукцией по формулам Σ 0 1 ). Слабая лемма Кёнига доказуема в ZF, системе теории множеств Цермело–Френкеля без аксиомы выбора, и, таким образом, теоремы о полноте и компактности для счетных языков доказуемы в ZF. Однако ситуация меняется, когда язык имеет произвольно большую мощность с тех пор, хотя теоремы о полноте и компактности остаются доказуемо эквивалентными друг другу в ZF, они также доказуемо эквивалентны слабой форме аксиомы выбора, известной как лемма об ультрафильтре . В частности, ни одна теория, расширяющая ZF, не может доказать теоремы о полноте или компактности над произвольными (возможно, несчетными) языками без доказательства леммы об ультрафильтре на множестве той же мощности.
Теорема о полноте является центральным свойством логики первого порядка , которое не выполняется для всех логик. Логика второго порядка , например, не имеет теоремы о полноте для своей стандартной семантики (хотя имеет свойство полноты для семантики Хенкина ), а множество логически допустимых формул в логике второго порядка не является рекурсивно перечислимым. То же самое верно для всех логик более высокого порядка. Можно создать надежные дедуктивные системы для логик более высокого порядка, но ни одна такая система не может быть полной.
Теорема Линдстрёма утверждает, что логика первого порядка является наиболее сильной (при соблюдении определенных ограничений) логикой, удовлетворяющей как требованиям компактности, так и полноты.
Теорема полноты может быть доказана для модальной логики или интуиционистской логики относительно семантики Крипке .
Первоначальное доказательство теоремы Гёделя сводилось к сведению проблемы к частному случаю для формул в определенной синтаксической форме, а затем к обработке этой формы с помощью специального аргумента.
В современных текстах по логике теорема Гёделя о полноте обычно доказывается с помощью доказательства Хенкина , а не с помощью оригинального доказательства Гёделя. Доказательство Хенкина напрямую конструирует модель термина для любой последовательной теории первого порядка. Джеймс Маргетсон (2004) разработал компьютеризированное формальное доказательство с использованием доказательной машины теоремы Изабеллы . [4] Известны и другие доказательства.
