Автор: Метакидес Г. Нероуд А.
Теги: вычислительная математика численный анализ математика программирование математическая логика логическое программирование
ISBN: 5-88688-037-2
Год: 1998
Текст
STUDIES IN COMPUTER SCIENCE 1
AND ARTIFICIAL INTELLIGENCE ■
PRINCIPLES OF LOGIC
AND LOGIC PROGRAMMING
G. METAKIDES
European Commission
Brussels, Belgium
A. NERODE
Mathematical Sciences Institute
Cornell University
Ithaca, NY, USA
With the cooperation of
A. SINACHOPOULOS
Universite Libre de Bruxelles
Belgium
1996
ELSEVIER
AMSTERDAM - LAUSANNE - NEW YORK - OXFORD - SHANNON - TOKYO
.- U,г
ПМЕТАКИДЕС
А. НЕРОУД
ПРИНЦИПЫ ЛОГИКИ
И ЛОГИЧЕСКОГО
ПРОГРАММИРОВАНИЯ
Перевод с английского
;, В. А. Захарова, •'■ ^
С.:Щт Селезневой и В. В. Спанупол<Х$
)■■-■■ ' *.
под редакцией
В. А* Садовничего и В. А. Захарова
V 1'.,
ИЗДАТЕЛЬСТВО «ФАКТОРИАЛ» »»s «»•
^^ МОСКВА, 1998
ББК 22.19 ~r"\ , , * Издание осуществлено по инициа-
М 54 ■ j ;, ^ ., тиве и при поддержке Московско-
УДК 519.68 " - 'го государственного университе-
университета им. М. В. Ломоносова
f < *■ у г -
М 54 Метакидес Г., Нероуд А. Принципы логики и логическое
программирование / Пер. с англ. под ред. к.ф.м.н В. А. Захаро-
Захарова и акад. В. А. Садовничего. — М.: Изд-во «Факториал», 1998.—
288 с. — ISBN 5-88688-037-2.
Книга известных специалистов в области математической логики и логического
программирования (Греция, США). Излагаются основные понятия и принципы ма-
математической логики. Основное внимание уделяется вопросам применения языка
математической логики для представления знаний и формальным методам доказа-
доказательства теорем с использованием семантических таблиц и резолютивного вывода.
На примере языка ПРОЛОГ рассматриваются принципы логического программи-
программирования. Подробно анализируется механизм вычислений и методика проектиро-
проектирования логических программ. Изложение отличается методическими достоинства-
достоинствами — книга написана в хорошем стиле, не требует специальных предварительных
знаний, содержит большое количество примеров и задач.
Может быть рекомендована в качестве учебного пособия для программистов
разной квалификации, специалистов по искусственному интеллекту и для всех
интересующихся математической логикой, а также теорией и практикой логиче-
логического программирования.
л '' -ч-х 'Лиг, :> O'-vv^i-iYy
Научное издание , , ,. ,. , <.. ('■_ ).\
Метакидес Г., Нероуд А.
Принципы логики и логического программирования - '■•■■
Формат 60 х 90/16. Гарнитура литературная. Усл. печ. л. 18. Подписано к печа-
печати 12.9.1998. Тираж 1000 экз.
Издательство «Факториал», 117449, Москва, а/я 331; J1P № 063537 от 22.07.1994.
Оригинал-макет подготовлен с использованием макропакета АР-Т^Х.
Отпечатано с готовых диапочитивов в ППП «Типография «Наука»
I21U99 Москва, Шубинский пер., 6. Заказ 31
ISBN 0-444-81644-5 Copyright © 1996 by © Изд-во Элсивер,
(англ.) Elsiver Science 1996
ISBN 5-88688-037-2 Translation Copyright © 1998 МГУ, пер.
(русск.) ©1998 by Moscow на русск. яз., 1998
St. University.
All rights reserved. Все права защищены.
,« ; f ПРЕДИСЛОВИЕ К РУССКОМУ ИЗДАНИЮ
Мне доставляет удовольствие представить российским читателям
новый учебник, написанный всемирно известными американскими
математиками, профессором Корнельского университета, Анилом
Нероудом совместно с признанным специалистом в области логиче-
логического программирования, профессором Георгием Метакидесом. Соз-
Созданная ими книга весьма необычна, и поэтому нуждается в кратком
предисловии, поясняющем некоторые ее замечательные особенно-
особенности.
До недавнего времени математическая логика не выходила за пре-
пределы «чистой» математики и обеспечивала только корректность по-
построения математических теорий. Традиционно считалось, что пол-
полноценное изучение этой математической дисциплины целесообраз-
целесообразно начинать лишь тогда, когда объем и разнообразие математиче-
математических знаний учащихся потребуют их упорядочения для того, что-
чтобы осмыслить структуру и принципы устройства всей математики.
Поэтому значительная часть учебников по математической логики
изначально ориентированы на круг читателей, имеющих достаточно
высокую математическую подготовку и свободно владеющих фор-
формальным аппаратом современной математики. Вполне естественно,
что при таких условиях круг людей, знакомых с методами мате-
математической логики, ограничивался выпускниками математических
факультетов.
Но с течением лет положение дел сильно изменилось. По ме-
мере развития информатики, математическая логика раскрыла свой
огромным потенциал практического применения. Совершенствова-
Совершенствование вычислительной техники и ее математического обеспечения
привело к тому, что круг задач, для решения которых можно исполь-
использовать компьютеры, существенно расширился. Стало ясно, что вы-
вычислительные машины можно применять не только для численных
расчетов и чисто математических или статистических исследова-
исследований, но и для обработки информации и знаний самого разного рода.
Возникла потребность в разработке такого языка общения с компь-
компьютером, который позволял бы человеку наиболее естественным и
удобным способом представлять знания, относящиеся к произволь-
произвольным областям деятельности, и в создании таких методов обработки
данных, которые позволяли бы компьютеру извлекать новые сведе-
сведения и давать ответы на вопросы исходя из имеющихся знаний.
Проведенные исследования показали, что для этой цели лучше
всего подходит язык математической логики. Подобно тому, как но-
новые математические теоремы доказываются на основе изначальных
аксиом и ранее доказанных теорем, новые знания о предметной об-
области могут быть извлечены из накопленных знаний чисто автомати-
автоматически при помощи логических методов вывода. Совершенствование
аппарата логического вывода привело к созданию нового направле-
направления в программировании — логического программирования. Логи-
Логическое программирование изменило устоявшиеся представления о
ПРЕДИСЛОВИЕ
технологии проектирования компьютерных программ. В самом об-
общем виде логическая программа представляет собой собрание све-
сведений о предметной области решаемой задачи, записанных на язы-
языке, приближенным к естественному языку человеческого общения.
Обращаясь к программе с запросами, пользователь может получать
все возможные ответы, логически вытекающие из той совокупности
знаний, которыми располагает логическая программа. Чем полнее
и детальнее будет описание области знаний, к которой относится
решаемая задача, тем точнее будут ответы на поставленные вопро-
вопросы. Диалог программы с пользователем теперь становится похожим
на обычную беседу учителя с послушным и аккуратным учеником:
учитель наделяет ученика знаниями, а ученик, опираясь на эти зна-
знания, безошибочно решает задачи и отвечает на вопросы. Поэтому
в логическом программировании для решения поставленной зада-
задачи нужно всего лишь как можно точнее и детальнее описать, что
именно требуется решить. Если решение задачи существует, то в
этом случае компьютер самостоятельно «догадается», как достичь
искомого решения. Логическое программирование открывает новые
возможности использования компьютера. Теперь мы можем общать-
общаться с ним как с интеллектуальным, хотя и несколько своеобразным,
собеседником, который берет на себя значительную часть работы,
связанную с организацией вычислений программы. Поэтому основ-
основное внимание программиста может быть сосредоточено на самой
задаче как таковой, на формировании тех знаний, которые могут
оказаться полезными при ее решении. В чем секрет таких необыч-
необычных свойств логического программирования? Каким образом логи-
логика дает возможность компьютеру решать задачи даже тогда, когда
человек не указывает алгоритмов их решения? В какой форме че-
человеку нужно представить свои знания об окружающем мире для
того, чтобы компьютер мог их понять и сделать из них выводы, т. е.
получить новые знания? Ответы на многие возникающие вопросы
такого рода можно получить, прочитав эту книгу.
Ее авторам удалось преодолеть самую большую трудность, воз-
возникающую при написании учебников по математической логике:
они сумели изложить основные принципы и методы этой необы-
необычайно формальной и абстрактной науки на очень простом и обще-
общедоступном уровне, не поступившись при этом строгостью и пол-
полнотой картины. Основная цель книги — объяснить читателям, как
можно использовать аппарат математической логики для решения
прикладных задач в самых разнообразных областях знаний. Поэто-
Поэтому наибольшее внимание авторы уделяют изучению выразительных
возможностей языка математической логики и эффективных мето-
методов доказательства теорем. Один из таких методов — метод резо-
резолюций — позволяет реализовать на практике концепцию логическо-
логического программирования, согласно которой вычислительная программа
может быть записана при помощи логических формул, играющих
роль аксиом, а ее вычисление представлено в виде доказательства
ПРЕДИСЛОВИЕ
формулы-запроса. Ознакомившись в первых двух главах с основны-
основными понятиями классической логики, с устройством и организаци-
организацией логического вывода, читатель сможет в третьей главе без труда
разобраться в технологии проектирования логических программ и
механизме их функционирования.
Для понимания книги не требуется никаких специальных знаний,
выходящих за рамки школьной программы, и она вполне доступ-
доступна большинству учащихся выпускных классов российских средних
школ. В то же время в ней в той или иной мере рассмотрены основ-
основные понятия классической логики, подробно описаны принципы и
наиболее существенные особенности логического программирова-
программирования. Поэтому эту же книгу можно рекомендовать в качестве учеб-
учебного пособия по математической логике и логическому программи-
программированию всем тем, кто хочет получить предварительные сведения
об этих разделах математики и информатики.
Читатель, освоивший эту замечательную книгу, конечно же, не
должен пребывать в праздной уверенности, что он получил исчер-
исчерпывающее представление о математической логике и может напи-
написать сколь угодно сложные логические программы. Он овладел лишь
ключиком, открывающим доступ к одному из разделов современной
математики, в котором ему еще предстоит отыскать немало ценных
и полезных знаний. И я надеюсь, что для многих из вас этот ключик
окажется поистине золотым.
i ■%.
1 ' '
1 л
. L
J 1«
.« .H
В. А. Садовничий
fii .;■*(.:>
ч-J1" '■■» 'f'fe^:, f^,-tA, '
'. я;г 4 Будущему информатике как мате-
,^'f; ■: ;;: матической науке*.
';.:0Г, г Чй *) Время покажет, в какой мере будет справед-
ливо обратное.
ВВЕДЕНИЕ t
Логика — это наука, которая изучает, каким образом мы выра-
выражаем мысли, делаем умозаключения, и как все это можно предста-
представить формально. К логическими высказываниями относятся прос-
простые предложения и элементарные умозаключения; они подвергают-
подвергаются анализу как с позиции их формы, то есть синтаксиса, так и с
позиции их интерпретации, иначе говоря, семантики. Изучается
также и взаимосвязь синтаксиса и семантики.
Первые упоминания о логике содержатся в произведениях ионий-
ионийских и эллинских философов и софистов. Однако основателем на-
настоящей логики как науки считается Аристотель. Первоначальный
интерес к логике постепенно утрачивался по мере распространения
римского владычества над Средиземноморьем. В средние века боль-
большинство трудов античных философов — за исключением Платона и
Аристотеля — было утеряно или уничтожено, и силлогистика Ари-
Аристотеля была доступна лишь немногим избранным монахам.
С открытием неевклидовых геометрий и возникновением потреб-
потребности в теоретическом обосновании математического анализа ин-
интерес к логике возродился. В 1879 г. Фреге впервые разработал
формальный язык для математики и логики. Однако наибольший
стимул к развитию логика получила в связи обнаружением пара-
парадоксов теории множеств и последующим широким обсуждением их
в математическом сообществе.
В 1895 и 1897 годах Кантор опубликовал первую и вторую ча-
части своих исследований по кардинальным и ординальным числам.
В этих исследованиях, составивших первоначальное обоснование
теории множеств, каждая совокупность объектов рассматривалась
как особая сущность, называемая множеством. Но уже в 1897 году
Буралли-Форти обнаружил парадокс в канторовской теории мно-
множеств. А в 1899 году сам Каитор опубликовал сообщение о па-
парадоксе, затрагивающем его теорию кардинальных чисел. Рассел
опубликовал в 1902 году упрощенную форму того же парадокса, во-
вошедшего в историю математики под названием «парадокс Рассела».
Его сущность такова.
В канторовской теории множеств каждое множество определяет-
определяется характеристическим свойством его элементов. Пусть А — мно-
множество всех множеств X", обладающих свойством X £ X,
А = {Х\Х$Х}
ВВЕДЕНИЕ
Но тогда ' у'1
А € А тогда и только тогда, когда А £ А "л
что, очевидно, образует противоречие.
Парадоксы теории множеств вызвали у математиков того вре-
времени большие сомнения и неуверенность относительно хорошего
обоснования математики. Стало понятно также, что создавать по-
настоящему непротиворечивые математические теории, лишенные
антиномий, можно только путем использования строгой формали-
формализации математических понятий и методов. И вот тогда, благодаря
настойчивым усилиям Гильберта (см. Замечание 1.4.1B)), началось
развитие аксиоматического подхода, и логика приобрела свой со-
современный вид.
Использование и совершенствование вычислительной техники в
начале 1950-ых годов привело к пониманию того, что компьютеры
можно применять не только для арифметических вычислений, но
также и для символьных преобразований. Таким образом, первые
арифметические вычислительные программы и первые программы,
призванные давать ответы на простейшие вопросы и доказывать
простые теоремы, были написаны почти одновременно. Основные
этапы создания общего метода, основанного на логике и позволяю-
позволяющего проводить как обработку предложений, так и символьную ма-
манипуляцию, были впервые осуществлены в 1965 году Робинсоном,
разработавшим метод резолюций, а позднее Ковальским и Колме-
роэ, которые предложили использовать логику непосредственно как
язык логического программирования.
В этой книге раскрываются элементарные понятия математи-
математической логики, рассматриваются взаимоотношения и взаимосвязи
между логикой и логическим программированием.
В первой главе описана логика высказываний (PL). Вначале в
ней изучается язык высказываний, а также синтаксис и семанти-
семантика формул PL. Далее рассматриваются методы доказательства: ме-
метод аксиоматического доказательства, представленный, главным об-
образом, по причинам исторического характера, затем метод таблиц
Бета, в котором доказательства сводятся к математическому ана-
анализу высказываний, и, наконец, метод резолюций. В последнем из
указанных методов доказательства представляются в простой, но
чрезвычайно эффективной форме, которая может быть легко реа-
реализована в виде программы. Перечисленные методы доказательств
обоснованы соответствующими теоремами корректности и полноты.
Во второй главе изучается логика предикатов (PrL). В логике
предикатов более подробно изучается структура высказываний, по-
поскольку язык логики предикатов существенно разнообразнее, неже-
нежели язык логики высказываний. Этот язык содержит кванторы и кон-
константы, предикаты и функции, и поэтому семантика PrL значитель-
значительно сложнее. Среди прочих разновидностей семантики языка логи-
логики предикатов особо выделяются эрбрановские интерпретации, по-
поскольку они позволяют проверять выполнимость предложений PrL,
10 ВВЕДЕНИЕ
используя методы PL. Далее изучаются аксиоматический метод до-
доказательства, метод таблиц Бета и метод резолюций. Метод резолю-
резолюций вместе с алгоритмом унификации положен в основу логического
программирования. Для обоснования этих методов приводятся со-
соответствующие теоремы корректности и полноты.
В третьей главе речь идет о логическом программировании во-
вообще и о языке ПРОЛОГ в частности. Здесь рассматривается также
механизм построения вывода в ПРОЛОГе. Логика обеспечивает логи-
логическое программирование и ПРОЛОГ выразительным языком и предо-
предоставляет теоретическое обоснование, гарантирующее правильность
полученных результатов.
Каждая глава содержит примеры и задачи, предназначенные для
лучшего усвоения соответствующих тем. Примеры демонстрируют
методику решения задач, а сами задачи призваны стимулировать
личную инициативу читателя. Книга является самодостаточной, т. е.
в ней подробно раскрываются все основные понятия математиче-
математической логики, и от читателя требуются лишь элементарные знания
алгебры и анализа. В связи с этим ее можно рекомендовать сту-
студентам любого курса как для самостоятельного изучения, так и для
использования в качестве учебного пособия, подкрепляющего соот-
соответствующий курс лекций. Книга может также оказаться полезной
тем программистам, кто уже имел практический опыт работы с си-
системами логического программирования, не обладая при этом спе-
специальной теоретической подготовкой по логике, а также всем тем,
кто просто интересуется логикой и логическим программированием.
Все темы, затронутые в этой книге, рассматриваются в перспекти-
перспективе перехода от логики к логическому программированию. Поэтому
доказательства некоторых теорем, связанных, как правило, с обос-
обоснованием полноты аксиоматического метода, опущены. В тех случа-
случаях, когда те или иные понятия и доказательства выходят за рамки
книги и обсуждаются в ней лишь поверхностно, мы указываем биб-
библиографические источники, где они изложены более полно.
В основу настоящего пособия положена книга, опубликованная
первым автором в Греции в 1992 году; эта книга была написана по
материалам семинаров, посвященным основам логического програм-
программирования, проведенных в Корнелле и Рочестере, США, и Универ-
Университете Патраса, Греция.
Пользуясь случаем, авторы отмечают значительный вклад, кото-
который внесла Анета Синахопулос-Сварна в разделы 1.1, 1.8, 2.3, 2.11,
3.2, 3.3, 3.6, 3.8, 3.9, в размещение и расположение общего содер-
содержания книги, а также помощь, которую оказал Георгий Потамиас
при написании разделов 3.4, 3.5 и 3.7. Содействие при подготовке
всего материала книги оказали также аспиранты университета Па-
Патраса Костас Контогианнис, Спирос Пападакис и Петрос Петропу-
лос. Все программы, включенные в книгу, равно как и упражнения,
были проверены Георгием Потамиасом в системе программирования
TURBO-PROLOG, V.2.O. ^с;шт .Цк -.л,,пт.,., ■%;,гН,г,>
Глава 1 ' '
ЛОГИКА ВЫСКАЗЫВАНИЙ
,1 , >
Merpov kolvtuv XPW р(
'' > •■ ' тшу ^eV omwv u>( sari, ти/v Si \iv
-jfc '•« i j» » *i ! ! & ovtwv шС ovx ecrri.
i t. f , , Человек — мера всех вещей; сущест-
• ; \ вующих — что они существуют; несу-
несуществующих — что они не существу-
i ■ ... ; ют-
.ii Протагор
)*С>: '^Ч'1, ..sis
§ 1.1. Введение ■ .
,'/>;) .А ■> '>
До 1850 года математические доказательства основывались на
эксперименте и интуиции. В 1666 году Лейбниц впервые отметил
необходимость создания формального языка, названного им «уни-
«универсальной характеристикой», который можно было бы использо-
использовать в математических формулировках и методологии. Однако его
идеи опережали свое время. Начало развития формализма в мате-
математике связывается с публикациями Булем, два века спустя, своих
трудов «Математический анализ логики» A847) и «Законы мыш-
мышления» A854). Свой вклад в создание логического формализма в
математике внесли работы Де Моргана A847, 1864), Пирса A867)
и Фреге A879, 1893, 1903). Публикация же трехтомника Рассела
и Уайтхеда «Principia Mathematica» стала кульминацией этих уси-
усилий, так как в нем была представлена формализующая математику
логическая система, в которой теоремы выводились при помощи ло-
логических аксиом и правил.
Расцвет логики как самостоятельной науки пришелся на 20-е годы
XX века и связан с такими именами, как Лукашевич A878-1956),
Леви A883-1964), Гёдель A906-1978), Тарский A901-1983), Черч
A903-1995) и Клини A909-1994).
Начиная с 50-х годов нашего века компьютерная технология
столкнулась с проблемой использования компьютера для символь-
символьных преобразований. Одно из решений этой задачи предлагает
функциональное программирование. Этот стиль программирования
был разработан Мак-Карти и получил широкое распространение в
12 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
США. Другое решение обеспечивает логическое программирование,
созданное, преимущественно, европейскими учеными, в том числе,
Колмероэ и Ковальским. Логическое программирование придало ло-
логике новый импульс. Оно решило многие проблемы, касающиеся
строения логических высказываний, при помощи которых компью-
компьютер может выполнять процедуры вывода заключений и суждений.
Логическое программирование также раскрывает природу и меха-
механизмы логических процедур, выполняемых компьютером.
В первую очередь нам необходимо рассмотреть, каким образом
формализуются логические и математические высказывания. Как
мы увидим в следующих примерах, логические связки являются ос-
основными элементами формализации.
1. Конъюнкция формализуется при помощи символа Л. Предпо-
Предположим, нам известны два свойства некоторого х:
А: х>3, В: х < 10.
То есть мы знаем, что х больше трех и меньше десяти. Другими
словами, нам известно высказывание , ,
А А В, V
где логическая связка Л соответствует соединительному союзу «и».
Таким образом, высказывание А К В утверждает, что х > 3 и х < 10,
т. е. 3 <х < 10.
2. Отрицание формализуется при помощи символа ->. Например,
рассмотрим высказывание
/гл м •
С: 50 делится на 7П ..-ц
->С обозначает, что 50 не делится на 7. а
3. Дизъюнкция обозначается при помощи символа V. Ееди D
и Е — высказывания
>*?
D: 60 делится на 6, « Е: 60 делится на 5, «
и,
то высказывание
DVE
утверждает, что «60 делится на 6 или 60 делится на 5». Символ V не
является исключающе разделительным, так как 60 является крат-
кратным 6 и 5 также, как и 20, не упомянутого в высказываниях D
и Е.
4. Импликация «если ..., то ...» обозначается в логике симво-
символом —к Если F и G есть высказывания
F: число а кратно 10, , G: число а кратно 5,
§ 1.1. ВВЕДЕНИЕ 13
то высказывание
утверждает, что «если число а кратно 10, то оно кратно 5». '
5. Равносильность «...тогда и только тогда, когда ...» обозначается
символом «->. Например, если Н и I есть высказывания
Н: 16 кратно 2, /: 16 является четным числом,
то формально мы записываем Н «-> /.
Свойства логических связок не одинаковы. В примере о высказы-
высказываниях А и В запись А Л В по существу не отличается от записи
В А А. Интуитивно понятно, что логическая связка V (равно как
и Л) должна быть коммутативной. Однако ответ на вопрос о комму-
коммутативности связки —> будет отрицательным: высказывание G —» F,
«если а кратно 5, то а кратно 10» неверно, так как 15 кратно 5, но
не кратно 10. Поэтому нам необходимо изучить свойства логических
связок.
Существуют также различные типы высказываний. Например, вы-
высказывания
«6 кратно 6»,
£..,'*'г «7 — простое число», ;ч >ог, '
1 «рациональное число есть либо 0, либо не равно 0»
являются «верными», «правильными», в то время, как высказывания
«50 — нечетное число»,
.,,.. «50 делится на 7»,
♦если х = 3, то х = 5»,
относятся к числУ*«неверных», «ошибочных». Наконец, такие вы-
высказывания, как ^ ■
. . ,_, «идет дождь»,
".;;• ,,'v * «я голоден»,
*х равно своему абсолютному значению»,
иногда являются «правильными», а иногда — «ошибочными».
Интуитивно понятно, что каждое высказывание имеет некоторую
интерпретацию: оно может выражать истину или ложь, иначе го-
говоря, может быть истинным или ложным. Но что делает выска-
высказывание истинным? Какова связь между интерпретацией составно-
составного высказывания и интерпретациями высказываний, составляющих
его? И какую роль играют логические связки в интерпретациях?
Нам необходимо изучить интерпретации высказываний и опреде-
определить роль логических связок в этих интерпретациях.
Наша собственная логика позволяет нам принимать решения и де-
делать выводы. Например, мы говорим «если х > 3, то х > 0», или,
формально,
...,. ,-i *:.,-,, >..■ 1,е ...... (Я > 3) —» (Х > 0). »v : „ч..*».*«У,,..-.
14 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Давайте предположим, что х > 3. Тогда х > 0. Какое правило позво-
позволяет нам заключать, что х > 0 в случае, когда высказывание х > 3
истинно? И обладает ли это правило всеобщностью, другими слова-
словами, если М —»N истинно и М истинно, то всегда ли истинно N7
Обратимся к другому примеру. Мы знаем, что для того, чтобы
пойти в кино, нужно иметь деньги на билет. Таким образом,
иду в кино —» имею деньги на билет. A)
Давайте предположим, что мы не имеем достаточно денег на $Й1лет,
т. е. .■■'-'
-> (имею деньги на билет). B)
',«А
Можем ли мы пойти в кино? Каково влияние отрицания? Каквй вид
будет иметь A) с отрицанием? к
-1 (иду в кино) —» -| (имею деньги на билет)? ><•:
Щ 4»' Или -1 (иду в кино —> имею деньги на билет)? :
>.!«;,< Или -1 (имею деньги на билет) —» -■ (иду в кино)?
И какое заключение истинно, если истинны A) и B)?
Для того, чтобы ответить на эти вопросы, нам нужно изучить син-
синтаксис высказываний и правила, которые определяют, когда и как
мы можем выводить истинные заключения, располагая в качестве
посылок имеющимися в распоряжении данными. Логика высказыва-
высказываний, равно как и более сложная логика предикатов, исследует эти
вопросы.
В главе 1, посвященной логике высказываний (PL), мы изучим
высказывания PL с точки зрения их синтаксиса и семантики. Мы
также исследуем методы получения заключений из посылок и опре-
определим формы высказываний PL, необходимые для представления
знаний, разрешающих процедур и автоматического доказательства
теорем в логическом программировании.
,. ,,. . • кч '
'"'' ; § 1.2. Язык логики высказываний >п' ' '
Алфавит, синтаксис и семантика л ,
Язык логики высказываний (PL) является весьма строгим языком.
В терминах этого языка мы формализуем те части повседневной ре-
речи, которые необходимы для представления логических и матема-
математических понятий. Имея ^формализованные в этом языке высказы-
высказывания, мы затем исследуем их в соответствии с их структурой и
ИСТИННОСТЬЮ. ,.,л .. -. ^,, ■:,.■) „ - , ..,.,- ;
§ 1.2. ЯЗЫК ЛОГИКИ ВЫСКАЗЫВАНИЙ 15
Каждый формальный язык задается:
а) алфавитом, содержащим все символы языка;
б) синтаксисом, определяющим, каким образом из символов фор-
формируются высказывания;
в) семантикой, при помощи которой интерпретируется элементы
языка путем приписывания значений символам алфавита.
Алфавит языка логики высказываний состоит:
1) из пропозициональных символов: А, А,, А2,..., В, Ви В2,... ;
2) из логических связок: V, Л, ->, —>, <->;
3) из запятой и скобок: «,» и ♦(», ♦)».
Логические связки интуитивно соответствуют частицам и союзам,
которые мы используем в повседневной речи. Соответствие между
ними таково:
V, дизъюнкция — или;
Л, конъюнкция — и;
—», импликация — если ..., то ...;
<->, эквивалентность— ...тогда и только тогда, когда ...;
->, отрицание — не.
Произвольная последовательность символов, принадлежащих ал-
алфавиту языка, называется выражением. Например, AVVA, А VВ,
+-»А — выражения языка логики высказываний. Некоторые пра-
правильно построенные выражения рассматриваются синтаксисом как
высказывания. В следующем определении 1.2.1 вводится понятие
высказывания и, тем самым, описываются законы синтаксиса языка
логики высказываний.
Определение 1.2.1 (индуктивное определение высказыва-
высказывания). . 1. Пропозициональные символы являются высказываниями
и называются атомарными высказываниями или атомами.
2. Если (гит — высказывания, то выражения (<т Л т), (ст V т),
(<т—>т), (оч-»т), (-кг) — также высказывания; их называют состав-
составными высказываниями.
3. Выражения, построенные в соответствии с пунктами 1 и 2, и
только они являются высказываниями. D 1.2.1
Выражения У А У В и *-»А, таким образом, не являются выска-
высказываниями, так как они построены вопреки пунктам 1 и 2. А вот
выражения (А V В) и ((->А) V (В *-* (->С)) в самом деле являются
высказываниями.
Приведенное выше определение 1.2.1 использует метод индук-
индукции для определения составного высказывания: пункт 1 есть ба-
базис индукции, пункт 2 есть индуктивный переход. Индукция про-
проводится по логической длине, структуре высказывания. Под «ло-
«логической длиной» высказывания А мы подразумеваем натуральное
16 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
число, обозначающее число, тип и порядок появления логических
связок, используемых при построении А, начиная с атомарных вы-
высказываний, составляющих А. Нам известно, что принцип мате-
математической индукции справедлив для натуральных чисел.
Определение 1.2.2 (математическая индукция). Если Р(а)
обозначает свойство натурального числа а и нам известно, что
а) .Р(О) справедливо,
б) для любого натурального п из истинности Р(п) вытекает истин-
истинность Р(п + 1),
то мы можем заключить, что для всех натуральных чисел п истинно
Р(п). О 1.2.2
Тот факт, что множество натуральных чисел вполне упорядоче-
упорядочено (под этим подразумевается, что каждое непустое подмножество
натуральных чисел имеет наименьший элемент), вместе с принци-
принципом математической индукции приводят ко второй форме индукции,
называемой полной.
Определение 1.2.3 (полная индукция). Если Р(а) есть
свойство натурального числа а, и нам известно, что
а) .Р(О) справедливо,
б) для всех натуральных чисел тип, таких, что т < га, из Р(т)
можно вывести Р(п),
то для всех натуральных чисел га истинно Р(п). О 1.2.3
Мы использовали полную индукцию в индуктивном определении
высказываний (определение 1.2.1). Теперь применим ее в следую-
следующем определении 1.2.4.
Определение 1.2.4 (общая схема индукции для высказы-
высказываний). Пусть Р — пропозициональное свойство. Мы будем пи-
писать Р(а), чтобы обозначить, что высказывание а имеет свойст-
свойство Р. Если мы докажем, что
а) Р(А) — истинно для любого атома А языка,
б) если а, и о-, — высказывания и P(&i), -Р(<72), то Р((<Т| Л ст2)),
P(( V <г2)), Р({а, -+ <т2)), Р((а{ ~ <т2)), Р((-<т1)) и Р(Ы))
то мы можем заключить, что свойство Р{о) справедливо для любого
высказывания а нашего языка. □ 1.2.4
Пример 1.2.5.
1. Свойство Р «число левых скобок совпадает с числом правых
скобок» истинно для всех высказываний PL.
В самом деле, согласно общей схеме индукции мы имеем:
а) в пропозициональных символах число левых и правых скобок
равно 0;
б) если в высказываниях ст, и ст2 число левых и правых скобок
совпадает и равно для ах и ст2 соответственно п и т, то в высказы-
высказываниях (G, Л <72), ((Т, V (Т2), ((Т, —» (Т2), ((Т, ♦-» <72), (-Х7,) И (--СГ2) ЧИСЛО
§ 1.2. ЯЗЫК ЛОГИКИ ВЫСКАЗЫВАНИЙ 17
левых и правых скобок совпадает и равно п + т + 1 в первых че-
четырех, п + 1 и т + 1 соответственно — в двух последних.
2. Выражение ((->(А А В))—» С) является высказыванием.
Доказательство основано на определении 1.2.1:
1) А, В являются высказываниями по определению 1.2.1A);
2) (А А В) является высказыванием по определению 1.2.1B);
3) (~>{А А В)) является высказыванием по определению 1.2.1B);
4) С является высказыванием по определению 1.2.1B);
5) ((->(А А В) —> С) является высказыванием по определению
1.2.1B).
3. Выражения, приведенные ниже, не являются высказываниями:
-1 — символ -> не является атомом;
Л —» А — символ Л не является высказыванием;
(А А В —нет правой скобки, соответствующей левой. D 1.2.5
Пример 1.2.6. Рассмотрим повествовательное предложение
обыденной речи:
F: «Если нет дождя, то я пойду на прогулку».
Для того, чтобы формализовать его в логике высказываний, можно
ввести вспомогательные пропозициональные символы:
А: «Идет дождь»; В: «Я иду на прогулку».
Тогда предложение F соответствует высказыванию ((->А) —> В).
Если не возникает путаницы, то скобки можно опустить:
F: -^A^B. U 1.2.6
Каждый атом, который встречается в правильно построенной фор-
формуле1) D рассматривается как подформула D. Например, А и В —
подформулы F в примере 1.2.6. Более того, каждая правильно по-
построенная составная часть D является также подформулой D. Рас-
Рассмотрим в качестве примера формулу
D: (A A ^B) ^((CV^A)^B).
Тогда ->А, С V ->А, А Л ->В равно, как и (С V ->А) —► В, являются
подформулами D. Наконец, сама формула D, т. е. (АЛ->1?)—>((CV
V->A)—» В), также рассматривается как подформула D.
Множество subform(o-) всех подформул правильно построенной
формулы а определяется индуктивно:
Определение 1.2.7. 1) Если а — атом А, то subform(cr) =
{А}
1) Высказывания логики высказываний называются также формулами. — Прим.
18 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
2) если а имеет вид -it, to subform(o-) = subform(r)u{(r};
3) если а имеет вид т о ip, где о е {V, Л, —>, ♦-»}, то subform((r) =
= sub{orm(T)usubform(^)u{(r}. D 1.2.7
Замечание 1.2.8. Чтобы избежать неоднозначностей при
использовании связок в формулах без скобок, мы будем считать, что
-1 связывает сильнее, чем все остальные связки, Л и V связывают
сильнее, чем <-> и —*,*-* связывает сильнее, чем —*. Таким образом,
высказывания
(I. i :'.
обозначают соответственно i ,',
(H)^(BVC)), ((ЛлВ)->С), (А^(В^С)). О 1.2.8
Замечание -1.2.9. Следуя сложившейся традиции, символ
«— мы будем также рассматривать как логическую связку, В <— А
обозначает то же, что и А —» В. □ 1.2.9
§ 1.3. Понятие семантики в логике высказываний
Означивания и истинностные означивания
Согласно определению 1.2.1 высказывания являются общим и аб-
абстрактным объектом. Мы хотим интерпретировать эти абстрактные
объекты при помощи семантики. Это означает, что нас интересует
определение условий, при которых высказывание является истин-
истинным или ложным. Поэтому мы создадим структуру, область опреде-
определения которой — {t, /}, где t, f обозначают истинностные значения
«истина» и «ложь» соответственно, и попытаемся приписать одно из
этих значений каждому высказыванию. Используемый метод при-
приписывания истинностных значений, подкрепленный необходимыми
определениями, и составляет семантику логики высказываний.
Определение 1.3.1. Означиванием назовем произвольную
функцию
где Q — множество атомов языка. D 1.3.1
Таким образом, означивание приписывает истинностные значения
атомам языка.
Теперь мы введем на множестве {t, /} внутренние алгебраиче-
алгебраические операции для того, чтобы преобразовать его в алгебраическую
структуру. Внутренние операторы над t, f, которые мы определим, а
именно, ~, U, П, ~* и <~>, будут соответствовать логическим связкам
-1, Л, V, —> и <->. Сходство соответствующих символов не случайна,
§ 1.3. ПОНЯТИЕ СЕМАНТИКИ В ЛОГИКЕ ВЫСКАЗЫВАНИЙ
19
она отражает их соответствие. Рассмотрим, например, высказыва-
высказывание А У В. Приписав некоторые истинностные значения А и В, мы
интерпретируем AVB, используя интерпретации А и В и применяя
операцию U, на основании определения 1.3.2.
Определение 1.3.2. Внутренние операции ~, U, П, —* и «~>
над {t, /} определяются следующими таблицами.
t
f
f
t
LJ
t
f
t
t
t
f
t
f
П
t
f
t
t
f
f
f
f
t
f
t
t
t
f
f
t
t
f
t
t
f
f
f
t
k)
В приведенных таблицах в первом столбце перечислены значения
первого аргумента и в первой строке — значения второго аргумента
соответствующих операций. П 1.3.2
Структура ({£, /}, ~, U, П), в которой операции ~, U, П определе-
определены описанными таблицами, является двузначной булевой алгеброй.
Булевы алгебры важны как для семантики логики высказываний
(см. [RaSi70, СиггбЗ, Rasi74, Raut79]), так и для изучения теорети-
теоретических основ информатики вообще.
Определение 1.3.3. Пусть 5 — множество высказываний
нашего языка. Истинностным означиванием, или булевым озна-
означиванием назовем такую функцию
V: S~{t,f},&t
что для произвольных G, т € S верно: ,.
а) если о- — атом, то V(a) e{t, /};
б) V(-.(t) =~ V(a);
в) V(<xVT) = V(ff)uV(T); ' '
г) V(a А т) = V{a) П V(t); '. , .
д) V(<t-» т) = V»-» V(t);
е) V(a ч-> т) = V(a) <~» V(t). !«♦ • : м,.,< ,ч ■♦ П 1.3.3
20 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Согласно этому определению истинностные значения атомов
некоторого высказывания преобразуются алгебраическими операци-
операциями ~, U, П, ~», <~> и определяют тем самым истинностное означи-
означивание рассматриваемого высказывания (см. [Smul68]).
Означивание приписывает истинностное значение, t или /, ато-
атомам языка. Истинностное означивание является расширением озна-
означивания на множество высказываний языка. В последующей теоре-
теореме 1.3.4 будет доказано, что каждое означивание может быть одно-
однозначно расширено до истинностного означивания.
Теорема 1.3.4. Для каждого означивания F существует
одно и только одно истинностное означивание V, являющееся
расширением F.
Доказательство. Проведем доказательство индукцией по
длине высказывания.
Пусть F — означивание, Q — множество атомов. Индуктивно
определим истинностное означивание V, полагая
а) V(A) = F(A) для каждого А 6 Q.
Пусть a, tp — высказывания. Если V(a) и V(tp) уже определены,
то положим
б) V{-«j) =~ V(a); u, 4 . ,. „ ,
. т г/ v ТЛ/ \ ЛТI \ *~~ "~ ' " 1'" — --
д) V(cr —»tp) = V(cr) -~* V(tp); ц~)-< '?! ..,| .;■ nq !-.
Очевидно, что V является истинностным означиванием, расши-
расширяющим F.
Остается доказать, что если истинностные означивания VJ и V2
являются расширениями F, то равенство VJ(i^)= V2(tp) выполняет-
выполняется для любого высказывания tp. Докажем по индукции свойство Р:
Базис индукции.
Для каждого пропозиционального символа А верно, что VJ(A) =
= ^(А), так как V[, V2 — расширения F.
Индуктивный переход.
Предположим, что VJ(tr) = V2(a) и V^tp)— V2(tp). Тогда справед-
справедливы соотношения:
V,ba) =~ Vt(a) =~ Va(<p) = Vabip);
V2(aVtp); . ., . i
Л<р)= Vx(o) П V&) = V2(a) П Щч>) = V2(a A tp); ' ,,AV
= V2{o) ~* V2(tp) = V2{o - <p); 4
§ 1.3. ПОНЯТИЕ СЕМАНТИКИ В ЛОГИКЕ ВЫСКАЗЫВАНИЙ 21
x( р) j() Щр) = V2(a) <~* V2(p) = V2(a <-» у>).
Таким образом, Vj и V^ имеют одинаковые значения для каждого
высказывания, и поэтому совпадают. D 1.3.4
Следствие 1.3.5 непосредственно вытекает из теоремы 1.3.4.
Следствие 1.3.5. Пусть а — высказывание, все атомы ко-
которого содержатся в списке А,, ..., Ak. Если два истинностных
означивания Vx, V2 имеют одни и те же значения на множестве
{A1,...,Ak},moVl(a) = V2(a). D 1.3.5
Пример 1.3.6. Вычисление истинностного означивания по
заданному означиванию.
Пусть 5 — множество атомарных высказываний, 5 = {А1,А2},
F — такое означивание, что
F(At)=t, F(A2) = f.
По теореме 1.3.4 искомое истинностное означивание V^., расширя-
расширяющее F, определено однозначно.
Положим, что
VF(Ai)-=t, VF(A2):=f,
где := обозначает «равно по определению».
Теперь мы можем вычислить значения истинностного означива-
означивания Vp для каждого множества высказываний, которые содержат
только атомы А, и А2:
VF(A, A A2) = VF{Ax) П VF(A2) = i П / = /;
VF(A\ v A2) = VAAJ U VF(A2) =tuf = t;
VF((A, A A2) - A2) - VF(At V A2) ~* VF(A2) = t ~* f = f;
и т.д. D 1.3.6
Мы можем классифицировать высказывания логики высказыва-
высказываний в соответствии с истинностными значениями, которые они при-
приобретают.
Определение 1.3.7. Высказывание а называется логически,
истинным, или тавтологией, если для каждого истинностного
означивания V верно, что V(a) — t. Мы будем пользоваться за-
записью f= а для обозначения тавтологии. В свою очередь, запись ^
будет обозначать, что а не является тавтологией, т. е. существует
истинностное означивание V, такое, что V(a) = /.
Высказывание а называется выполнимым или подтверждае-
подтверждаемым, если существует такое истинностное означивание V, что
V(a\ = t. При этом про истинностное означивание V, для которого
V(cr) = t, говорят, что оно подтверждает высказывание а.
Высказывание а, такое, что для каждого истинностного озна-
означивания V верно V{a) = /, называется логически ложным, или
невыполнимым, или противоречием. О 1.3.7
22 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Замечание 1.3.8. Пусть V — истинностное означивание, и
множество
Sy = {a: V(a)=t}
состоит из всех высказываний языка, выполнимых при означива-
означивании V. Если высказывание ip принадлежит множеству Sv для каж-
каждого истинностного означивания V, то ip является тавтологией.
Каждое множество Sv< где V — истинностное означивание, состав-
составляет возможный мир (см. [Fitt69, Chel8O]) множества высказываний
PL. Каждый возможный мир является аристотелевым в том смыс-
смысле, что для каждого высказывания о только одно из двух высказы-
высказываний а к-у а может быть истинно в этом мире. И в самом деле, мы
имеем либо V(a) = t, либо V{a) = f, что равносильно V{->a) = t,
сообразно аристотелеву принципу исключенного третьего, заме-
замечание 1.4.4).
Возможные миры — основное понятие семантики Крипке. Се-
Семантика Крипке используется при изучении модальной логики. В
модальной логике кроме логических связок содержатся специаль-
специальные символы, как, например, о, называемые модальными операто-
операторами, что расширяет выразительные возможности языка. Поэтому в
модальном языке кроме выражения А встречается выражение оА,
которое может интерпретироваться как «иногда А истинно», или
«А будет истинно в будущем».
Модальная логика позволяет нам выражать особые свойства, за-
затрагивающие расположение и порядок выполнения операторов про-
программы.
Рассмотрим, например, программу на языке ФОРТРАН, предназна-
предназначенную для вычисления п! для всех целых чисел п от 1 до 10.
;■№..>? .:,'-<.! , do 10 i =1,..., 10 '•: n. "■ ".^'
•■'Г -i''» -■- " '''4 k = k*i ,.,...,
10 write(*, *)&
end , .. ;, . . ,,,,!
Пусть Л и В — высказывания модальной логики, ' :"\' ' " '|
А := write(*, *)к и В := end. ' ' f
ln/' ■
В тот момент, когда программа начинает выполняться, высказы-
высказывания оА и оВ истинны. Это означает, что программа когда-то в
будущем вычислит п! и когда-то в будущем она остановится. D 1.3.8
Определение 1.3.9. Два высказывания, а и т, такие, что
V(a) = V(t) для каждого "истинностного означивания V, называ-
называются логически эквивалентными. Для обозначения эквивалентных
высказываний будем использовать запись а = т. D 1.3.9
§ 1.3. ПОНЯТИЕ СЕМАНТИКИ В ЛОГИКЕ ВЫСКАЗЫВАНИЙ 23
Пример 1.3.10. Высказывания А V ->А и {{А —* В) —> А) —>
—> А — тавтологии.
Доказательство. Сначала докажем, что А V ->А — тавтоло-
тавтология. Пусть VJ и V2 — два таких истинностных означивания, что
Vx(A)=t, V2(A) = f.
Заметим, что
Vt(A V -,А) = Vl(A)U Щ-iA) = V;(A) U (~ F2(A)) = t U (~ t) =
= tuf = t,
= f\jt-t.
Произвольное истинностное означивание V на А совпадает либо
с VJ, либо с V2.
Таким образом, согласно следствию 1.3.5 выполняется одно из
двух:
V(Av->A) = V;(AV-iA)=t или V(A V ->А) = V2(A V ->Л) = t.
То есть высказывание истинно для любого истинностного означива-
означивания V. Следовательно, оно является тавтологией.
Теперь докажем, что ((А —>В)-* А)—* А — тавтология. На Q =
= {А, В} имеется четыре различных означивания Fu F2, F3, FA:
F1(A)=t, Fx(B)=t, ^
'? m.^ *. ^ F2(A) = t,
Для каждого из этих означиваний существует единственное истин-
истинностное означивание 1^, fc G {1, 2, 3,4}, расширяющее его. Неслож-
Несложно проверить, что
Vk(((A-^B)-^A)-^A)=t для каждого fee {1,2, 3,4}.
Произвольное истинностное означивание V на пропозициональных
символах А и В совпадает с Vk для некоторого А; е {1, 2, 3,4}. В
силу следствия 1.3.5 справедливо равенство
V(((A ^B)-*A)-*A) = Vk(((A -+B)^A)-+A) = t.
Следовательно, высказывание ((А —* В)—* А)—* А истинно для
любого истинностного означивания и поэтому является тавтологи-
тавтологией- Jlift'Wr, '^.г^-ЬЩ^ф- ■i№,-->jLhs.:^;!j.t,wu.->^ .. С 1-3.10
24 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Пример 1.3.11. Высказывание ((->А Л В)—> С) У D) (обозна-
(обозначим его К) выполнимо. В самом деле, пусть F — такое означивание
пропозициональных символов К, что
F{A)=t, F(B)=t, F(C) = f, F(D) = f.
Истинностное означивание V, расширяющее F, приписывает сле-
следующие значения: ...''':•',.'
Тогда
A Л В) - С) = V(-^A ЛВ)~> V(C) = fZ*f=t,
V(((-nA Л В) -» С) V Z?) = V((-.A Л В) -► С) U V(D) = t U / = t,
следовательно, ()
Высказывание К не является тавтологией. И в самом деле,
пусть G — такое означивание, что
G(A)=t, G(B)=t, G(C) = f, G(D) = f. ;" J--
Предположим, что G' — истинностное означивание, расширяю-
расширяющее G. Применяя метод, аналогичный используемому при доказа-
доказательстве того, что V(K)= t, мы можем доказать, что G'(K) = f.
Тогда, по определению 1.3.7, высказывание К не является тавтоло-
тавтологией. D 1.3.11
•if" ">У. -1 >. ■'■■■■■'. -• - .-; i:>A O'.:;,,.'v Л К!\ГЧ
§ 1.4. Таблицы истинности
В предыдущем параграфе мы определили означивание атомов язы-
языка и, затем, распространив означивание атомов на составные вы-
высказывания, определили истинностные означивания. При помощи
этого метода мы можем установить, является ли высказывание тав-
тавтологией, противоречием, или оно выполнимо. Однако, чем больше
составляющих содержит высказывание, тем более сложным стано-
становится этот метод.
Чтобы сделать его несколько проще, мы соберем все возможные
означивания атомов высказывания в таблицу, называемую табли-
таблицей истинности высказывания. Итак, для составных высказываний
-уA, AVВ, А ЛВ, А —> В и А <->В мы имеем следующие таблицы:
§ 1.4. ТАБЛИЦЫ ИСТИННОСТИ
25
A
t
f
->A
f
t
A
t
f
t
f
В
t
t
f
f
AW В
t
t
t
f
A
t
f
t
f
В
t
t
f
f
АЛВ
t
f
f
f
A
t
f
t
f
В
t
t
f
f
A -*B
t
t
f
t
A
t
f
t
f
В
t
t
f
f
A<-+B
t
f
f
t
;■ i u.
Каждая строка в этих таблицах соответствует означиванию и его
однозначному расширению до истинностного означивания. Напри-
Например, вторая строка в таблице А А В имеет вид t, /, /. Она означа-
означает, что А принимает значение t (это первый элемент строки), В
принимает значение / (это второй элемент строки). На основании
определения 1.3.2 и определения 1.3.3 мы знаем, что соответству-
соответствующее истинностное значение А А В есть t П /, а именно /. Таким
образом, мы находим / (это третий элемент строки).
В дальнейшем мы будем использовать описанные выше таблицы
истинности как определения результирующих значений при исполь-
использовании логических связок, не ссылаясь на означивания и истин-
истинностные означивания.
Замечание 1.4.1. 1. Дизъюнкция логики высказываний не
является разделительной, т. е. А V В принимает значение t и тогда,
когда и А, и В принимают значение t. В повседневной речи, напро-
напротив, чаще всего фигурирует разделительная дизъюнкция. Например,
мы говорим: «Я останусь дома или пойду в кино», подразумевая при
этом выбор только одного варианта, но никак не обоих.
2. Высказывание А —> В принимает значение / только тогда, ко-
когда А принимает значение t, а В принимает значение /. Таким
образом, если А есть /, то А —* В есть t, независимо от того ка-
какое значение принимает В. Эти свойства —> и, как следствие, та
часть логики высказываний, которая основывается на этих свойст-
свойствах, принимаются не всеми логическими школами.
26
Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
В 1910-1920 гг. в области прикладных наук в Европе преобладала
концепция школы Гильберта (Гильберт, 1862-1943) (см. [Воуе68,
Heij67]):
«Математика и логика должны иметь аксиоматическое ос-
основание, и используемые этими науками методы должны быть
максимально формальными».
Но в 1918 г. Брауэр A881-1966) опубликовал суровую критику ло-
логики высказывании. Представленная в его работе альтернативная
система была названа интуиционистской логикой. Это название
происходит из утверждаемого Брауэром факта, основанного на мне-
мнении Канта, что мы ощущаем натуральные числа (и, соответствен-
соответственно, логику, которая характеризует науку) только интуитивно (см.
[Dumm77, Brou75]). Интуиционистская логика никогда целиком не
замещала логику, основанную на концепции Гильберта, однако, се-
сегодня она имеет некоторые приложения в информатике.
С другой стороны, логика высказываний предлагает эффективный
инструмент (в аристотелевом смысле) для изучения и решения раз-
различных задач и составляет основу современной науки и техники.
D 1.4.1
Резюмируем:
опираясь на индуктивное определение высказываний и на
определение значений логических связок, мы можем построить
таблицу истинности для любого высказывания, приписав зна-
значения всем атомам, составляющим его.
' Пример 1.4.2. Таблица истинности высказывания А ЛВ —> С:
■if
A
t
t
t
t
f
f
f
f
В
t
t
f
f
t
t
f .
f
С
t
f
t
f
t
f
t
f
АЛВ
t
t
f
f
f
f
f
f
АЛВ ->C
t
f
t
t
t
t
t
t
1' '
V . » ■
t &>
§ 1.4. ТАБЛИЦЫ ИСТИННОСТИ
27
Для тройки атомов (А, В, С) тройка истинностных значений (/, t, f)
обращает А А В —> С в истину, тогда как тройка (t, t, f) обращает
его в ложь. D 1.4.2
Сокращенной таблицей истинности высказывания А А В —> С
называется его таблица истинности, в которой вспомогательный
четвертый столбец пропущен.
Сокращенная таблица истинности высказывания, содержащего п
атомов, состоит из 2" строк и п + 1 столбца.
При помощи таблицы истинности мы можем устанавливать, когда
высказывание истинно, а когда — ложно. В силу следствия 1.3.5, ес-
если в таблицах истинности для двух высказываний столбцы значений
атомов и последние столбцы совпадают, то эти два высказывания
логически эквивалентны.
Пример 1.4.3.
1. Высказывание ((А —> В) —> А) —* А является тавтологией.
A
t
t
f
f
В
t
f
t
f
A-*B
t
f
t
t
(A^B)^A
t
t
f
f
{(A-*B)-*A)-+A
t
t
t
t
2. Высказывание (P —* Q) A (P Л ->Q) невыполнимо.
p
t
t
f
f
Q
t
f
t
f
/
t
f
t
P-*Q
t
f
t
t
P A-yQ
f
t
f
f
(P-*Q)A(PA^Q)
f
f
f
f
Замечание 1.4.4. Основываясь на определении 1.3.7 мы
имеем:
1) высказывание является тавтологией тогда и только тогда, когда
его отрицание невыполнимо; ,;; -^ик, »•>«■ . .■■■>&* •< ■.*и.у.:ь>п<»! .«.
28 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
2) высказывание невыполнимо тогда и только тогда, когда его
отрицание является тавтологией;
3) высказывание, являющееся тавтологией, выполнимо, тогда как
выполнимое высказывание не обязательно является тавтологией;
4) некоторые часто используемые тавтологии:
' 1) ~i(A A B) = (~iA V-1.B) — закон де Моргана; ' '', ,
2) -i(А V В) = (-1А А -уВ ) — закон де Моргана; - ч "*
3) -i(-iA) = А —закон двойного отрицания; "•
4) (А —* В) = (~>В —► -уА) — закон контрапозиции;
5) E-»С)-» ((А —* В) —* (А —> С)) — первый закон силлогисти-
силлогистики;
6) (А —> В) —> ((В —> С) —> (А —► С)) — второй закон силлогистики;
7) (А —> (В —> С)) = ((Л Л5)-*С) — закон транспозиции;
8) А V -нА — закон исключенного третьего.
Высказывания 5 и б называются аристотелевыми законами сил-
силлогистики. □ 1.4.4
Метод нахождения значения составного высказывания при помо-
помощи таблицы истинности достаточно прост, если высказывание со-
содержит небольшое число атомов. В том случае, когда высказывание
имеет три атома, соответствующая таблица истинности состоит из
23 = 8 строк. Таблица истинности высказывания, имеющего четыре
атома, состоит уже из 24 = 16 строк, а имеющего десять атомов, —
из 210= 1024 строк!
Кроме того, нужно иметь ввиду, что мы не можем использовать
таблицы истинности в логике предикатов. Поэтому в следующих па-
параграфах мы изучим более совершенные и более экономные методы
определения истинностных значений высказываний и множеств вы-
высказываний. Эти методы будут составлять основу логического про-
программирования.
f *
t § 1.5. Логические следствия и интерпретации ' ;
Из таблицы истинности высказывания (АлВ)-»С в приме-
примере 1.4.2 можно видеть, что это высказывание принимает значение t,
если все три атома А, В, С принимают значения t. В этом случае
говорят, что истинность (ААВ)—* С следует из того факта, что каж-
каждое высказывание из S = {А, В, С} имеет значение t (см. [Chur56]).
Таким образом, введем следующее понятие.
Определение 1.5.1. Пусть S — множество высказываний.
Высказывание о называется логическим следствием S (этот факт
§ 1.5. ЛОГИЧЕСКИЕ СЛЕДСТВИЯ И ИНТЕРПРЕТАЦИИ 29
будет обозначаться S \= а), если для каждого истинностного озна-
означивания V, обладающего свойством V(ip)= t для любого ip E S, мы
можем заключить, что V(a)= t.
Обозначим Con(S) = {<r: S |=ст} множество всех логических след-
следствий S. Формальное определение этого множества таково:
а е СопE')^(для каждого истинностного означивания V)
(для каждого tp e S верно V(tp) = t) => {V(a)— t).
В дальнейшем вместо выражения «для каждого ip G S верно V(<p) =
— t» мы будем использовать запись ^[5'] = {t}, или даже еще менее
формально F[.S]=£. D 1.5.1
Замечание 1.5.2. Символы о и =>-, используемые в данном
выше определении в значениях «тогда и только тогда» и «влечет»,
являются символами метаязыка. Метаязык — это язык, исполь-
используемый для рассуждений о формулах логики высказываний и для
исследования их свойств. Когда, например, мы говорим, что |= ip,
т. е. высказывание р — тавтология, мы выражаем суждение о ip.
Поэтому |= tp является метавысказыванием для PL , а именно вы-
высказыванием метаязыка PL.
Как и язык логики высказываний, метаязык может быть форма-
формализован. Но для того, чтобы избежать чрезмерного и педантичного
использования символов, например, —> в языке и => в метаязыке,
в качестве метаязыка мы будем использовать тщательно и точно
сформулированные предложения разговорного языка.
Завершим комментарий о метаязыке следующим примером. Пусть
А — высказывание PL. Тогда выражение «А —> А» — это высказы-
высказывание PL, а выражение «если А является высказыванием PL, то А
является высказыванием PL» — это высказывание метаязыка PL.
. . D 1.5.2
Пример 1.5.3. Пусть S = {А А В, В —> С} — множество вы-
высказываний. Тогда С — логическое следствие S, т. е. S |= С.
Доказательство. Допустим, что V — истинностное озна-
означивание, которое обращает все высказывания S в истину:
V(AAB) = t, V(B-4C)=t.
Тогда по определению 1.3.3 мы имеем:
hi. ■
if
V(A)nV(B)=t, A)
V(B)~+V(C)=t. B)
Затем, из A) и определения 1.3.2 следует, что ss^j, „
= t. Д» C)
30 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
и, следовательно, B) преобразуется к виду • ,■ , •
t~>V(C)=t. ' ]/^■'•Zv-..а* ' D)
Из определения 1.3.2 и D) мы можем заключить, что F(C)= t. Это
означает, что каждое истинностное означивание, подтверждающее
все высказывания из S, подтверждает также С. Таким образом, С
является логическим следствием S, т. е. S |= С. □ 1.5.3
Обозначив Taut множество всех тавтологий, докажем следствие.
Следствие 1.5.4. Соп@) — Taut, где 0 обозначает пустое
множество.
Доказательство. Рассмотрим оG Taut. Тогда для каждого
истинностного означивания V имеем V(a)= t, т. е. справедливо
соотношение
Следовательно, о е Соп{0). v * "
Верно и обратное. Рассмотрим а е Соп@). Тогда для 'ЮЬкдого
истинностного означивания V имеем:
если для каждого ip G 0 справедливо V(ip)= t, то V(tf)'*s't A)
Но в 0 нет элементов. Поэтому мы можем записать:
'! если для каждого <р е0 верно, { ''*
i, что V(tp)=t или
То есть V(a) = t независимо от значения tp e 0. Это означает, что
для всех истинностных означиваний V верно, что V(a)= t. Следо-
Следовательно, о является тавтологией. □ 1.5.4
Таким образом, тавтологии не являются следствием какого-либо
специального множества высказываний1), они не зависимы ни от ка-
какого множества высказываний и связаны только с таблицами истин-
истинности, определенными в § 1.3.
Подчеркнутые части в доказательстве следствия 1.5.4 отмечают
технические моменты доказательства. В пустом множестве нет эле-
элементов. Как же мы можем записать импликацию с подчеркнутой
частью? Давайте вспомним третью и четвертую строки определе-
определения таблицы истинности высказывания А —> В (см. стр. 25). Если А
принимает значение / и В принимает значение t или /, то А —* В
равно t. Это значит, что если А есть ложь, то импликация А —* В
всегда истинна! Именно этим свойством мы и воспользовались в ме-
метаязыке, в котором доказываются наши теоремы. В A), например,
') Это означает, что тавтологии логически следуют из любого множества выска-
высказываний S вне зависимости от его состава. — Прим. перев.
§ 1.5. ЛОГИЧЕСКИЕ СЛЕДСТВИЯ И ИНТЕРПРЕТАЦИИ 31
утверждение <ир 6 0» не может быть истинно, так как в 0 нет эле-
элементов. Независимо от того, является ли утверждение «V(tp) = t»
истинным или нет, A) истинно!
Как упоминалось выше, PL изучает множества высказываний.
Следующие два определения касаются выполнимости множества вы-
высказываний.
Определение Л .5.5. Множество высказываний S (семанти-
(семантически) непротиворечиво, если существует истинностное означива-
означивание, которое подтверждает каждое высказывание из S. Формально:
непротиворечивоE')^(существует означивание V)
[(для каждого о G S) (F(a)= *)].
Тот факт, что S непротиворечиво, обозначается V(S)= t.
Непротиворечивое множество S мы будем называть также под-
подтверждаемым, или выполнимым. Про истинностное означивание
V, которое подтверждает каждое высказывание непротиворечивого
множества S, говорят, что оно подтверждает S.
Соответственно, S противоречиво, неподтверждаемо, или
невыполнимо, если каждое истинностное означивание не подтвер-
подтверждает по меньшей мере одно высказывание из S. Формально:
противоречиво (S) =Ф-
(для каждого означивания V) [(существует а Е S) (V(<r) = /)].
D 1.5.5
Пример 1.5.6. Множество высказываний S = {АЛ-*В, А -+В}
противоречиво.
Доказательство. Предположим, существует такое истин-
истинностное означивание V, что для каждого С G S верно V(C)— t.
Тогда
V(AA-^B)=t, V(A-*B)=t,
что означает
V(A)nV(-,B) = t, A)
% V(A)~*V(B)=t.\:; B)
Из A) и определения 1.3.2 следует, что V(A)= V(^B)= t, и
V(A)=t, V(B) = f.
Тогда из B) следует, что t ~»/ = t, что противоречит определе-
определению 1.3.2, в котором t -~+f = f. Следовательно, никакое истинност-
истинностное означивание не может подтвердить все высказывания S, т. е. S
противоречиво. □ 1.5.6
Определение 1.5.7. Истинностное означивание, подтвер-
подтверждающее множество высказываний S, называется интерпретаци-
интерпретацией S. Множество всех интерпретаций S обозначается Int(S).
32 Глава I. ЛОГИКА ВЫСКАЗЫВАНИЙ
Int(S) = {V: V — истинностное означивание и для каждого а е S
верно V(a) = t}. D 1.5.7
Докажем некоторые полезные свойства логических следствий и
интерпретаций.
Следствие 1.5.8. Для любых множеств высказываний S,
Su S2 верно:
-6 1) 5, С S2=$-Con(Sx)<ZCon{S2); -а-;,: .> .;. . , -.v.-i- .,•/и Ьь . •■
■ 2)SCCon(S); :г: ^--.Р---^^- '
: 3) Taut С Con(S) для любого S;o)<r? ^у.хт"У\^г:г.у>Лп-.у
4) Con(S) = Con(Con(S)); $\ ''.'." : > '
^ 5) ^ CSz^InHSjClntiSi); "*,',.'' !/;л,„ ., :> 0,U! ,. Й
-е 6) ConE) = {cr: V(a) = t для каждого Velnt(S)};
« 7) а е Соп({ап ..., ая}) «■ а, -»(а2 -»(.. .(а„ -» а)...)) е Таи*.
у Доказательство. 1. Предположим, что о е Con{S{).
Пусть V — такое истинностное означивание, что для каждого р е S2
справедливо V(ip)— t. Таким образом, верно, что V(y?) = t для каж-
каждого ц> е 5, (так как 5, С 52). Тогда V(cr) = t, поскольку а е Con(Sx).
Следовательно, Con(S{) С Con(S2).
2. Если сг е S, то каждое истинностное означивание V, подтвер-
подтверждающее все высказывания S, также подтверждает о. Таким обра-
образом, а е Con(S). Но тогда S С Con(S).
3. Предположим, что а е Taut. Пусть V — такое истинностное
означивание, что для каждого ре S верно V(f)—t. Тогда V(a)= t,
и поэтому а е Con(S). Следовательно, Taut С Con(S).
4. Согласно пункту 2 мы имеем S С Con(S), а согласно пунк-
пункту 1 — Con(S) С Con(Con(S)). Остается только доказать, что
Con(Con(S)) С Con(S). шки*
Предположим, что сте Соп(СопE)). Пусть У — истинностное озна-
означивание, такое, что для каждого р е S имеет место V(p) = t. То-
Тогда для каждого т е Con(S) верно, что V(t) = t. Из определения
Con(S) следует, что У(сг)= £. Это означает, что о е Con(S). Сле-
Следовательно, Con(Con(S)) С Con(S).
5. Если V е Int(S2), то для каждого ст е 52 справедливо У(ст) = t.
Ввиду того, что .?! С 52, для каждого о е 5, верно, что V(cr) = t и,
следовательно, Ve/n£(S,).
6. Если сте Con(S), то для каждого Ve/ni(S) верно, что V(a) =
— t. Тогда ~ \ К]
«!*• ?"*.' •'
{ = t для казщого Ve/ntE)}. f.
§ 1.5. ЛОГИЧЕСКИЕ СЛЕДСТВИЯ И ИНТЕРПРЕТАЦИИ 33
Более того, если . .:sjj«W« > j>
H'S' '.. "'' '■ 'i4 its**-:?»'
ip € {a: V(a) — t для каждого V е Int^S>)}t г, "■ t -
то, очевидно, у? е Con(S). ^ f ■ ' ; • * •; <
7. (=Ф-) Предположим, что <р е Соп({сг1,..., cr$f.' flycti'■*!*"•***■
истинностное означивание. Возможны два случая: -,,
а) для каждого сг, 1 ^ г < n, V(cri) = t и
б) хотя бы для одного cr, I ^ j ^ п, У(сту) = /. <l na ^кчуг* "'! ^
Проанализируем каждый случай в отдельности. Щ - ,^Л
а) Для каждого а{, где 1 ^ г ^ п, верно, что >■•{.. ;?-)\г
,-UK"f: не я
}) #1^
поэтому V(ip) = t. Следовательно, , .,,,.
ЕСЛИ V(ak -»K + 1-»...К-►¥>)...))=*. т0
Следовательно, (по индукции) ax —> (cr2 —»• (.. .(crn —»• cr)...)) = t.
б) Пусть г — наименьшее натуральное число, для которого верно
V(ar) = f. Тогда
cT _,) =«, то
Vfo.,-» (аг->...К-*>)...)) =
, , = ^К-1) ^ ^(^г - .. .(а„ - V)...) = * -» * = *•
)...)) = t, где fc^r-1, то
= V{ak_x) ~* V(ak _> (fft + 1 - .. .(а„ -><р). .
Следовательно, ах —> (сг2 —»• (.. .(crn —»• a).. .)) = t.
2 Г. Метакиденс, А. Нероуд
34 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Как в случае а), так и в случае б) для любого истинностного озна-
означивания V справедливо соотношение сг, —> (а2 —> (.. .(ап —> а)...)) =
= t. Следовательно, ах —»• {а2 —> (.. .(ап —у а)...)) — тавтология.
(<=) Предположим, что сг, —> (сг2 —»■ (• • ■(<?„ —»■ с). • ■)) — тавтология.
Пусть V — истинностное означивание, такое, что V(cr)=t для
каждого г е {1, 2,..., п}. Если мы предположим, что V(ip) — f, то
Поэтому, если V(ak ->(ak + l->.. .(an -> tp)...)) = t, то
,pr, .,.
Следовательно, V(cr, —> (ст, —* (• • -(^ —> ст)- • •))) = / вопреки тому,
что ох —> (сг2 —> (.. ,(сгп —> сг)...)) — тавтология. П 1.5.8
Следствие 1.5.8 дает нам метод, позволяющий для любой задан-
заданной формулы f установить, является ли она логическим следствием
заданного конечного множества высказываний S: мы проверим за
2" шагов, является ли правая часть пункта 7 тавтологией. Однако
для бесконечного множества высказываний S этот метод потребует
бесконечного числа шагов. В этом случае более уместно воспользо-
воспользоваться семантическими таблицами.
•'г; •■'■ ; u § 1.6. Полнота множеств логических
^•■SS&U*-:'.. связок и нормальные формы "■ S'#S»M,'#V
Нахождение истинностного значения высказывания, доказатель-
доказательство противоречивости или непротиворечивости множества выска-
высказываний в большинстве случаев зависит от числа и типа связок,
содержащихся в высказываниях. Используемые нами пять логиче-
логических связок наиболее часто встречаются в математических текстах.
В этом разделе мы докажем, что произвольное множество логиче-
логических связок выразимо через множество {->, А, V}, и, следовательно,
множества логических связок {->, Л, V} достаточно, чтобы выразить
каждое высказывание логики высказываний (см. [Smu68, Mend64,
Schm60]).
Определение 1.6.1. Множество логических связок Q на-
называется полным, если для каждого высказывания логики выска-
высказываний существует логически эквивалентное ему высказывание,
содержащее только связки из Q. О 1.6.1
Теорема 1.6.2. Множество {->, Л, V} является полным.
Доказательство. Пусть а — о(Ах, А2,..., Ак) — высказы-
высказывание, в котором встречаются только атомы Аи А2,..., Ак. Постро-
Построим сокращенную таблицу истинности а:
§ 1.6. ПОЛНОТА МНОЖЕСТВ ЛОГИЧЕСКИХ СВЯЗОК
35
А,
%
Ay
аК
°*>
Ак
Опк
*к
а(А1; А2,..., Ак)
о»
В этой таблице ащ обозначает соответствующее истинностное
значение в строке п и столбце I, а ап обозначает истинностное
значение высказывания с(А,,..., Ак) в строке п.
1. Предположим, что в последнем столбце найдется хотя бы од-
одно значение t. Докажем, что существует высказывание, содержа-
содержащее только связки -л, Л, V, последний столбец сокращенной табли-
таблицы истинности которого совпадает с последним столбцом указанной
выше таблицы.
Для произвольного атома А обозначим А' сам атом А и А1 —
его отрицание -<А. По строке п построим конъюнкцию
которая содержит только связки -i и Л. Тогда высказывание
является искомым, так как его сокращенная таблица истинности
содержит t в точности в.тех же строках, что и сокращенная таблица
истинности (г(Аи ..., Ак).
2. Если последний столбец не содержит t, то высказывание ложно
и, следовательно, логически эквивалентно А Л->А, где А — произ-
произвольный пропозициональный символ. □ 1.6.2
Используя технику доказательства теоремы 1.6.2, мы можем вы-
выразить произвольное высказывание через связки -i, Л и V. Полу-
Полученное в результате эквивалентное высказывание называется дизъ-
дизъюнктивной нормальной формой (ДНФ).
Пусть F — высказывание, содержащее атомы А,,..., Ап. В об-
общем случае ДНФ формулы F имеет вид
ДНФ^): {Ah Л ... Л Ак) V (A2i Л ... Л Ак) V ... V (А^ Л ... Л Ак),
где Aif е {А„ ..., Ап} или A{j е {-А1(..., -,Л„}, т. е. Atj — атомы
или отрицание атомов F, и в каждой конъюнктивной компоненте
2>
36
Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
встречается каждый атом F либо с отрицанием, либо без
него1).
К
)
Конъюнктивная нормальная форма (КНФ), двойственная к
ДНФ, имеет вид
KJ№(F): (Ah V ... V А, ) Л (А2_ V ... V А2 ) Л ... Л (А^ V ... V Ак ).
Пример 1.6.3. Найдем ДНФ высказывания F, заданного
сокращенной таблицей истинности:
г ,М1
1 •*• , [
1*4
ft*/-
г
л-г
А
t
t
t
t
/
/
/
/
В
t
t
f
f
t
t
f
f
С
t
f
t
f
t
f
t
f
F
t
f
f
f
t
f
f
t
, I ■
9 И', '
"■■«;•
Применим метод, описанный в доказательстве теоремы 1.6.2.
Шаг 1. Находим все строки, содержащие t в последнем столбце.
В нашем случае это строки с номерами 1, 5, 8.
Шаг 2.
ЛA).
□ 1.6.3
Теперь докажем два следствия, устанавливающих полноту кон-
конкретных множеств логических связок.
Следствие 1.6.4. Множества связок Кх — {-i, V} и К2 —
= {->, Л} являются полными.
') Дизъюнктивная нормальная форма, каждый конъюнктивный сомножитель кото-
рои содержит все пропозициональные символы, называется совершенной ДНФ. Как
будет видно в дальнейшем, в общем случае не требуется, чтобы каждый атом входил
в состав конъюнктивного сомножителя ДНФ. Аналогичное замечание относится и к
устройству конъюнктивной нормальной формы (КНФ) — Прим. перев.
§ 1.6. ПОЛНОТА МНОЖЕСТВ ЛОГИЧЕСКИХ СВЯЗОК
37
Доказательство. Используя таблицы истинности, мы мо-
можем доказать, что
В,
А),
А А В =->(->A V-1.B).
Следовательно, каждое высказывание логики высказываний может
быть выражено при помощи связок из множества {-i, V}. Таким
образом, Кх полно.
Аналогично мы можем доказать, что К2 полно.
А -+ В = -iA V В, А^В =(А->В)Л(В -* А),
А V В= i(-.A Л -iB). О 1.6.4
Пример 1.6.5. Наряду со связками ->, Л, V, —»• и <-> мы можем
ввести другие связки, например, | и : , определенные следующими
таблицами истинности:
■it !!■
H-
, - к1
А
t
t
f
f
В
t
f
t
f
A\B
f
t
t
t
A
t
t
f
f
В
t
f
t
f
A :B
f
f
f
t
a 1.6.5
Следствие 1.6.6. Множества связок Е, = {|} и Е2 = {:}
полны.
Доказательство. 1. Докажем полноту Е,. В сущности, А\В
обозначает, что А и В не могут быть одновременно истинными. То-
Тогда А\В = -i(A А В). (Эту эквивалентность легко проверить при
помощи таблиц истинности.) Соотношения А\А = ->(А Л А) = ->А
показывают, что отрицание может быть выражено при помощи связ-
связки |. Для конъюнкции верно, что А Л В = -i-i(A Л В) = ->(А\В) =
= (А\В)\(А\В).
2. Докажем полноту Е2. Мы можем выразить отрицание: ->А =
= -<(А V А) = А : А, и конъюнкцию: А Л В = -i(->A V ~>B) =
= (А:А):(В:В). П 1.6.6
Заметим, что множествами {|} и {: } исчерпываются все одно-
одноэлементные полные множества связок (см. упражнение 20). Кро-
Кроме того, каждое множество логических связок с двумя элементами,
один из которых — -1, а другой — Л, V или —>, является полным (см.
[Schm60, Smul68, Mend64]). , -us н?..
38 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Замечание 1.6.7. Преобразование высказывания а в выска-
высказывание р, логически эквивалентное ему, но содержащее другие
связки, часто бывает полезным. Например, в методе резолюций, ко-
который исследуется в следующих параграфах, мы выражаем импли-
импликации, т. е. высказывания вида а —► р, через связки ->, А и V. При
этом мы используем эквивалентность
АВАВ
проверить которую можно при помощи таблиц истинности.
□ 1.6.7
В последующих параграфах мы опишем используемые в логике
высказываний методы доказательств. Их описание упростит даль-
дальнейший переход к логическому программированию.
§ 1.7. Семантические таблицы
Методы доказательства — это алгоритмические процедуры, сле-
следуя которым мы можем устанавливать, является ли высказывание
тавтологией, и выполнимо ли множество высказываний. Эти методы
разрабатываются в теории автоматического доказательства теорем
и составляют основу логического программирования.
Первый из описанных методов алгоритмического доказательства
использует семантические таблицы. Генцен A909-1945) в 1934 г.
впервые доказал, что все тавтологии могут быть получены приме-
применением некоторых правил, то есть существует некоторая процедура
проверки тавтологичности формул (см. [Юее52, Rault79]). Исполь-
Используя теорию доказательств Бет и Хинтикка в 1955 г. построили ал-
алгоритм, устанавливающий, является высказывание тавтологией или
нет.
При помощи семантических таблиц Бета (далее мы будем их на-
называть просто семантическими таблицами) можно исследовать воз-
возможность того, что данное высказывание принимает значение t или
значение /.
Семантическая таблица составного высказывания К строится ин-
индуктивно, исходя из семантических таблиц высказываний, составля-
составляющих К. Таким образом, мы определим атомарные семантические
таблицы (см. [Smul68, Fitt90]).
Определение 1.7.1. 1. Пусть а — высказывание. Обозна-
Обозначим через fa утверждение «а ложно», а через to — утверждение *а
истинно». При этом to и fo называются помеченными формулами.
2. Атомарные семантические таблицы для высказываний А, ох,
о2 и высказываний, составленных из А, ах и ст2, представлены в
следующей таблице. ,«,^*.*■„», ,\ .-> »■.-.■■ ■;,■;•■•' ivf g: <.,•, \,-r\u''
§ 1.7. СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ
39
la
*
За
5a
/
'■:■•'
;J •
"'
Л
'Л ■
.7)
°
\
<<72
1Л . '!
36
;.; to;«J
55
/(G1 -+ G2)
*Gl
/<72
2a
*(^i Л cr2)
T\
tG2
4a
6a
t{ax i
/
tax
ta2
VG2)
\
\
->CT2)
\
M
/G2
25
/(<^i
M
45
Лсг2)
\
\
/G2
/(cri V cr2)
t
f
65
/
tax
/G2
71
^2
f4G2)
\
M
tCT2
T5
Интуитивно, tA (или fA) можно рассматривать как утверждение
о том, что А истинно (ложно). Как следует из атомарной семантиче-
семантической таблицы 4а, истинность утверждения сг1 V а2 требует истинно-
истинности СГ[ или истинности а2 (т. е. имеет место ветвление), в то время
как из атомарной семантической таблицы 56 следует, что ложность
утверждения ах —> о2 требует истинности ах и ложности о2 (т. е.
в данном случае мы имеем последовательное соединение). Таким
образом, в семантических таблицах ветвление обозначает дизъюнк-
дизъюнкцию, а последовательное соединение — конъюнкцию утверждений.
D 1.7.1
Построение семантической таблицы составного высказывания К
мы начинаем с того, что записываем помеченную формулу tK
или /К в корень семантической таблицы. Затем мы разворачива-
разворачиваем семантическую таблицу К в соответствии с определением 1.7.1.
Прежде, чем определить общие правила построения семантиче-
семантических таблиц, рассмотрим пример.
40
Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
Пример 1.7.2. Пусть К = (AA^A)v(BV(C AD)). В К при-
присутствуют атомы А, В, С и D. Построим семантическую таблицу
с корнем tK.
t((A А -.Л) V {В V (С Л £>)))
4а „
t(A Л -.Л)
2а
t{BV{CAD))
4a/ \,... \
r. • ' г
: Щ : IB
<-f, ;
* . . t(C АШЧ01 :V
■I1" -'t,-
"За"[
fA
4v4 ■.-!■? i..i.to-.; v-.-'i:K.:
i
«3
("»i. M
'.>.>'т.Г- .5 -
i 'Ц v.": . -ЛУ
Это замкнутая семантическая таблица, содержащая три ветви,
а именно, три последовательности хх, Zj и х3. Ветви произраста-
произрастают из корня. Левая ветвь х,, противоречива, так как она содержит
противоречащие друг другу помеченные формулы tА и /А. Проти-
Противоречивая ветвь помечается внизу символом <g>. Две другие ветви
не являются противоречивыми.
Из семантической таблицы К мы можем заключить, что гипотеза
tK правильна при некоторых условиях, например, при выполнении
tB (ветвь Zj) или выполнении tC и tD (ветвь Xj).
Однако иногда она ложна.
Несложно выделить из семантической таблицы К
составляющие ее атомарные семантические табли-
таблицы. Например, ограниченная прямоугольником из то-
I чек семантическая таблица является атомарной се-
t(->A) мантической таблицей 2а. D 1.7.2
Теперь мы сформулируем понятия, необходимые
для построения семантических таблиц.
Определение 1.7.3. 1. Вершинами семантической табли-
таблицы называются все помеченные формулы, встречающиеся в этой
таблице.
t(A Л -А)
tA
§1.7. СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ 41
2. Вершина семантической таблицы называется особой, если она
встречается как корень некоторой атомарной семантической табли-
таблицы. В противном случае, вершина называется обычной.
3. Ветвь семантической таблицы называется противоречивой, ес-
если для некоторого высказывания а помеченные формулы to и fa
являются вершинами этой ветви.
4. Семантическая таблица называется замкнутой, если каждая
непротиворечивая ее ветвь не содержит обычных вершин. В про-
противном случае, семантическая таблица называется незамкнутой.
5. Семантическая таблица противоречива, если каждая ее ветвь
противоречива. D 1.7.3
Определение 1.7.4 (индуктивное определение семантиче-
семантической таблицы). Построим семантическую таблицу высказыва-
высказывания К следующим образом.
Вначале помещаем помеченную формулу tK (или /К) в корень.
Затем продолжаем построение по индукции.
Шаг п . Пусть мы уже построили семантическую таблицу Тп,
Шаг п + 1 . Расширим семантическую таблицу Тп до семантиче-
семантической таблицы Тп + 1. При этом мы пользуемся некоторой вершиной
семантической таблицы Тп, которую в дальнейшем не будем исполь-
использовать. Из всех обычных вершин Тп, ближайших к корню, выбираем
самую левую. Обозначим выбранную вершину X.
К концу каждой непротиворечивой ветви семантической таблицы
Тп мы присоединяем атомарную семантическую таблицу, имеющую
корнем X. (При этом вершина X становится особой вершиной.) В
результате получаем семантическую таблицу Тп +1 (как правило, мы
не записываем саму вершину X, так как она уже присутствует в
каждой из рассматриваемых непротиворечивых ветвей).
Построение заканчивается, если каждая непротиворечивая ветвь
не содержит обычных вершин. □ 1.7.4
Поясним описанную методику на примере построения противоре-
противоречивой семантической таблицы.
Пример 1.7.5. Рассмотрим закон Пирса ((А —у В)—у А) —> А.
1. В корень таблицы мы помещаем утверждение о том, что выска-
высказывание ((А—у В)—у А)—у А ложно. (См. рис. 1.1) Предположение о
ложности закона Пирса приводит нас к построению противоречивой
семантической таблицы. Следовательно, соответствующая формула
истинна.
2. Если бы мы поместили в корень семантической таблицы утвер-
утверждения о том, что закон Пирса истинен, то заключение осталось
бы таким же. (См. рис. 1.2.) Заметим, что в этой семантической
таблице нет противоречивых ветвей. Для каждой из трех альтерна-
альтернатив /А, или tB и /А, или tA утверждение ((А —у В)—* А)—у А)
42
Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
f((A -4 В) -4 A) -4 A)
ЩА ->B)-¥A)
■f,- ■ • • '■,...-■.0 ■< •'■ .-.1 ■
fA
tA
i W
•.*,■•.>•;;•■
<A
/a
t(A -* B)
fA ;.
:: И •■ 'f'-. V !■,'.;*5'0-* )
"■се i-t '.ь-'.»-. ■.■<■;',k;.-I f-- , М-.Г
<УА
tB
Рис. 1.1
i ',t,^
Рис. 1.2
' ; ili
■i1
истинно. Даже в случае /В одно из утверждений tA или /Л имеет
место. Следовательно, закон Пирса логически истинен. □ 1.7.5
Итак: если замкнутая семантическая таблица с /К в корне
противоречива (а это означает, что мы пытались всеми воз-
возможными способами сделать высказывание К ложным и не су-
сумели), то К —тавтология.
В следующем определении 1.7.6 этот замысел представлен более
формально.
Определение 1.7.6. Доказательством, или выводом по
Бету высказывания К называется замкнутая противоречивая се-
семантическая таблица, в корне которой помещена помеченная фор-
формула /К. Замкнутая противоречивая таблица, имеющая в качестве
корня tK называется опровержением по Бету высказывания К.
Говорят, что высказывание К доказуемо, или выводимо по Бе-
Бету, если оно имеет доказательство по Бету. Высказывание К
называется опровержимым по Бету, если существует опроверже-
опровержение К по Бету. Тот факт, что К доказуемо по Бету, обозначается
\-в К. П 1.7.6
Как мы докажем в теореме 1.10.7 и теореме 1.10.9, каждая тав-
тавтология доказуема по Бету (полнота доказательств по Бету) и, на-
наоборот, каждое доказуемое по Бету высказывание есть тавтология
(корректность доказательств по Бету). ,-. , j.;. ■*,• v\-; й?л, J'\ зъ
§ 1.7. СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ 43
Пример 1.7.7. Предположим, что истинны высказывания:
1: Джордж любит Марию, или Джордж любит Екатерину;
2: Если Джордж любит Марию, то он любит Екатерину.
Кого же Джордж любит?
Обозначим символом М высказывание «Джордж любит Марию»
и символом К высказывание «Джордж любит Екатерину». Тогда вы-
высказывание 1 эквивалентно MV К, а высказывание 2 эквивалентно
М —* К и, следовательно, ^М У К. Конъюнкцию высказываний 1
и 2, то есть (М V К) А (->М V К), обозначим А. По условию при-
примера предполагается, что А истинно. Мы хотим узнать, любит ли
Джордж Екатерину, или, говоря формально, верно ли tK. Предпо-
Предположим, что он ее не любит, то есть верно fK. Мы можем построить
семантическую таблицу с корнем /К. .
С л'
V ib>
.' !
> «
\
1 4
t((M
h
г ■
1 U ,<
fK
VK)A (iAf
<(M V /f)
f(nM V /f)
vjo)
U i
Ф.
-•+*■
n /
.p,
i
tK ; s. tM
На шаге 2 мы присоединили t((MvK)A(->MvК)), так как 1 и 2
даны истинными. Начав построение таблицы с корнем fK, мы полу-
получили противоречивую таблицу. Это означает, что высказывание К
всегда истинно, другими словами, Джордж любит Екатерину!
Если бы мы построили семантическую таблицу с помеченной фор-
формулой /М в корне, то получили бы непротиворечивую таблицу, и,
следовательно, не могли бы заключить, любит Джордж Марию или
нет! □ 1.7.7
44 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
§ 1.8. Аксиоматическая система вывода
Логика высказываний, подобно другим математическим системам,
может быть представлена как аксиоматическая система с логиче-
логическими аксиомами и правилами вывода. Аксиомы — это некоторые
тавтологии, правило вывода R выводит высказывание а из после-
последовательности высказываний ст,, ст2,..., ап. Мы опишем вкратце ак-
аксиоматическое представление логики высказываний (см. [Schm60,
RaSi7O, Mend64]).
Определение 1.8.1 (аксиомы). Каждое высказывание сле-
следующего вида является аксиомой. . ■•■*•■
1. уз->(Т->уз). UM?'.:V ' .■О»'7».-МГИГ.У9Э
2. (уз -»{г -» а)) -> ((уз -> г) -> (уз -> а)).
3. (->уз —> -it) —> (т —> уз).
Заметим, что высказывания уз, т и ст могут быть произвольны-
произвольными. Таким образом, мы описали схемы аксиом, из которых можно
получить неограниченное число аксиом. Легко проверить, что все
эти аксиомы являются правильно построенными формулами логики
высказываний и, конечно, тавтологиями. □ 1.8.1
Определение 1.8.2 (правило вывода Modus Ponens). Мы
будем использовать только одно правило вывода, правило Modus
Ponens, которое утверждает, что высказывание т выводится из вы-
высказываний уз и уз —> т. Правило Modus Ponens1) своим названием
обязано Диогену Лаэртскому (Diogenes Laertius), см. [Zeno]. Оно
обозначается следующим образом:
или .. ■ . *" ■ '{ *" " ■■* ••■
уз, уз^тКт '■ ■■• B)
В A), типичном определении логического правила, горизонталь-
горизонтальная линия отделяет гипотезы от заключения. В B) символ Ь- обозна-
обозначает выводимость в аксиоматической системе. Мы рассматриваем
три аксиомы определения 1.8.1 как формулы, выводимые в аксио-
аксиоматической системе. Новые высказывания получаются при помощи
этих трех аксиом и правила Modus Ponens. В следующем примере
1.8.3 демонстрируется, как можно применить аксиомы и правило
Modus Ponens для вывода формулы логики высказываний А —> А.
1) В русской математической литературе это правило иазывают правилом заклю-
заключения. — Прим. перев.
§ 1.8. АКСИОМАТИЧЕСКАЯ СИСТЕМА ВЫВОДА
Пример 1.8.3. Докажем, что Ь А —> А. ч,'.„'ьл,' I
Доказательство. Сначала возьмем первую щриому а
\-А->«В->А)->А). *^*?' A)
Вторую аксиому запишем в виде •* К *—:'^3)
h (Л -»((Я -> Л) -> Л) -» (((А -> (Я -> Л)) -> (Л -> А)). B)
Из A) и B) по правилу Modus Ponens получаем, что
+(А-+А). C)
Используя вновь первую аксиому А —> (В —> Л), по правилу Modus
Ponens заключаем, что Ь .А —>А. Следовательно, высказывание
А —> А выводимо в нашей аксиоматической системе. П 1.8.3
Следующая теорема 1.8.4 позволяет производить в высказывани-
высказываниях замену одних подформул на другие, логически им эквивалентные.
Доказательство теоремы можно найти в упражнении 22.
Теорема 1.8.4 (подстановка эквивалентных формул). Пусть
высказывание а+->а1 выводимо в PL, ст —подформула высказыва-
высказывания ip, и высказывание <р{ получено в результате подстановки
в высказывание у вместо некоторых вхождений формулы а эк-
эквивалентной ей формулы ст,. Тогда высказывание <р +-> <р1 также
выводимо в PL. Формально записываем:
\- а *-> а{ =$> \- tp +-+ <рг О 1.8.4
Теперь мы приведем формальное определение доказательства вы-
высказывания аксиоматическим методом.
Определение 1.8.5. Пусть 5 — множество высказываний.
1. Доказательством, или выводом из 5 называется такая конеч-
конечная последовательность высказываний ст,, ст2,..., ап, что для каждо-
каждого 1 ^ i^ n верно:
а) oi принадлежит 5, или
б) ai — аксиома, или
в) ai получено из ар ак, где 1 ^j, к ^ i, по правилу Modus Ponens.
2. Высказывание а называется доказуемым, или выводимым из
множества высказываний S, если существует такое доказатель-
доказательство ст,, а2,..., ап из 5, что ап совпадает с а. Для обозначения
выводимости высказывания а из множества высказываний 5 будем
использовать запись 5 h ст.
3. Высказывание ст называется доказуемым, или выводимым, ес-
если Ь ст, то есть ст выводимо в аксиоматической системе определе-
определения 1.8.1 при помощи правила Modus Ponens. Отметим, что если
46 Глава 1. ЛОГИКА ВЫСКАЗЫВАНИЙ
5 = 0, то понятие выводимого из множества 5 высказывания со-
совпадает с понятием выводимого высказывания. □ 1.8.5
Пример 1.8.6. Выведем ->В —> (С —» А) из 5 — {А}. Имеем:
1) A —AeS;
2) А —>(С —* А) — аксиома 1; ', •&•, ••■ . .., -, ;,*г>ж<.;
3) С —> А —Modus Ponens к 1 и 2; ' ., ,:t ; ,
4) (С-► А)->(-.£-> (С-> А)) —аксиома 1; ' - .^'-; ^ <;*п
5) -.Я->(С->Л) — Modus Ponens к 3 и 4. □ 1.8.6
Заметим, что если а выводимо из 5 и 5 — бесконечное множе-
множество, то а выводимо из некоторого конечного подмножества S, так
как доказательство всегда конечно.
Следующая теорема 1.8.7 является основной в теории доказа-
доказательств.
Теорема 1.8.7 (теорема дедукции). Пусть S —множество
высказываний; K,L— высказывания. Тогда : < ■
SU{K}\-L <* ShK^L. \:«b*iv ;
Доказательство. (-<=) Предположим S \- К —* L. Рассмо-
Рассмотрим доказательство ст,, а2,..., ап формулы К —> L, в котором ап
есть сама формула К —> L, и для каждого г е {1,..., п} либо ai —
аксиома, либо а{ е 5, либо а{ выводится из двух предшествую-
предшествующих высказываний с использованием правила Modus Ponens. То-
Тогда последовательность аи а2, ..., ап, <тп + 1, сгп + 2, где стп + 1 есть К,
а сгп + 2 есть L, является доказательством L, так как для каждого
г £ {1,..., п, п+1} либо а{ — аксиома, либо а{ G Su{K}, либо а{ вы-
выводится из двух предшествующих высказываний с использованием
правила Modus Ponens, «тп + 2 выводится из ап и орп + 1 с использова-
использованием правила Modus Ponens.
(=Ф>) Мы знаем, что существует доказательство L из 5 U {К}.
Обозначим его через L,, L2,..., Ln, где Ln есть L. Рассмотрим
последовательность высказываний
Эта последовательность не является доказательством. Однако, она
превратится в доказательство, если мы дополним ее высказывания-
высказываниями, полученными следующим индуктивным методом.
Для L [ возможны три случая: L { — аксиома, либо L { принадле-
принадлежит 5, либо Lj есть К.
Высказывание L, —> (if —> L,) — аксиома 1. Поэтому в первых
двух случаях мы запищем L, и L, —> (К —* L{) перед К —* L,. В
последнем случае теорема верна (пример 1.8.3).
Предположим, что мы дополнили последовательность вплоть до
высказывания К —> Lm таким образом, что первые m элементов
§ 1.8. АКСИОМАТИЧЕСКАЯ СИСТЕМА ВЫВОДА 47
последовательности вместе с дополняющими ее элементами состав-
составляют доказательство К —> Lm.
Тогда мы запишем между К —> Lm и К —> Lm + l еще v высказы-
высказываний так, что первые т + 1 элементов последовательности вместе
дополняющими ее элементами составят доказательство К —> Lm + l.
Высказывание Lm + l либо аксиома, либо принадлежит S, л:;бо
есть К, либо получено из L jt Lk (I < j, к ^ m) по правилу Modus
Ponens. Другими словами, Lk имеет вид Li —> Lm + r
В первых трех случаях мы поступаем аналогично тому, как посту-
поступали выше, то есть записываем между К —»Lm и К —>Lm+l выска-
высказывания Lm + l и Lm + l —>(K—>Lm+1). В четвертом случае по индук-
индуктивному предположению первые т элементов последовательности
вместе с дополняющими ее элементами составляют доказательства
К —> L} и К —> (Lj. —> im + 1). Дополним последовательность выска-
высказыванием
представляющим собой аксиому 2.
Тогда К -*Lm+l можно вывести, если дважды последовательно
применить правило Modus Ponens. Заметим, что при доказательст-
доказательстве теоремы дедукции мы использовали только две из трех аксиом
аксиоматической системы. D 1.8.7
Аксиомы логики высказываний часто называют логическими ак-
аксиомами. Обычно мы определяем теорию, расширяя аксиоматиза-
аксиоматизацию логики высказываний множеством S дополнительных аксиом,
которые характеризуют теорию. Теоремы теории 5 являются эле-
элементами множества {tp: S\- <p} (см. замечание 1.8.8).
Замечание 1.8.8. 1. Аксиоматическая система. Аксиомы
PL и правило Modus Ponens составляют аксиоматическую систему
Фреге-Лукашевича (см. [Heij67, Boye68, Schm60]). Фреге (Frege,
1898 - 1925) стал первым, кто определил формальный язык, подхо-
подходящий для логики. Лукашевич (Lukasiewicz, 1878 - 1926) разрабо-
разработал аксиоматизацию логики высказываний.
2. Modus Ponens. Если а и а —> т доказуемы по Бету, то а и а —> т
логически истинны, следовательно, г также логически истинно (по-
(почему?). Известен алгоритмический метод, позволяющий строить до-
доказательство по Бету высказывания т из доказательств по Бету вы-
высказываний GИ(т->т. Этот метод применяется в теореме Генцена,
однако его доказательство выходит за рамки этой книги.
3. Теоремы. Теоремой является любое высказывание, присутству-
присутствующее в доказательстве. Это означает, что теоремы теории 5 — это
в точности элементы множества высказываний {a: S Ь- ст}. Обычно
мы считаем заключением последнее высказывание доказательства,
однако, фактически, каждый начальный фрагмент доказательства
также является доказательством, j,,» •? /.жм-.л л