3.10.2. Теорема Эрбрана

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

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

Для начала будем считать, что операции выполняются только над стандартными выражениями, представляющими собой дизъюнктивные формы которые называются предложениями:

Формула представляет собой конъюнкцию предложений: Ниже мы увидим, что подобная стандартизация всегда возможна для формул первого порядка. Входящие в предложения литералы не содержат символов или

Пусть Е представляет собой множество предложений, — множество констант, появляющихся в Е, и для всякого натурального числа множество представляет собой объединение множества и всех термов где — функция аргументов-термов из Пусть

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

1) Е — корень дерева А;

2) всякая вершина дерева А является подмножеством Е, случайным образом означенным;

3) всякий путь, исходящий из корня дерева, не может содержать одновременно где — какая-либо формула.

Ассоциировать (сопоставить) какое-то конкретное значение истинности с формулами, построенными над означает просто выбрать какой-то конкретный путь на А. Противоречие выявляется, когда приведенное выше условие 3 уже не удовлетворяется. Теорема Эрбрана гарантирует, что это достигается всегда, когда Е невыполнимо (т. е. противоречиво).

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

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

Теорема о резолюции. Пусть имеется формула в стандартной форме представления

и пусть имеется формула

Тогда если формула противоречива, то и формула также противоречива.

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

также противоречиво и С для не влияют на результат. Для логики первого порядка выполняется тождество

и, следовательно,

По правилу модус поненс и метатеореме имеем что приводит к требуемому результату

В противном случае, когда доказательство аналогично, если учесть, что

либо

и, следовательно, снова

В общем случае имеет вид

и, как и в предыдущем случае, получаем

Следовательно,

Используя теорему , получаем

либо.

и, следовательно,

Таким образом, формула выводима из формулы и предложение нового не добавляет, так как если противоречиво, то противоречиво и Более того, процесс последовательных “резолюций”, установленный таким образом, является полным, т. е. если формула Е противоречива, то резолюция докажет это противоречие за конечное число шагов, что как раз и гарантирует теорема Эрбрана.

Предложения называются родительскими предложениями к предложению, называемому резольвентой Разумеется, если предложения и -содержат переменные, что в общем случае имеет место в логике первого порядка, то с помощью процедуры унификации может быть найден общий литерал Несколько унификаций могут дать этот литерал как дерево формул, которое нужно построить, чтобы иолучить доказательство, т. е. противоречие.

Примеры резолюций

1) Исчисление высказываний. Пусть формула

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

2) Логика первого порядка. Пусть даны х, у, z, i, v — пять переменных, а, b и с — три константы, и — три каких-то предиката и следующее, выражение

Унификация дает три подстановки и три возможные резольвенты, исходя из

В этом случае доказательство будет также завершено, когда окажутся пустыми, т. е. когда внутреннее противоречие возникает при построении резольвенты. В данном случае это относится к и второму предложению в Подстановка дает т. е. снова то же предложение, резольвента и (пустое предложение). Таким образом, было противоречиво.