Логика естественных рассуждений - Кулик Б.А.
ISBN 5-7940-0080-5
Скачать (прямая ссылка):
Теорема Б. 14. Если в СТ-замыкании корректной Е-структуры E содержится элементарное суждение A-* В, то
(і)Л*В = 0; (ii) Л + Л = і.
Доказательство. Докажем (і). Предположим, что в E существует базовый литерал 0, такой что W=А* В. Тогда в соответствии с правилом (2) получаем W-* А и W-* В. В то же время эта пара суждений несовместима с существующим в E суждением А —* В, поскольку в этом случае появляется коллизия парадокса W-* W, из чего следует W= 0. Докажем (ii). Предположим, что в E существует базовый литерал І, такой что V= А + В. Тогда в соответствии с правилом (3) получаем A-* VwB-* V. В то же время при совмещении этих суждений с существующим в E суждением A-* В инициируется коллизия парадокса V-* V, из чего следует V=I. Конец доказательства.
Приложение Б. Частично упорядоченные множества
121
В более общем случае для формальных QC-структур соотношения теоремы 14 выполняются не во всех случаях из-за существования в них допустимых коллизий парадокса, но при определенных ограничениях их все же, видимо, можно применять. Точная формулировка этих ограничений в настоящее время автором не получена и предлагается читателю в качестве нерешенной проблемы.
Рассмотрим для QC-структур другой класс несравнимых пар литералов, для которых точное значение операции "умножения" неизвестно, но при этом существует хотя бы одна не равная 0 общая нижняя грань. Для таких пар литералов можно утверждать, что их "произведение" отличается от 0.
Теорема Б. 15. Если в СТ-замыкании QC-структуры Г пара (А, В)литералов содержится в некотором главном фильтре ZA, где L - базовый литерал Г, то для этой пары в Г существует отличающаяся от 0 нижняя грань.
Доказательство. Из определения ?Аясно, что литерал L предшествует одновременно А и В, из чего следует существование для них по крайней мере одной значимой нижней грани. Конец доказательства.
Теорема Б.16. Если в СТ-замыкании QC-структуры Г для пары элементов (А, В) выполняется Pred(A) л Pred(B) & 0, то для этой пары в Г существует отличающаяся от 0 нижняя грань.
Доказательство. Представим, что некоторый литерал W содержится в Pred(A) л Pred(B). Отсюда следует, что этот литерал предшествует одновременно литералам А и В. Конец доказательства.
Аналогичные утверждения можно сформулировать и для верхних границ. Эти утверждения ввиду их тривиальности приводятся без доказательств.
Теорема Б.17. Если в СТ-замыкании QC-структуры Г пара (А, В) литералов содержится в некотором главном идеале Lv, где L — базовыйлите-рал Г, то для этой пары в Г существует отличающаяся оті верхняя грань.
Теорема Б. 18. Если в СТ-замыкании QC-структуры Г выполняется Post(A) л Post(B) ^ 0, то для этой пары в Г существует отличающаяся от 1 верхняя грань.
С помощью теорем Б.15-Б.18 можно для каждой пары литералов найти множество всех верхних и нижних граней. Если эта пара литералов несравнима, то для интервальной оценки их "произведения" и суммы" необходимо среди литералов, являющихся верхними и нижними гранями этой пары, выбрать ближайшие грани. При этом следует учесть, что в QC-структурах в отличие от решеток допускается существование пар, не имеющих точных верхних или нижних граней, — это
122
Приложение Б. Частично упорядоченные множества
означает, что для каждой из этих пар найдется более одной ближайшей грани.
Рассмотрим схему алгоритма поиска ближайших нижних граней для произвольной пары (А, В) литералов. Для этого необходимо из всех главных фильтров структуры выбрать те, которые содержат множество {А, В), а из них — те, которые не вложены ни в один из других фильтров. Тогда ближайшей нижней гранью пары (А, В) будет литерал, являющийся инициатором любого главного фильтра, оставшегося в списке на последнем этапе алгоритма. Поиск ближайших верхних граней осуществляется аналогично на множестве главных идеалов структуры. Тем самым находятся все варианты интервальных оценок результатов соответствующих операций.
7. Соотношение между ОС-структурами и исчислением высказываний
В математической логике структура, во многом сходная с QC-струк-турами, была открыта более 30 лет назад [Кгот, 1967] и в некоторых источниках называется классом Крома формул первопорядковой логики. По определению класс Крома — это конъюнкция подформул типа (X V У), где X и Y — атомы или отрицания атомов, а V — обозначение дизъюнкции. Это определение можно сузить до формул исчисления высказываний. Тогда эквивалентным определением класса Крома будет такое: класс Крома — это формула исчисления высказываний типа KH Ф. в которой каждая дизъюнкция представлена не более чем двумя литералами.
В своей работе М. Кром доказал, что для формул этого класса задача выполнимости решается с помощью алгоритма полиномиальной сложности. Для доказательства этого утверждения вначале производится следующее преобразование.
Каждая формула Ф класса Крома преобразуется в ориентированный граф G(O), при этом каждой дизъюнкции типа X V Fb Ф соответствуют в С(Ф) две ориентированные дуги (~>Х — Y) и (-1F — X), а каждая дизъюнкция с единственным литералом X в Є(Ф) представлена дугой (—1X -* X) в С(Ф). После этого можно доказать следующее утверждение:
