Теорема Гёделя о полноте

Теорема Гёделя о полноте является важной теоремой в формальной логике, которая была впервые доказана Куртом Гёделем в 1929 году. В своей наиболее знакомой формулировке она утверждает, что в логике первого порядка произвольная логически верная формула доказуема.

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

Формула называется логически верной, если она истинна в произвольной модели языка, который используется для записи формулы. Для формальной формулировки теорему Гёделя о полноте необходимо определить понятие «модель». Базовое определение этого понятия приводится в теории моделей.

Другое понимание теоремы Гёделя о полноте говорит о том, что система правил вывода исчисления предикатов первого порядка является «полной» в том смысле, что для доказательства всех логически верных формул нет надобности вводить дополнительные правила вывода. Дополнительно к полноте система правил вывода исчисления предикатов первого порядка также обладает прочностью, то есть эта система применима только к логически верным формулам.

Раздел математической логики, который изучает проблемы истинности высказываний в различных моделях, называется теорией моделей. Раздел, называемый «теория доказательств», изучает возможности доказательства высказываний в рамках заданной формальной системы. Теорема о полноте связывает оба этих фундаментальных раздела, предоставляя связь между синтаксисом и семантикой. Однако теорема о полноте не должна применяться в качестве обоснования стирания границ между указанными разделами. Фактически, первая теорема Гёделя о неполноте показывает, что в математике существуют определённого рода ограничения на возможности формального доказательства утверждений. Тут же необходимо отметить, что теорема Гёделя о неполноте использует иной смысл слова «полный», нежели теорема о полноте. В частности, теорема о полноте используется только в логике первого порядка, в то время как первая теорема о неполноте применима к теориям первого порядка, которые включают в себя как логику, так и другие формальные системы.

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

Теорема Гёделя о полноте является одним из центральных принципов логики первого порядка, но она не применима к другим логикам. К примеру, логика второго порядка не имеет в своём составе теоремы о полноте.

Теорема Гёделя о полноте эквивалентна лемме ультрафильтра, слабой форме аксиомы выбора, которая доказывается в рамках аксиоматики Цермело-Френкеля, в которой нет аксиомы выбора.

Из теоремы о полноте следует теорема компактности, другое фундаментальное свойство логики первого порядка.

См. также

• Теоремы Гёделя о неполноте

Литература

• Kurt Gödel. Über die Vollständigkeit des Logikkalküls, doctoral dissertation, University Of Vienna, 1929. Эта диссертация включает оригинальное доказательство теоремы о полноте.
• Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionen-kalküls, Monatshefte für Mathematik und Physik 37 (1930), 349-360. Эта статья содержит тот же материал, что и в докторской диссертации в переработанной и укороченной форме. Доказательства более просты, объяснения более сжаты, пространное введение опущено.