Теорема Эрбрана¶

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

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

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

Более формально: пусть F — замкнутая формула логики первого порядка, приведённая к предварённой нормальной форме, а затем к сколемовской нормальной форме S. Пусть H — эрбрановский универсум (множество всех термов, построенных из констант и функциональных символов, встречающихся в S, с добавлением одной константы, если в S нет констант). Тогда F общезначима тогда и только тогда, когда существует конечное множество основных примеров (ground instances) дизъюнктов из S, которое пропозиционально невыполнимо.

¶Исторический контекст

Теорема была доказана Жаком Эрбраном в его докторской диссертации «Исследования по теории доказательства», опубликованной в 1930 году. Работа Эрбрана была частью более широкой программы Гильберта по формализации математики и доказательству её непротиворечивости. Эрбран трагически погиб в возрасте 23 лет во время горного похода, оставив после себя труд, который стал одним из краеугольных камней современной логики.

¶Основные понятия

¶Сколемовская нормальная форма

Для применения теоремы Эрбрана формулу необходимо привести к сколемовской нормальной форме. Этот процесс включает:

1. Удаление кванторов существования путём введения новых функциональных символов (сколемовских функций).
2. Вынесение всех кванторов общности в начало формулы.
3. Преобразование матрицы (бескванторной части) к конъюнктивной нормальной форме.

¶Эрбрановский универсум

Эрбрановский универсум H для множества дизъюнктов S — это множество всех термов, которые можно построить из:

• Констант, встречающихся в S (если S не содержит констант, добавляется одна константа, например, a).
• Функциональных символов, встречающихся в S.

¶Эрбрановская интерпретация

Эрбрановская интерпретация — это интерпретация, в которой:

• Область интерпретации — эрбрановский универсум H.
• Каждая константа интерпретируется как сама себя.
• Каждый функциональный символ интерпретируется как функция, строящая терм из аргументов.

¶Доказательство и значение

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

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

¶Значение

Теорема Эрбрана имеет фундаментальное значение для:

1. Автоматического доказательства теорем: она сводит проверку общезначимости формулы логики первого порядка к проверке пропозициональной невыполнимости конечного множества дизъюнктов. Это позволяет применять алгоритмы пропозициональной логики (например, метод резолюций) для решения задач в логике первого порядка.
2. Теории доказательств: теорема является одним из основных результатов, связывающих синтаксические и семантические аспекты логики.
3. Программирования в логике: лежит в основе работы таких языков, как Prolog.

¶Применение

¶Метод резолюций

Метод резолюций, разработанный Джоном Аланом Робинсоном в 1965 году, напрямую опирается на теорему Эрбрана. Он позволяет автоматически находить противоречие в множестве дизъюнктов, используя правило резолюции и унификацию. Теорема Эрбрана гарантирует, что если исходная формула общезначима, то метод резолюций рано или поздно найдёт пустой дизъюнкт (противоречие).

¶Проверка выполнимости

Теорема также используется в алгоритмах проверки выполнимости формул логики первого порядка (SMT-решатели). Она позволяет свести задачу к пропозициональной выполнимости, что делает возможным применение эффективных SAT-решателей.

¶Пример

Рассмотрим формулу: ∃x ∀y P(x, y) → ∀y ∃x P(x, y).

1. Приведём отрицание к сколемовской нормальной форме: ¬(∃x ∀y P(x, y) → ∀y ∃x P(x, y)) = ∃x ∀y P(x, y) ∧ ∃y ∀x ¬P(x, y).
2. После сколемизации: ∀y P(a, y) ∧ ∀x ¬P(x, b), где a и b — сколемовские константы.
3. Множество дизъюнктов: {P(a, y), ¬P(x, b)}.
4. Эрбрановский универсум: {a, b}.
5. Основные примеры: P(a, a), P(a, b), ¬P(a, b), ¬P(b, b).
6. Пропозициональная невыполнимость: дизъюнкты P(a, b) и ¬P(a, b) образуют противоречие. Следовательно, исходная формула общезначима.

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

Несмотря на свою фундаментальность, теорема Эрбрана имеет практические ограничения:

• Экспоненциальный рост: количество основных примеров может расти экспоненциально, что делает прямой перебор непрактичным для сложных формул.
• Неразрешимость: логика первого порядка в общем случае неразрешима, поэтому теорема Эрбрана не даёт алгоритма, который всегда завершается за конечное время. Она лишь утверждает, что если формула общезначима, то существует конечное множество, но не указывает способ его эффективного нахождения.

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

• Жак Эрбран опубликовал свою диссертацию в возрасте 22 лет, а через год погиб в горах.
• Теорема Эрбрана была независимо переоткрыта несколькими математиками, включая Курта Гёделя, который включил её в свою знаменитую статью о полноте логики первого порядка.
• Метод резолюций, основанный на теореме Эрбрана, стал одним из первых успешных методов автоматического доказательства теорем и используется до сих пор.

¶Источники

• Эрбран, Ж. «Исследования по теории доказательства» (1930).
• Робинсон, Дж. А. «Машино-ориентированная логика, основанная на принципе резолюции» (1965).
• Чан, Ч.-Л., Ли, Р. «Символическая логика и автоматическое доказательство теорем» (1973).
• Мендельсон, Э. «Введение в математическую логику» (1964).