та», то дворянство может менять основы власти и закона, а может этого и не делать. Всё равно сложное высказывание будет сохранять свою истинность. Если же мы потребуем, чтобы при ложности g всегда было бы ложным и все высказывание целиком, сохраняя остальные свойства импликации, то мы опять вернемся к конъюнкции.
Наверное, самым разумным с точки зрения здравого смысла было бы вообще отказаться от определения истинности или ложности выражения (ЕСЛИ ? ТОГДА ?), когда ? является ложным. Ибо для выводов в этом случае нет никакой информации. Во второй главе мы использовали знак выводимости
. Вот с его-то помощью и можно формализовать случай, когда в записи g
h из истинности g всегда следует истинность h , а при ложности g ничего сказать нельзя. Но знак выводимости не является логической связкой и не входит в синтаксис исчисления высказываний. Поэтому, оставаясь в рамках этого исчисления, мы вынуждены пользоваться импликацией.
И еще одно замечание, касающееся импликации. Эта связка, как и разделительная дизъюнкция, может быть сведена к комбинации других связок, имеющихся в исчислении. Читатели легко могут убедиться в справедливости замены ?
? на
?
?. Однако по ряду причин в исчислении высказываний в его классической форме импликация сохраняется как самостоятельная связка.
Не нужно думать, что переход от фраз на естественном языке к соответствующим им правильным формулам исчисления высказываний столь прост. На этом пути стоит немало трудностей, И прежде всего потому, что частицы и союзы языка типа НЕ, И, ИЛИ, ТО, ЕСЛИ и т.п. не являются однозначными свидетельствами наличия похожих на них связок. Цитата из стихотворения «Смерть поэта» Д. Самойлова иллюстрирует это положение:
И не ведал я, было ли это
Отпеванием времени года,
Воспеваньем страны и народа
Или просто кончиной поэта.
Встречающиеся здесь И и ИЛИ не являются прямыми аналогами связок исчисления высказываний.
Мы ввели множество базовых элементов и множество синтаксических правил. Теперь необходимо ввести множество аксиом. В логике в качестве множества аксиом выбирают обычно совокупность правильных формул, которые являются общезначимыми (или тождественно истинными ). Высказывания, описываемые этими формулами, таковы, что они всегда истинны. Вот пример такого множества формул:
Читатели могут сами убедиться в том, что при всех комбинациях истинности и ложности формул ?, ? и ? четыре выписанные аксиомы всегда являются истинными. Такие аксиомы принято называть абсолютными или логическими .
Перейдем к описанию правил вывода R . Вспомним, что Аристотель, создавая свои силлогистические правила, добивался того, чтобы из истинных посылок всегда следовали истинные заключения. Если в качестве аксиом используются абсолютные аксиомы, то правила вывода должны обладать тем свойством, что их применение не должно нарушать истинность. Другими словами, из тождественно истинных формул должны выводиться лишь тождественно истинные формулы. Введем, учитывая это, два правила вывода исчисления высказываний.
Первое правило носит название правило подстановки . Согласно ему в формулу, которая уже выведена, можно вместо некоторого высказывания подставить любое другое при непременном условии, что эта подстановка сделана во всех местах вхождения заменяемого высказывания в данную формулу. Такая подстановка сохраняет свойство формулы быть тождественно истинной. Если в аксиому (?
(?
?)) вместо ? подставить любую формулу, например (?&?), то формула ((?&?)
((?&?)
?)) останется тождественно истинной, что легко доказывается перебором всех комбинаций истинностных значений ? и ? и проверкой того, что для всех них полученная формула остается истинной.
Второе правило называется модус поненс (лат. modus ponens) или правило заключения и выглядит следующим образом: если ? и (?
?) являются истинными формулами, то формула ? также истинна. Если ? является истинной, то истинность (?
?) означает, что ? является истинной. Поэтому правило заключения не портит истинности выводимых формул.
Мы полностью описали исчисление высказываний. Заметим еще раз, что оно устроено так, что в результате выводов из аксиом получаются лишь тождественно истинные формулы. Можно показать, что система логических аксиом может быть выбрана таким образом, что для любой тождественно истинной формулы всегда найдется цепочка выводов (логических рассуждений), с помощью которой она будет выведена из системы аксиом путем применения правил подстановки и заключения. Другими словами, может быть построена полная система аксиом, из которой будут выводиться все тождественно истинные формулы и только они. Как показали исследования логиков, таких полных систем аксиом существует много. Система из четырех аксиом, которую мы только что рассмотрели является полной. Ее предложил известный немецкий математик и логик Д. Гильберт.
Подобное свойство исчисления высказываний позволяет достаточно легко ответить на кардинальный вопрос, возникающий для любой формальной системы: принадлежит ли некоторая правильная формула к множеству формул, выводимых в данной формальной системе? Для ответа на этот вопрос надо построить таблицу, в которой в левой части перечислены все возможные комбинации значений истины и лжи для высказываний, входящих в эту формулу (легко видеть, что при n различных таких высказываниях число комбинаций будет равно 2n ), а в правой части выписаны значения истинности проверяемой формулы. Если правый столбец состоит только из значений «истина», то формула выводима в исчислении высказываний. В противном случае ее выводимость не имеет места.
Пусть, например, надо узнать, выводима ли в исчислении высказываний формула ((
?
?)
?). В эту формулу входит одно высказывание ?. Поэтому нужно проверить лишь две комбинации истинности: когда ? истинно и когда оно ложно. В первом случае по свойству импликации первая скобка является истинной, ибо
? ложно. Но тогда истинна и вся формула, ибо импликация истинна, когда истинны ее левая и правая части. Если же ? ложно, то первая скобка является ложной, так как левая часть импликации (
?
?) истинна, а правая ложна. Но тогда вся формула является истинной. Тем самым доказано, что интересующая нас формула является тождественно истинной и, следовательно, выводимой в исчислении высказываний.
О чем все это говорит? Прежде всего о том, что процедура выводимости в исчислении высказываний конструктивно разрешима. Проверка общезначимости (тождественной истинности) формулы сводится к построению нужной конечной таблицы и перебору всех вариантов, содержащихся в ее левой части, с целью определения истинностного значения проверяемой формулы. Получение первого значения «ложь» свидетельствует о невыводимости. Если же при всех комбинациях, перечисленных в левой части таблицы, формула принимает значение «истина», то она выводима с помощью описанных выше двух правил вывода из той или иной полной системы абсолютных аксиом.
Проиллюстрируем эту процедуру еще на одном примере. Проверим, является ли выводимой формула ((?
?)
((
?
?)&?)). В этой формуле (будем обозначать ее ?) имеется три высказывания, что приводит к необходимости рассмотрения истинного значения ? на 23=8 комбинациях. Эти комбинации и соответствующие шаги по определению истинностного значения ? на них даны в табл. 3, в которой И и Л означают соответственно значения «истина» и «ложь».
Таблица 3
Появление в пятой строке в столбце ? значения Л свидетельствует о невыводимости исследуемой формулы. На этом шаге процесс вывода можно прекратить. Остальные строки в таблице приведены лишь для полноты картины.
«Логик-теоретик»
Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ?1 и ?2 равны между собой, и записывать этот факт обычным образом ?1=?2, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ?1 и ?2 одинакова.
Появление знака равенства, которого не было в исчислении высказываний, не должно нас смущать. Его легко можно исключить из рассмотрения, введя формулу ((?1&?2)
(
?1&
?2)). Читатели могут проверить, что эта формула будет истинной только в том случае, когда оценки истинности ?1 и ?2 одинаковы. Тогда утверждение, что ?1=?2, становится эквивалентным утверждению, что формула ((?1&?2)
(
?1&
?2)) является истинной.
«Логик-теоретик» должен был доказывать справедливость утверждений вида ?1=?2 для различных ?1 и ?2. Однако авторы «Логика-теоретика» не пошли по прямому пути. Не стали строить таблицы для ?1 и ?2 и проверять совпадение истинности ?1 и ?2 на всех возможных интерпретациях истинности их аргументов. Ведь с ростом числа аргументов n число строк в этих таблицах растет как 2n . А. Ньюэлл и Г. Саймон пошли по пути приближения процедуры доказательства к тому, как это делают люди.
В основу процесса доказательства они положили идею ликвидации различий в формульной записи ?1 и ?2. Авторы программы составили перечень из шести различий.
1. В ?1 и ?2 различное число членов в формулах. Например, ?1=?
?, а ?2=?
?.
2. В ?1 и ?2 имеется различие в основной связке (т.е. в связке, которая выполняется последней). Например, ?1=(??)
(
), а ?2=(?
)
?.
3. Перед всем выражением для ?1(?2) стоит знак отрицания, а перед ?2(?1) его нет. Например, ?1=
(?
?), а ?2=??.
4. Аналогичное различие, но оно касается не всего выражения для ?i (i =1,2), а некоторого его подвыражения.
5. Скобки в ?1 расставлены не так, как в ?2. Например, ?1=?
(?
?), а ?2=(?
?)
?.
6. Записи для ?1 и ?2 отличаются порядком следования подвыражений. Например, ?1=(??)
?, а ?2=?
(??).
Для того чтобы иметь возможность ликвидировать подобные различия, используются 12 преобразований формул исчисления высказываний. Первые семь преобразований носят тождественный характер, т.е. не меняют истинного значения преобразуемых формул. Последние пять верны только при условии, что левая часть их является тождественно истинной (T -выражением).
В преобразованиях использованы большие латинские буквы, которые могут соответствовать любым подвыражениям формул ?1 и ?2. Стрелки
и
показывают направление преобразований. (Знак
есть по сути знак
.)
С помощью этих преобразований можно устранять различия между ?1 и ?2, которые мы перечислили выше. Укажем в специальной табл. 4 классы преобразований F 1, которые можно использовать для устранения различий. Первое различие разделено на два: различие 1’ требует добавления выражений в формулу, а различие 1’’ – вычеркивания из формулы лишних выражений.
Таблица 4
Крестики поставлены там, где можно устранить различие с помощью соответствующего преобразования.
Покажем работу программы «Логик-теоретик» на несложном примере. Пусть требуется доказать равенство ?1=?2, имеющее вид
Применим к ?1 первое преобразование из F 7 справа налево. Выбор F 7 определяется различием ?1 и ?2. Из ?1 необходимо убрать лишнее подвыражение С , которого нет в ?2. После этого получим
Поскольку в ?1 осталось еще выражение С , которого нет справа, то снова фиксируется различие 1’’ и ищется подходящее преобразование. Таким преобразованием является четвертое из F 7. Но для его применения надо сначала использовать преобразование F 1 для устранения различия 6. После этого, применяя четвертое преобразование из F 7, получаем
Теперь можно применить второе преобразование из F 7:
Четвертое преобразование из F 7 приводит к окончательному результату
Пример, конечно, не отражает всех особенностей работы программы «Логик-теоретик». Мы несколько упростили задачу. Как видно из таблицы различий, выбор преобразования на каждом шаге далеко не однозначен. В формулах могут существовать одновременно несколько различий, а для ликвидации различия можно использовать несколько преобразований. Всякий вывод, как бы он не был организован, носит переборный характер. И успешность того или иного выбора преобразования не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода.
Исчисление предикатов
Исчисление высказываний не позволяет описывать дедуктивные рассуждения всех типов, в частности силлогистические умозаключения. Оно слишком бедно выразительными средствами.
Его естественным развитием является исчисление предикатов. Как и исчисление высказываний, исчисление предикатов представляет собой формальную систему. Мы не будем описывать его в такой строгой форме (любители строгости могут найти подобные описания в литературе к данному разделу), а попытаемся оставаться на содержательном уровне описания.
Под предикатом будем понимать некоторую связь, заданную на наборе из констант или переменных, например утверждение «? больше ? ». Если семантика ? и ? не задана, то о предикате сказать особенно нечего. Пожалуй, только то, что он задает двуместное отношение, семантика которого такова, что оно является антирефлексивным (неверно, что «? больше ? »), асимметричным и транзитивным. Но при задании семантики (т.е. областей определения переменных ? и ? ) о предикате можно будет сказать существенно больше. Если ? и ? – площади городов соответственно в СССР и Японии, то при задании списков городов и означивании переменных константами мы получим отношение между двумя высказываниями типа «Площадь Вологды больше площади Токио» или «Площадь Ленинграда больше площади Нары». После этого становится возможным говорить об истинности или ложности предиката. Для нашего примера первое означивание дает ложное значение предиката, а второе – истинное. Иногда для утверждения об истинности или ложности предиката можно обойтись и без означивания. Например, если областью определения х являются целые положительные числа, то предикат «х больше ?5» будет тождественно истинен.
В исчислении предикатов используются те же операции, что и в исчислении высказываний. С их помощью образуются предикатные формулы. Будем обозначать предикаты большими латинскими буквами. Примерами предикатных формул могут служить Р (х ,у )&Q (a ,b ) или
P (? )
P (z ,l ).
В исчислении предикатов используются два квантора: квантор общности и квантор существования . Первый обозначается как
, а запись
xP (x ) эквивалентна утверждению «Для всех х из области его определения имеет место Р (х )». Второй квантор обозначается как
, а запись
хР (х ) эквивалентна утверждению «Найдется по крайней мере один х * в области определения х , такой, что истинен Р (х *)». Переменные, находящиеся в сфере действия кванторов, называются связанными , остальные переменные – свободными .
Вспомним И.А. Крылова: «А вы, друзья, как ни садитесь, все ж в музыканты не годитесь!». Обозначим через Р(х ,у ) предикат, который связывает между собой способ рассаживания участников квартета и качество исполняемой ими музыки. Предикат Р (х ,у ) становится истинным лишь тогда, когда найдено такое взаимное расположение зверей в квартете, что качество музыки позволяет назвать исполнителей музыкантами. При этих условиях цитате из басни «Квартет» соответствует формула
x
P(x ,у ).
А вот Ф. Тютчев: «Бывают роковые дни лютейшего телесного недуга и страшных нравственных тревог…». Если Q (u ,v ) есть предикат, в котором переменная u определена на множестве дней, а переменная v на области настроений, связанных с «телесным недугом» и «страшными нравственными тревогами», то в исчислении предикатов началу стихотворения Тютчева будет соответствовать формула
uQ (u ,v ).
Отметим, что имеют место следующие соотношения:
Справедливость их вытекает из смысла кванторов. Они позволяют любую формулу в исчислении предикатов представить в виде предваренной нормальной формы (ПНФ). В ней сначала выписываются все кванторы, а затем предикатные выражения. Например, формула
записана в ПНФ.
Введение кванторов
и
, а также их отрицаний наводит на мысль о связи исчисления предикатов и силлогистики Аристотеля. Вспомним еще раз смысл кванторов, использованных в силлогистике: Asp – «Всякое s есть р »; Esp – «Ни одно s не есть р », Isp – «Некоторые s есть р » и Osp – «Некоторые s не есть р ». Представляется вполне справедливым заменить эти выражения силлогистики следующими четырьмя формулами исчисления предикатов:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
Наверное, самым разумным с точки зрения здравого смысла было бы вообще отказаться от определения истинности или ложности выражения (ЕСЛИ ? ТОГДА ?), когда ? является ложным. Ибо для выводов в этом случае нет никакой информации. Во второй главе мы использовали знак выводимости
. Вот с его-то помощью и можно формализовать случай, когда в записи g
h из истинности g всегда следует истинность h , а при ложности g ничего сказать нельзя. Но знак выводимости не является логической связкой и не входит в синтаксис исчисления высказываний. Поэтому, оставаясь в рамках этого исчисления, мы вынуждены пользоваться импликацией.
И еще одно замечание, касающееся импликации. Эта связка, как и разделительная дизъюнкция, может быть сведена к комбинации других связок, имеющихся в исчислении. Читатели легко могут убедиться в справедливости замены ?
? на
?
?. Однако по ряду причин в исчислении высказываний в его классической форме импликация сохраняется как самостоятельная связка.
Не нужно думать, что переход от фраз на естественном языке к соответствующим им правильным формулам исчисления высказываний столь прост. На этом пути стоит немало трудностей, И прежде всего потому, что частицы и союзы языка типа НЕ, И, ИЛИ, ТО, ЕСЛИ и т.п. не являются однозначными свидетельствами наличия похожих на них связок. Цитата из стихотворения «Смерть поэта» Д. Самойлова иллюстрирует это положение:
И не ведал я, было ли это
Отпеванием времени года,
Воспеваньем страны и народа
Или просто кончиной поэта.
Встречающиеся здесь И и ИЛИ не являются прямыми аналогами связок исчисления высказываний.
Мы ввели множество базовых элементов и множество синтаксических правил. Теперь необходимо ввести множество аксиом. В логике в качестве множества аксиом выбирают обычно совокупность правильных формул, которые являются общезначимыми (или тождественно истинными ). Высказывания, описываемые этими формулами, таковы, что они всегда истинны. Вот пример такого множества формул:
Читатели могут сами убедиться в том, что при всех комбинациях истинности и ложности формул ?, ? и ? четыре выписанные аксиомы всегда являются истинными. Такие аксиомы принято называть абсолютными или логическими .
Перейдем к описанию правил вывода R . Вспомним, что Аристотель, создавая свои силлогистические правила, добивался того, чтобы из истинных посылок всегда следовали истинные заключения. Если в качестве аксиом используются абсолютные аксиомы, то правила вывода должны обладать тем свойством, что их применение не должно нарушать истинность. Другими словами, из тождественно истинных формул должны выводиться лишь тождественно истинные формулы. Введем, учитывая это, два правила вывода исчисления высказываний.
Первое правило носит название правило подстановки . Согласно ему в формулу, которая уже выведена, можно вместо некоторого высказывания подставить любое другое при непременном условии, что эта подстановка сделана во всех местах вхождения заменяемого высказывания в данную формулу. Такая подстановка сохраняет свойство формулы быть тождественно истинной. Если в аксиому (?
(?
?)) вместо ? подставить любую формулу, например (?&?), то формула ((?&?)
((?&?)
?)) останется тождественно истинной, что легко доказывается перебором всех комбинаций истинностных значений ? и ? и проверкой того, что для всех них полученная формула остается истинной.
Второе правило называется модус поненс (лат. modus ponens) или правило заключения и выглядит следующим образом: если ? и (?
?) являются истинными формулами, то формула ? также истинна. Если ? является истинной, то истинность (?
?) означает, что ? является истинной. Поэтому правило заключения не портит истинности выводимых формул.
Мы полностью описали исчисление высказываний. Заметим еще раз, что оно устроено так, что в результате выводов из аксиом получаются лишь тождественно истинные формулы. Можно показать, что система логических аксиом может быть выбрана таким образом, что для любой тождественно истинной формулы всегда найдется цепочка выводов (логических рассуждений), с помощью которой она будет выведена из системы аксиом путем применения правил подстановки и заключения. Другими словами, может быть построена полная система аксиом, из которой будут выводиться все тождественно истинные формулы и только они. Как показали исследования логиков, таких полных систем аксиом существует много. Система из четырех аксиом, которую мы только что рассмотрели является полной. Ее предложил известный немецкий математик и логик Д. Гильберт.
Подобное свойство исчисления высказываний позволяет достаточно легко ответить на кардинальный вопрос, возникающий для любой формальной системы: принадлежит ли некоторая правильная формула к множеству формул, выводимых в данной формальной системе? Для ответа на этот вопрос надо построить таблицу, в которой в левой части перечислены все возможные комбинации значений истины и лжи для высказываний, входящих в эту формулу (легко видеть, что при n различных таких высказываниях число комбинаций будет равно 2n ), а в правой части выписаны значения истинности проверяемой формулы. Если правый столбец состоит только из значений «истина», то формула выводима в исчислении высказываний. В противном случае ее выводимость не имеет места.
Пусть, например, надо узнать, выводима ли в исчислении высказываний формула ((
?
?)
?). В эту формулу входит одно высказывание ?. Поэтому нужно проверить лишь две комбинации истинности: когда ? истинно и когда оно ложно. В первом случае по свойству импликации первая скобка является истинной, ибо
? ложно. Но тогда истинна и вся формула, ибо импликация истинна, когда истинны ее левая и правая части. Если же ? ложно, то первая скобка является ложной, так как левая часть импликации (
?
?) истинна, а правая ложна. Но тогда вся формула является истинной. Тем самым доказано, что интересующая нас формула является тождественно истинной и, следовательно, выводимой в исчислении высказываний.
О чем все это говорит? Прежде всего о том, что процедура выводимости в исчислении высказываний конструктивно разрешима. Проверка общезначимости (тождественной истинности) формулы сводится к построению нужной конечной таблицы и перебору всех вариантов, содержащихся в ее левой части, с целью определения истинностного значения проверяемой формулы. Получение первого значения «ложь» свидетельствует о невыводимости. Если же при всех комбинациях, перечисленных в левой части таблицы, формула принимает значение «истина», то она выводима с помощью описанных выше двух правил вывода из той или иной полной системы абсолютных аксиом.
Проиллюстрируем эту процедуру еще на одном примере. Проверим, является ли выводимой формула ((?
?)
((
?
?)&?)). В этой формуле (будем обозначать ее ?) имеется три высказывания, что приводит к необходимости рассмотрения истинного значения ? на 23=8 комбинациях. Эти комбинации и соответствующие шаги по определению истинностного значения ? на них даны в табл. 3, в которой И и Л означают соответственно значения «истина» и «ложь».
Таблица 3
Появление в пятой строке в столбце ? значения Л свидетельствует о невыводимости исследуемой формулы. На этом шаге процесс вывода можно прекратить. Остальные строки в таблице приведены лишь для полноты картины.
«Логик-теоретик»
Так была названа программа для ЭВМ, созданная в середине шестидесятых годов американским кибернетиком А. Ньюэллом в содружестве с психологом Г. Саймоном. Она была предназначена для доказательства теорем в исчислении высказываний, т.е. для поиска обоснования тождественной истинности некоторых утверждений. Для того чтобы перейти к описанию программы «Логик-теоретик», введем предварительно понятие о равенстве двух выражений исчисления высказываний. Будем говорить, что выражения ?1 и ?2 равны между собой, и записывать этот факт обычным образом ?1=?2, если на всех возможных наборах интерпретации истинности входящих в них элементарных высказываний истинность ?1 и ?2 одинакова.
Появление знака равенства, которого не было в исчислении высказываний, не должно нас смущать. Его легко можно исключить из рассмотрения, введя формулу ((?1&?2)
(
?1&
?2)). Читатели могут проверить, что эта формула будет истинной только в том случае, когда оценки истинности ?1 и ?2 одинаковы. Тогда утверждение, что ?1=?2, становится эквивалентным утверждению, что формула ((?1&?2)
(
?1&
?2)) является истинной.
«Логик-теоретик» должен был доказывать справедливость утверждений вида ?1=?2 для различных ?1 и ?2. Однако авторы «Логика-теоретика» не пошли по прямому пути. Не стали строить таблицы для ?1 и ?2 и проверять совпадение истинности ?1 и ?2 на всех возможных интерпретациях истинности их аргументов. Ведь с ростом числа аргументов n число строк в этих таблицах растет как 2n . А. Ньюэлл и Г. Саймон пошли по пути приближения процедуры доказательства к тому, как это делают люди.
В основу процесса доказательства они положили идею ликвидации различий в формульной записи ?1 и ?2. Авторы программы составили перечень из шести различий.
1. В ?1 и ?2 различное число членов в формулах. Например, ?1=?
?, а ?2=?
?.
2. В ?1 и ?2 имеется различие в основной связке (т.е. в связке, которая выполняется последней). Например, ?1=(??)
(
), а ?2=(?
)
?.
3. Перед всем выражением для ?1(?2) стоит знак отрицания, а перед ?2(?1) его нет. Например, ?1=
(?
?), а ?2=??.
4. Аналогичное различие, но оно касается не всего выражения для ?i (i =1,2), а некоторого его подвыражения.
5. Скобки в ?1 расставлены не так, как в ?2. Например, ?1=?
(?
?), а ?2=(?
?)
?.
6. Записи для ?1 и ?2 отличаются порядком следования подвыражений. Например, ?1=(??)
?, а ?2=?
(??).
Для того чтобы иметь возможность ликвидировать подобные различия, используются 12 преобразований формул исчисления высказываний. Первые семь преобразований носят тождественный характер, т.е. не меняют истинного значения преобразуемых формул. Последние пять верны только при условии, что левая часть их является тождественно истинной (T -выражением).
В преобразованиях использованы большие латинские буквы, которые могут соответствовать любым подвыражениям формул ?1 и ?2. Стрелки
и
показывают направление преобразований. (Знак
есть по сути знак
.)
С помощью этих преобразований можно устранять различия между ?1 и ?2, которые мы перечислили выше. Укажем в специальной табл. 4 классы преобразований F 1, которые можно использовать для устранения различий. Первое различие разделено на два: различие 1’ требует добавления выражений в формулу, а различие 1’’ – вычеркивания из формулы лишних выражений.
Таблица 4
Крестики поставлены там, где можно устранить различие с помощью соответствующего преобразования.
Покажем работу программы «Логик-теоретик» на несложном примере. Пусть требуется доказать равенство ?1=?2, имеющее вид
Применим к ?1 первое преобразование из F 7 справа налево. Выбор F 7 определяется различием ?1 и ?2. Из ?1 необходимо убрать лишнее подвыражение С , которого нет в ?2. После этого получим
Поскольку в ?1 осталось еще выражение С , которого нет справа, то снова фиксируется различие 1’’ и ищется подходящее преобразование. Таким преобразованием является четвертое из F 7. Но для его применения надо сначала использовать преобразование F 1 для устранения различия 6. После этого, применяя четвертое преобразование из F 7, получаем
Теперь можно применить второе преобразование из F 7:
Четвертое преобразование из F 7 приводит к окончательному результату
Пример, конечно, не отражает всех особенностей работы программы «Логик-теоретик». Мы несколько упростили задачу. Как видно из таблицы различий, выбор преобразования на каждом шаге далеко не однозначен. В формулах могут существовать одновременно несколько различий, а для ликвидации различия можно использовать несколько преобразований. Всякий вывод, как бы он не был организован, носит переборный характер. И успешность того или иного выбора преобразования не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы прежде, чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода – центральная проблема всех автоматизированных систем дедуктивного вывода.
Исчисление предикатов
Исчисление высказываний не позволяет описывать дедуктивные рассуждения всех типов, в частности силлогистические умозаключения. Оно слишком бедно выразительными средствами.
Его естественным развитием является исчисление предикатов. Как и исчисление высказываний, исчисление предикатов представляет собой формальную систему. Мы не будем описывать его в такой строгой форме (любители строгости могут найти подобные описания в литературе к данному разделу), а попытаемся оставаться на содержательном уровне описания.
Под предикатом будем понимать некоторую связь, заданную на наборе из констант или переменных, например утверждение «? больше ? ». Если семантика ? и ? не задана, то о предикате сказать особенно нечего. Пожалуй, только то, что он задает двуместное отношение, семантика которого такова, что оно является антирефлексивным (неверно, что «? больше ? »), асимметричным и транзитивным. Но при задании семантики (т.е. областей определения переменных ? и ? ) о предикате можно будет сказать существенно больше. Если ? и ? – площади городов соответственно в СССР и Японии, то при задании списков городов и означивании переменных константами мы получим отношение между двумя высказываниями типа «Площадь Вологды больше площади Токио» или «Площадь Ленинграда больше площади Нары». После этого становится возможным говорить об истинности или ложности предиката. Для нашего примера первое означивание дает ложное значение предиката, а второе – истинное. Иногда для утверждения об истинности или ложности предиката можно обойтись и без означивания. Например, если областью определения х являются целые положительные числа, то предикат «х больше ?5» будет тождественно истинен.
В исчислении предикатов используются те же операции, что и в исчислении высказываний. С их помощью образуются предикатные формулы. Будем обозначать предикаты большими латинскими буквами. Примерами предикатных формул могут служить Р (х ,у )&Q (a ,b ) или
P (? )
P (z ,l ).
В исчислении предикатов используются два квантора: квантор общности и квантор существования . Первый обозначается как
, а запись
xP (x ) эквивалентна утверждению «Для всех х из области его определения имеет место Р (х )». Второй квантор обозначается как
, а запись
хР (х ) эквивалентна утверждению «Найдется по крайней мере один х * в области определения х , такой, что истинен Р (х *)». Переменные, находящиеся в сфере действия кванторов, называются связанными , остальные переменные – свободными .
Вспомним И.А. Крылова: «А вы, друзья, как ни садитесь, все ж в музыканты не годитесь!». Обозначим через Р(х ,у ) предикат, который связывает между собой способ рассаживания участников квартета и качество исполняемой ими музыки. Предикат Р (х ,у ) становится истинным лишь тогда, когда найдено такое взаимное расположение зверей в квартете, что качество музыки позволяет назвать исполнителей музыкантами. При этих условиях цитате из басни «Квартет» соответствует формула
x
P(x ,у ).
А вот Ф. Тютчев: «Бывают роковые дни лютейшего телесного недуга и страшных нравственных тревог…». Если Q (u ,v ) есть предикат, в котором переменная u определена на множестве дней, а переменная v на области настроений, связанных с «телесным недугом» и «страшными нравственными тревогами», то в исчислении предикатов началу стихотворения Тютчева будет соответствовать формула
uQ (u ,v ).
Отметим, что имеют место следующие соотношения:
Справедливость их вытекает из смысла кванторов. Они позволяют любую формулу в исчислении предикатов представить в виде предваренной нормальной формы (ПНФ). В ней сначала выписываются все кванторы, а затем предикатные выражения. Например, формула
записана в ПНФ.
Введение кванторов
и
, а также их отрицаний наводит на мысль о связи исчисления предикатов и силлогистики Аристотеля. Вспомним еще раз смысл кванторов, использованных в силлогистике: Asp – «Всякое s есть р »; Esp – «Ни одно s не есть р », Isp – «Некоторые s есть р » и Osp – «Некоторые s не есть р ». Представляется вполне справедливым заменить эти выражения силлогистики следующими четырьмя формулами исчисления предикатов:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22