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

Теорема Гёделя о полноте — это фундаментальное утверждение математической логики, установленное Куртом Гёделем в 1929 году, которое устанавливает эквивалентность между семантическим понятием логической общезначимости (истинности во всех моделях) и синтаксическим понятием формальной выводимости (доказуемости) в рамках логики первого порядка. Теорема является одной из основ современной математической логики и теории моделей, гарантируя, что для любой формулы, истинной во всех интерпретациях, существует формальное доказательство в исчислении предикатов.

История

Предпосылки

В начале XX века в математике возник кризис оснований, связанный с парадоксами наивной теории множеств (например, парадокс Рассела). В ответ на это Давид Гильберт предложил программу формализации всей математики: построить непротиворечивую и полную систему аксиом, в которой любое истинное утверждение можно было бы вывести механически. Для этого требовалось доказать, что формальные системы, такие как логика первого порядка, обладают свойством полноты: любая истинная формула доказуема.

Работа Гёделя

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

Развитие

Теорема Гёделя о полноте стала отправной точкой для развития теории моделей (Альфред Тарский, Леон Хенкин) и теории доказательств. В 1949 году Леон Хенкин предложил упрощённое доказательство, основанное на построении максимально непротиворечивого множества формул, которое стало стандартным в учебниках.

Формулировка

Основная версия

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

В символьной записи: \[ \Gamma \models \varphi \ \Rightarrow \ \Gamma \vdash \varphi \] где \(\Gamma \models \varphi\) означает семантическое следование (общезначимость), а \(\Gamma \vdash \varphi\) — синтаксическую выводимость.

Эквивалентная формулировка

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

Доказательство

Классическое доказательство Гёделя

Гёдель использовал метод построения модели для непротиворечивого множества формул. Основные шаги:

1. Расширение языка до счётного множества констант (для каждого экзистенциального утверждения добавляется константа-свидетель).
2. Построение максимального непротиворечивого множества формул (расширение исходного множества до полного, где для каждой формулы либо она, либо её отрицание принадлежит множеству).
3. Определение модели на основе термов языка: элементы модели — классы эквивалентности термов, а предикаты интерпретируются согласно принадлежности формул к множеству.

Упрощённое доказательство Хенкина (1949)

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

Следствия и значение

Связь с теоремой о неполноте

Теорема Гёделя о полноте часто противопоставляется его же теореме о неполноте (1931). Первая гарантирует полноту логики первого порядка, вторая — неполноту формальных систем, содержащих арифметику (например, арифметики Пеано). Различие в том, что теорема о полноте относится к чистому логическому исчислению, а теорема о неполноте — к теориям, включающим аксиомы, выражающие арифметику.

Применение в теории моделей

Теорема является краеугольным камнем теории моделей. Она позволяет:

• Доказывать существование моделей для непротиворечивых теорий (например, нестандартных моделей арифметики).
• Использовать компактность (следствие теоремы): если каждое конечное подмножество формул имеет модель, то всё множество имеет модель.
• Устанавливать эквивалентность между семантическими и синтаксическими свойствами теорий.

Влияние на основания математики

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

Критика и ограничения

Ограничения логики первого порядка

Теорема не распространяется на логики высших порядков (второй, третий и т.д.), где полнота не выполняется. Кроме того, она не гарантирует разрешимости: хотя доказательство существует, алгоритм его поиска может быть неэффективным (проблема остановки).

Конструктивность

Классическое доказательство Гёделя неконструктивно в том смысле, что оно не даёт способа построить доказательство для конкретной формулы. Однако существуют конструктивные варианты (например, с использованием теоремы Эрбрана).

Интересные факты

• Теорема Гёделя о полноте была доказана за год до его теоремы о неполноте, что создало напряжённость в математическом сообществе: сначала казалось, что формализация математики возможна, но затем выяснились её фундаментальные ограничения.
• В 1930 году Гёдель представил свою работу на конференции в Кёнигсберге, где также выступал Давид Гильберт, который тогда ещё верил в полную формализацию математики.
• Теорема о полноте является частным случаем более общей теоремы о компактности, которая широко используется в алгебре и теории чисел (например, для доказательства существования неархимедовых полей).

Источники

• Гёдель, К. «О полноте аксиом логического исчисления функций» (1930).
• Хенкин, Л. «Полнота формальных систем» (1949).
• Мендельсон, Э. «Введение в математическую логику» (1964).
• Ершов, Ю.Л., Палютин, Е.А. «Математическая логика» (1979).
• Boolos, G., Burgess, J., Jeffrey, R. «Computability and Logic» (2007).