Первый из кванторов называется квантором общности, так как он указывает на все объекты, существующие во вселенной («для всех ν,…»). Второй квантор называется квантором существования, так как он указывает на существование некоторого объекта (или объектов) («существует ν такой что…»). В качестве примера приведем формулу
all(X, мужчина(Х) -› человек(Х))
которая значит, что какое бы значение X мы не выбрали, если X является мужчиной, то тогда X – человек. Эту формулу можно прочитать так: для любого X, если X является мужчиной, то X является человеком. Или в более простой формулировке: каждый мужчина является человеком. Аналогично
exists(Z, отец(джон,2)& женщина(Z)))
значит, что существует объект, обозначаемый Z такой, что Джон является отцом Z и Z – женщина. Эту формулу можно прочитать так: существует Z такой, что Джон является отцом Z и Z – женщина. Или в более естественной формулировке: Джон имеет дочь. Ниже приведены две более сложные формулы исчисления предикатов:
all(X, животное(Х) -› exists(Y,мать(X,Y)))
all(X, формула_исчисления_предикатов(Х) ‹-› атомарная_формула(Х) # составная_формула(Х))
10.2. Приведение формул к стандартной форме
Как было показано в предыдущем разделе, формулы исчисления предикатов, записанные с использованием связок -› (импликация) и ‹-› (эквивалентность), могут быть переписаны лишь с использованием связок& (конъюнкция), # (дизъюнкция) и ~ (отрицание). В действительности, существует множество разных форм записи формул, и мы ни в коей мере не принесли бы в жертву выразительность формул, если бы должны были полностью отказаться от использования, например, #, -›, ‹-› и exists(X, P). Как следствие этой избыточности, существуют много различных способов записи одного и того же высказывания. При необходимости выполнять формальные преобразования формул исчисления предикатов это оказывается очень неудобным. Было бы значительно лучше, если бы все, что мы хотим сказать, можно было выразить единственным способом. Поэтому здесь будет рассмотрен способ преобразования формул исчисления предикатов к специальному виду – стандартной форме, - обладающему тем свойством, что число различных способов записи одного и того же утверждения меньше по сравнению с использованием других форм. В действительности будет показано, что высказывание исчисления предикатов, представленное в стандартной форме, очень похоже на некоторое множество утверждений языка Пролог. Так что исследование стандартной формы имеет существенное значение для понимания связи между Прологом и математической логикой. В приложении В будет коротко описана программа на Прологе, автоматически транслирующая формулы исчисления предикатов в стандартную форму.
Процесс приведения формулы исчисления предикатов к стандартной форме состоит из шести основных этапов.
Этап 1 - исключение импликаций и зквивалентностей
Процедура начинается с замены всех вхождений -› и ‹-› в соответствии с их определениями, данными в разд. 10.1. Так, например, формула
аll(Х,мужчина(Х) -› человек(Х))
будет преобразована в формулу
аll(Х,~мужчина(Х) # человек(Х))
Этап 2 - перенос отрицания внутрь формулы
На этом этапе обрабатываются случаи применения отрицания к формулам, не являющимся атомарными. Если такой случай имеет место, то формула переписывается по соответствующим правилам. Так, например, формула
~(человек (цезарь)& существующий (цезарь))
преобразуется в
~человек(цезарь) # существующий (цезарь)
а
~аll(Х, человек (X))
преобразуется в
exists(Х,~человек(Х))
Преобразования, выполняемые на втором этапе, основаны на следующих фактах:
~(α&β) значит то же самое, что и (~α) # (~β)
~exists(ν,ρ) значит то же самое, что и all(ν,~ρ)
~all(ν,ρ) значит то же самое, что и exists(ν,~ρ)
После завершения второго этапа каждое вхождение отрицания в формулу будет относиться лишь к атомарным подформулам. Атомарная формула или ее отрицание называется литералом. На всех последующих этапах литералы обрабатываются как единый элемент, а то, какие литералы представлены отрицанием, будет существенным лишь в самом конце.
Этап 3 - сколемизация
На следующем этапе удаляются кванторы существования. Это делается путем введения новых констант – сколемовских констант - вместо переменных связанных (введенных) квантором существования. Вместо того чтобы говорить, что существует объект, обладающий некоторым множеством свойств, можно ввести имя для такого объекта и просто сказать, что он обладает данными свойствами. Это соображение лежит в основе введения сколемовских констант. Сколемизация более существенно изменяет логические свойства формулы, чем все обсуждавшиеся ранее преобразования. Тем не менее, она обладает следующим важным свойством. Если имеется формула, то интерпретация, в которой эта формула истинна, существует тогда и только тогда, когда существует интерпретация, в которой истинна формула, полученная из первой в результате сколемизации. Такая форма эквивалентности формул вполне достаточна для наших целей. Так, например, формула
exists(X,женщина(X)& мать(Х,ева))
в результате сколемизации преобразуется в формулу
женщина(g1)& мать(g1, ева)
где g1 – некоторая новая константа, не использовавшаяся ранее. Константа g1 представляет некоторую женщину, мать которой есть Ева. То, что для обозначения константы использован символ» отличный от использовавшихся ранее, существенно, так как в высказывании ничего не говорится о том, что какой-то конкретный человек является дочерью Евы. В утверждении говорится лишь о том, что такой человек существует. Может оказаться, что g1 будет соответствовать тот же самый человек, который соответствует другой константе, но это уже дополнительная информация, никак не выраженная в высказывании.
Если формула содержит кванторы общности, то процедура сколемизации уже не столь проста. Например, если в формуле [17]
аll(Х, человек(Х) -› exists(Y,мать(X,Y)))
(«каждый человек имеет мать») заменить каждое вхождение переменной V, связанной квантором существования, на константу g2 и удалить квантор существования, то получится:
all(X, человек(Х) -› мать(X,g2))
Последнее высказывание говорит о том, что все люди имеют одну и ту же мать, обозначенную в формуле константой g2. Если в формуле есть переменные, введенные посредством кванторов общности, то при сколемизации необходимо вводить не константы, а составные термы (функциональные символы с множеством переменных аргументов) для того, чтобы отразить, как объект, о существовании которого идет речь, зависит от того, что обозначают переменные. Таким образом, при сколемизации предыдущего примера должно получиться
all(X, человек(Х) -› мать(Х, g2(Х)))
В этом случае функциональный символ g2 соответствует функции, которая каждому конкретному человеку ставит в соответствие его мать.
Этап 4 - вынесение кванторов общности в начало формулы
Этот этап очень прост. Каждый квантор общности просто выносится в начало формулы. Это не влияет на значение формулы. Так, например, формула
all(X, мужчина(Х) -› аll(Y,женщина(Y) -› нравится (X,Y)))
преобразуется в
аll(Х, аll(Y,мужчина(Х) -› (женщина(Y) -› нравится (X,Y))))
Так как теперь каждая переменная в этой формуле вводится посредством квантора общности, находящегося в начале формулы, то кванторы сами по себе не несут больше какой-либо дополнительной информации. Поэтому можно сократить формулу, опустив кванторы. Необходимо лишь помнить, что каждая переменная вводится посредством не указанного явно квантора, который опущен при записи формулы. Таким образом, формулу
аll(Х,живой(Х) # мертвый(Х)& аll(Y,нравится(мэри,Y) #грязный(Y))
теперь можно представить так:
(живой(Х) # мертвый(Х))& (нравится(мэри,Y) # грязный (Y))
Эта формула значит, что, какие бы X и Y ни были выбраны, либо X живой, либо X мертвый, и либо Мэри нравится Y, либо Y – грязный.
Этап 5 - использование дистрибутивных законов для & и #
На этом этапе исходная формула исчисления предикатов претерпела довольно много изменений. Формула больше не содержит в явном виде кванторов, а из логических связок в ней остались лишь & и # (помимо отрицания, входящего в состав литералов). Теперь формула преобразуется к специальному виду - конъюнктивной нормальной форме, характерной тем, что дизъюнктивные члены формулы не содержат внутри себя конъюнкцию. Таким образом, формулу можно преобразовать к такому виду, когда она будет представлять последовательность элементов, соединенных друг с другом конъюнкциями, а каждый элемент является либо литералом, либо состоит из нескольких литералов, соединенных дизъюнкцией. Чтобы привести формулу к такому виду, необходимо использовать следующие два тождества:
