12.0.4. Модели и опровержение

Из предыдущего рассуждения следует, что доказать противоречивость высказывания вида (5) в принципе тривиально, если число атомов конечно. Тривиальна ли эта задача на практике, зависит, разумеется, от количества атомов и от наших возможностей порождать и проверять модели. Вместе с тем интересно выяснить условия, гарантирующие конечность числа атомов. — это множество высказываний, истинных для тех атомов, которые непосредственно входят в и тех, которые можно из первых вывести. Последнее множество может быть бесконечным; в этом легко убедиться на следующем тривиальном примере. Пусть — высказывание, содержащее единственный атом:

Предположим, что определена функция Из (6) можно построить бесконечную последовательность

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

Предположим на время, что в нет переменных. Такая ситуация называется основным случаем, а соответствующий универсум (область определения) называется эрбрановской базой. В основном случае можно провести перечисление. Для иллюстрации такой процедуры воспользуемся упрощенной версией примера (табл. 12.1) и докажем для конкретной пары чисел (а не для пары чисел вообще, которую мы записали бы в виде истинность высказывания

Атомами здесь будут

Соответствующие предложения из А и их интерпретации таковы: Выполняется одно из отношений.

В этих обозначениях высказывание (8) имеет вид а его отрицание — вид . Для большей наглядности запишем это в виде двух отдельных предложений:

Объединяя (10) и (11), получаем

Поскольку в может быть только атомных высказываний, легко построить все возможные модели (см. табл. 12.2). Если для каждой из них хотя бы одно предложение в принимает значение ложь, то высказывание вида (5) будет ложным, и потому высказывание (8) будет истинным.

Таблица 12.2

Доказательство проводится (рис. 12.1) исключительно механическим способом (и не самым эффективным). На этом рисунке показано дерево порождения моделей. В каждом внутреннем узле дерева выбирается атом, а две выходящие из этого узла дуги определяются как значения истина и ложь упомянутого атома. В качестве первого узла здесь выбран узел так что все дуги, расположенные „слева“ от корня, указывают на модели, в которых принимает значение истина, а все дуги „справа” от корня указывают на модели, в которых принимает значение ложь.

Рис. 12.1. Дерево моделей для простой задачи без переменных.

Если высказывание (8), в самом деле, имплицируется (10), то каждая из этих моделей, представленная концевым узлом рассматриваемого дерева, припишет значение ложь по крайней мере одному из предложений в . В этом можно убедиться, проверив полученные модели.

Поскольку в табл. 12.2 нет таких комбинаций атомов, которые могут присвоить высказыванию (12) значение истина, то гипотеза (8) логически следует из соответствующих аксиом.

К сожалению, этот метод для более сложных случаев может не работать. Легко придумать высказывание с таким большим числом атомов, что этот метод перечисления окажется практически непригодным. Более того, возможен случай, когда наш универсум Эрбрана будет содержать бесконечно много атомов. Наконец, хотя этот метод и приводит к результату, он избыточен. Можно показать, что высказывание (12) противоречиво, исследуя и меньшее число моделей. Рассмотрим поддерево, изображенное на рис. 12.2, которое

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

Рис. 12.2. Дерево более общих моделей.

В рассмотренном примере это можно показать, просто проверив все частичные присваивания значений истинности атомам (см. табл. 12.3).

Таблица 12.3

12.0.5. Теорема Сколема — Эрбрана — Гёделя

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

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

Рис. 12.3. Бесконечное двоичное дерево атомов. Каждый узел дерева соответствует частичному присваиванию атомам значений истинности.

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

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

В теореме Сколема — Эрбрана — Гёделя утверждается, что если ложное (невыполнимое), то для некоторого высказывание будет невыполнимым. Это наводит на мысль об одном методе механического доказательства теорем. что надо сделать, это образовать последовательность высказываний каждое из которых получается некоторой подстановкой в построить дерево частичных присваиваний, содержащее все атомы

высказывания и проверить его выполнимость. Если имеет вид (5), т. е. содержит несколько аксиом и отрицание требуемого заключения, то при невыполнимости высказывание, содержащее указанные аксиомы и требуемое заключение (как в (4)), выполнимо, при условии что множество аксиом непротиворечиво.

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