Теорема Эрбранда - Herbrands theorem - Wikipedia

Не путать с Теорема Эрбрана – Рибета. или же Теорема Эрбрана о группах ветвления.

Теорема Эрбрана является фундаментальным результатом математическая логика получено Жак Эрбранд (1930).^[1] По сути, это позволяет снизить логика первого порядка к логика высказываний. Хотя Эрбранд первоначально доказал свою теорему для произвольных формул логики первого порядка,^[2] показанная здесь более простая версия, ограниченная формулами в предварительная форма содержащий только кванторы существования, стал более популярным.

Заявление

Позволять

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$

быть формулой логики первого порядка с ${\displaystyle F(y_{1},\ldots ,y_{n})}$ бескванторный, хотя он может содержать дополнительные свободные переменные. Эта версия теоремы Эрбрана утверждает, что приведенная выше формула действительна тогда и только тогда, когда существует конечная последовательность терминов ${\displaystyle t_{ij}}$, возможно, в расширении языка, с

${\displaystyle 1\leq i\leq k}$ и ${\displaystyle 1\leq j\leq n}$,

такой, что

${\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})}$

действует. Если он действителен, он называется Дизъюнкция Гербрана за

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n}).}$

Неформально: формула ${\displaystyle A}$ в предварительная форма содержащий только кванторы существования, доказуем (действителен) в логике первого порядка тогда и только тогда, когда дизъюнкция, состоящая из экземпляры замены бескванторной подформулы ${\displaystyle A}$ это тавтология (выводимая пропозиционально).

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

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

Доказательство нетривиальной направленности теоремы можно построить в соответствии со следующими этапами:

1. Если формула ${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$ справедливо, то по полноте отсечения последовательное исчисление, что следует из Gentzen с отсечение теоремы, есть доказательство без сечения ${\displaystyle \vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$.
2. Начиная сверху вниз, удалите выводы, которые вводят кванторы существования.
3. Удалите сокращающие выводы из ранее существовавших количественных формул, поскольку формулы (теперь с терминами, замененными ранее количественно определенными переменными) могут больше не быть идентичными после удаления количественных выводов.
4. При удалении сокращений накапливаются все соответствующие экземпляры замены ${\displaystyle F(y_{1},\ldots ,y_{n})}$ в правой части секвенции, что приводит к доказательству ${\displaystyle \vdash F(t_{11},\ldots ,t_{1n}),\ldots ,F(t_{k1},\ldots ,t_{kn})}$, из которого может быть получена дизъюнкция Гербрана.

Тем не мение, последовательное исчисление и отсечение не были известны во время теоремы Эрбранда, и Эрбранду пришлось доказывать свою теорему более сложным способом.

Обобщения теоремы Эрбрана

• Теорема Эрбрана была распространена на логика высшего порядка используя доказательства дерева расширения.^[3] Глубокое представление о доказательства дерева расширения соответствует дизъюнкции Эрбранда при ограничении логикой первого порядка.
• Дизъюнкции Хербрана и доказательства дерева расширения были расширены с помощью понятия разрезания. Из-за сложности сечения-исключения дизъюнкции Гербрана с разрезами могут быть неэлементарно меньше, чем стандартная дизъюнкция Гербранда.
• Дизъюнкции Эрбрана были обобщены на секвенции Гербрана, что позволило сформулировать теорему Гербрана для секвенций: «Сколемизированная секвенция выводима, если и только если она имеет секвенцию Гербрана».

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

• Структура Herbrand
• Интерпретация Herbrand
• Вселенная Herbrand
• Теорема компактности

Примечания

1. Ж. Эрбранд: Исследования по теории демонстрации. Travaux de la société des Sciences et des Lettres de Varsovie, Класс III, Математические и физические науки, 33, 1930.
2. Сэмюэл Р. Басс: "Справочник по теории доказательства". Глава 1, «Введение в теорию доказательств». Эльзевир, 1998.
3. Дейл Миллер: компактное представление доказательств. Studia Logica1987. Т. 46, No4. С. 347--370.

Рекомендации

• Басс, Сэмюэл Р. (1995), «О теореме Эрбрана» в Морисе, Даниэле; Лейвант, Рафаэль (ред.), Логика и вычислительная сложность, Конспект лекций по информатике, Берлин, Нью-Йорк: Springer-Verlag, стр.195–209, ISBN  978-3-540-60178-4.