«С. В. СУДОПЛАТОВ, Е. В. ОВЧИННИКОВА МАТЕМАТИЧЕСКАЯ ЛОГИКА И ТЕОРИЯ АЛГОРИТМОВ УЧЕБНИК для дистанционного образования НОВОСИБИРСК 2006 Рецензенты: А. Г. Пинус д-р физ.-мат. наук, проф.; В. М. Зыбарев канд. техн.наук, ...»

Министерство образования и науки Российской Федерации

НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ

ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ

С. В. СУДОПЛАТОВ, Е. В. ОВЧИННИКОВА

МАТЕМАТИЧЕСКАЯ ЛОГИКА

И ТЕОРИЯ АЛГОРИТМОВ

УЧЕБНИК

для дистанционного образования

НОВОСИБИРСК

2006 Рецензенты: А. Г. Пинус д-р физ.-мат. наук, проф.;

В. М. Зыбарев канд. техн.наук, доц.

Сергей Владимирович Судоплатов Елена Викторовна Овчинникова Математическая логика и теория алгоритмов В книге излагаются основные классические исчисления математической логики: исчисления высказываний и исчисления предикатов, а также элементы теории алгоритмов и неклассических логик.

Книга предназначена для студентов технических вузов, изучающих математическую логику и теорию алгоритмов в рамках дистанционного образования.

c Судоплатов С.В., Овчинникова Е.В., 2006.

Оглавление Предисловие Г л а в а 1. Исчисления высказываний § 1.1. Определение формального исчисления...................... § 1.2. Исчисление высказываний генценовского типа................................. § 1.3. Эквивалентность формул............................. § 1.4. Нормальные формы................................. § 1.5. Семантика исчисления секвенций......................... § 1.6. Исчисление высказываний гильбертовского типа................ § 1.7. Алгоритмы проверки общезначимости и противоречивости в ИВ..... § 1.8. Логические задачи................................. § 1.9. Задачи и упражнения................................ Г л а в а 2. Логика и исчисление предикатов § 2.1. Формулы сигнатуры. Истинность формулы на алгебраической системе. § 2.2. Секвенциальное исчисление предикатов..................... § 2.3. Эквивалентность формул в ИПC........................ § 2.4. Нормальные формы................................. § 2.5. Теорема о существовании модели......................... § 2.6. Исчисление предикатов гильбертовского типа................. § 2.7. Скулемизация алгебраических систем...................... § 2.8. Метод резолюций в исчислении предикатов................... § 2.9. Логические программы............................... § 2.10. Элементарные теории................................ § 2.11. Типы. Основные классы моделей......................... § 2.12. Категоричность. Спектры моделей полных теорий............... § 2.13. Система аксиом арифметики Пеано.

Нестандартные модели арифметики....................... § 2.14. Задачи и упражнения................................ Г л а в а 3. Элементы теории алгоритмов § 3.1. Машины Тьюринга................................. § 3.2. Рекурсивные функции и отношения....................... § 3.3. Эквивалентность моделей алгоритмов...................... § 3.4. Универсальные частично рекурсивные функции. Теорема Райса..... § 3.5. Неразрешимость исчисления предикатов. Теорема Гделя о неполноте.

е Разрешимые и неразрешимые теории...................... § 3.6. Характеристики сложности алгоритмов..................... § 3.7. Задачи и упражнения................................ Г л а в а 4. Неклассические логики § 4.1. Пропозициональные логики............................ § 4.2. Предикатные логики................................ § 4.3. Предикатные временные логики и их приложение к программированию..................... § 4.4. Алгоритмические логики.............................. § 4.5. Задачи и упражнения................................ Варианты контрольной работы

ПРЕДИСЛОВИЕ

Книга предназначена для студентов младших курсов технических вузов, изучающих математическую логику и теорию алгоритмов дистанционно, и написана на основе учебника Судоплатов С. В., Овчинникова Е. В. Математическая логика и теория алгоритмов: Учебник М.:ИНФРА-М, Новосибирск: Изд-во НГТУ, 2004, доступного через библиотеку НГТУ, киоск НГТУ или Интернет-магазины России.

Материал учебника составлен в соответствии с рабочими программами курсов математической логики и теории алгоритмов, читаемых в НГТУ, и опирается на учебник Судоплатов С. В., Овчинникова Е. В.

Дискретная математика : Учебник М.:ИНФРА-М, Новосибирск:

Изд-во НГТУ, 2005.

Учебник включает четыре раздела: исчисления высказываний, логика и исчисления предикатов, элементы теории алгоритмов, неклассические логики. В конце книги приведены варианты контрольной работы.

Вариант N контрольной работы студента вычисляется по формуле N = k + 25 · m, где k число, состоящее из последних двух цифр личного шифра студента, а целое число m выбирается так, чтобы значение N находилось в пределах от 1 до 25.

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

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

Глава

ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

§ 1.1. Определение формального исчисления Введем общее понятие формального исчисления. Будем говорить, что формальное исчисление I определено, если выполняются следующие четыре условия:

1. Имеется некоторое множество A(I) алфавит исчисления I.

Элементы алфавита A(I) называются символами. Конечные последовательности символов называются словами исчисления I. Обозначим через W (I) множество всех слов алфавита исчисления I.

2. Задано подмножество E(I) W (I), называемое множеством выражений исчисления I. Элементы множества E(I) называются формулами или секвенциями.

3. Выделено множество Ax(I) E(I) выражений исчисления I, называемых аксиомами исчисления I.

4. Имеется конечное множество R(I) частичных операций R1, R2,..., Rn на множестве E(I), называемых правилами вывода исчисления I.

Итак, исчисление I есть четверка A(I), E(I), Ax(I), R(I).

Если набор выражений (1,..., m, ) принадлежит правилу Ri, то выражения 1,..., m называются посылками, а выражение непосредственным следствием выражений 1,..., m по правилу Ri, или заключением правила Ri. Записываться этот факт будет следующим образом:

Иногда в этой записи символ i будет опускаться, если из контекста ясно, о каком правиле идет речь:

Выводом в исчислении I называется последовательность выражений 1, 2,..., n такая, что для любого i (1 i n) выражение i есть либо аксиома исчисления I, либо непосредственное следствие каких-либо предыдущих выражений.

Выражение называется теоремой исчисления I, выводимым в I или доказуемым в I, если существует вывод 1,..., n,, который называется выводом выражения или доказательством теоремы.

П р и м е р 1.1.1. 1. Пусть E(I) множество повествовательных предложений русского языка, Ax(I) множество истинных в данный момент времени предложений вида “подлежащее сказуемое” с точкой на конце. Имея правила вывода можно из простых предложений (аксиом) составлять более сложные (теоремы), также истинные в данный момент времени.

2. Пусть E(I) множество программ Pf, производящих вычисления значений одноместных числовых функций f, Ax(I) множество “простых” программ. Для программ Pf, Pg E(I) обозначим через Pf Pg программу, составленную из программ Pf и Pg так, что по любым начальным данным производятся вычисления значений функции f, а затем полученные значения используются как начальные данные, по которым вычисляется значение функции g. Правило вывода позволяет задать формальное исчисление, в котором из простых программ (аксиом) можно составлять более сложные (теоремы).

Вообще говоря, может не существовать алгоритма, с помощью которого для произвольного выражения формального исчисления I за конечное число шагов можно определить, является ли выводимым в I или нет. Если такой алгоритм существует, то исчисление называется разрешимым, а если такого алгоритма нет неразрешимым.

Исчисление называется непротиворечивым, если не все его выражения доказуемы.

Ниже мы проведем построение двух формальных исчислений исчислений высказываний, в основе которых лежат формулы алгебры логики. Первое из этих исчислений исчисление высказываний генценовского типа, предложенное Генценом, в качестве выражений использует секвенции, построенные из формул алгебры логики. Это исчисление будет обозначаться через ИС. Второе исчисление исчисление высказываний гильбертовского типа, создано Гильбертом, и в нем выражениями являются непосредственно формулы алгебры логики. Исчисление высказываний гильбертовского типа будет обозначаться через ИВ.

Мы покажем, что оба исчисления эквивалентны в том смысле, что доказуемыми в них будут являться в точности тождественно истинные формулы. Из последнего факта будут вытекать разрешимость и непротиворечивость исчислений высказываний.

Строящиеся в дальнейшем исчисления ИПС и ИП, являющиеся расширениями исчислений ИС и ИВ соответственно, послужат примерами неразрешимых непротиворечивых исчислений.

§ 1.2. Исчисление высказываний генценовского типа Определим элементы исчисления высказываний ИС.

Алфавит ИС состоит из букв A, B, Q, P, R и других, возможно, с индексами (которые называются пропозициональными переменными), логических символов (связок) отрицания ¬, конъюнкции, дизъюнкции, импликации, следования, а также вспомогательных символов: левой скобки (, правой скобки ), запятой,.

Множество формул ИС определяется индуктивно:

а) все пропозициональные переменные являются формулами ИС (такие формулы называются элементарными или атомарными);

формулы ИС;

в) выражение является формулой ИС тогда и только тогда, когда это может быть установлено с помощью пунктов “а” и “б”.

Таким образом, любая формула ИС строится из пропозициональных переменных с помощью связок ¬,,,.

В дальнейшем при записи формул будем опускать некоторые скобки, используя те же соглашения, что и в алгебре логики.

Секвенциями называются конечные выражения следующих двух видов, где 1,..., n, формулы ИС:

1,..., n (“из истинности 1,..., n следует ”), 1,..., n (“система формул 1,..., n противоречива”).

Последовательности формул 1,..., n в секвенциях будут часто обозначаться через (возможно, с индексами):,. При этом последовательность считается пустой при n = 0. Значит, записи и также являются секвенциями, первая из которых может читаться как утверждение о доказуемости формулы. Смысл секвенции будет указан в § 1.5.

Таким образом, наряду с формулами, символизирующими простые или сложные высказывания, секвенции являются записями утверждений, в которых выделяются посылки и заключение.

Множество аксиом ИС определяется следующей схемой секвенций:

, где произвольная формула ИС.

Аксиомами являются, например, секвенции A ¬B A ¬B и Правила вывода ИС задаются следующими записями, где, произвольные (возможно пустые) конечные последовательности формул ИС,,, произвольные формулы ИС.

двух случаев).

9. (удаление ¬, или доказательство от противного).

12. (утончение, или правило лишней посылки).

Вывод S0,..., Sn в ИС называется линейным доказательством. Секвенция S называется доказуемой в ИС, или теоремой ИС, если существует линейное доказательство S0,..., Sn в ИС, заканчивающееся секвенцией S: Sn = S. Формула называется доказуемой в ИС, если в ИС доказуема секвенция.

Определим по индукции понятие дерева секвенций:

1) любая секвенция является деревом секвенций;

2) если D0,..., Dn деревья секвенций и S секвенция, то запись также является деревом секвенций;

3) любое дерево секвенций строится в соответствии с пп. 1 и 2.

Вхождением секвенции в дерево D называется место, которое секвенция занимает в дереве. Каждая секвенция может иметь несколько вхождений в дерево секвенций. Вхождение секвенции в дерево D, над (под) которым нет горизонтальной черты, называется начальным (соответственно заключительным).

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

Часть дерева, состоящая из секвенций, находящихся непосредственно над некоторой чертой, под той же чертой, а также самой черты, называется переходом.

Дерево D называется доказательством в ИС в виде дерева, если все его начальные секвенции суть аксиомы ИС, а переходы осуществляются по правилам 1–12. Дерево D называется доказательством секвенции S в виде дерева в ИС, или деревом вывода S в ИС, если D доказательство в ИС и S его заключительная секвенция.

Наличие линейного доказательства секвенции равносильно существованию доказательства секвенции в виде дерева:

Предложение 1.2.1. Секвенция S имеет доказательство в ИС в виде дерева тогда и только тогда, когда S теорема ИС.

Очевидно, что представление доказательства в виде дерева более наглядно и позволяет проследить все переходы по правилам вывода.

П р и м е р 1.2.1. 1. Следующее дерево демонстрирует доказуемость формулы ¬ для любой формулы :

для любых формул и :

мости в ИС секвенций S0,..., Sn следует выводимость в ИС секвенции Заметим, что допустимость правила равносильна тому, что его добавление в исчисление ИС не расширяет множество доказуемых секвенций.

Предложение 1.2.2. Следующие правила допустимы в ИС:

где в пп. (а) и (б) выполняется {1,..., m } {1,..., n };

(з) (выведение из противоречия);

Д о к а з а т е л ь с т в о. Допустимость правила показывается следующим деревом:

Допустимость правила (а) следует из допустимости указанного правила с помощью правил 11 и 12. Допустимость правила (б) вытекает из правил (а), (ж) и (з).

Докажем допустимость правила (з), а остальные правила оставим читателю в качестве упражнения.

Ясно, что секвенция может быть получена лишь применением правила 10. Поэтому из доказуемости секвенции следует доказуемость секвенций и ¬ для некоторой формулы. Учитывая доказуемость последних секвенций, дерево устанавливает доказуемость секвенции.

Использование допустимых правил вывода позволяет во многих случаях приводить сокращенные доказательства секвенций, которые при необходимости можно преобразовать в доказательства секвенций в виде деревьев в ИС.

Например, следующее дерево устанавливает доказуемость секвенции ( ), ¬ ¬:

Правило называется равносильным, если доказуемость (единственной) секвенции, стоящей над чертой, равносильна доказуемости секвенции, стоящей под чертой. Из предложения 1.2.2 вытекает, что следующие правила равносильны: 9, 11, (г), (д), (ж), (и), (к), (л), (м), (н), (о).

Пусть V = {Pi | i } множество всех пропозициональных переменных ИС, F множество всех формул ИС. Любая функция s : V F называется подстановкой пропозициональных переменных. Для любой формулы F обозначим через s() формулу, получающуюся из заменой всех пропозициональных переменных P, входящих в, на формулы s(P ).

¬P0 P1, то s() = ¬(P1 ¬P2 ) (P1 ¬P3 ).

Для любой секвенции (последовательности формул) R обозначим через s(R) секвенцию (последовательность формул), получающуюся из R заменой всех пропозициональных переменных P, входящих в R, на формулы s(P ).

Таким образом, отображение s естественным образом расширяется на множество всех выражений исчисления ИС.

Следующая теорема утверждает, что подстановкой в доказуемую секвенцию произвольных формул вместо пропозициональных переменных получается также доказуемая секвенция.

Теорема 1.2.3. (теорема о подстановке). Если s подстановка, R секвенция, то допустимое правило.

§ 1.3. Эквивалентность формул Для любых формул и ИС обозначим через ( ) формулу ИС (( ) ( )). Напомним, что таблица истинности последней формулы совпадает с таблицей истинности формулы алгебры логики ( ).

Лемма 1.3.1. Секвенция ( ) доказуема тогда и только тогда, когда доказуемы секвенции, и,.

Д о к а з а т е л ь с т в о. Предположим, что секвенция ( ) доказуема. Тогда доказуемость секвенции, устанавливается следующим деревом:

Доказуемость секвенции, показывается аналогично.

Установим теперь доказуемость секвенции ( ), предполагая, что секвенции, и, доказуемы:

Формулы и называются эквивалентными (обозначается ), если в ИС доказуемы секвенции и.

В силу леммы 1.3.2 условие равносильно доказуемости секвенции ( ). Покажем, что отношение образует отношение эквивалентности на множестве формул.

Лемма 1.3.2. Для любых формул, и исчисления ИС справедливы следующие утверждения:

Д о к а з а т е л ь с т в о. В пункте (а) доказывать нечего, поскольку аксиома. Пункт (б) следует из симметричности в определении отношения. Пункт (в) вытекает из правила сечения (предложение 1.2.2, в).

Установим, что эквивалентность формул сохраняется под действием операций ¬,, и.

Д о к а з а т е л ь с т в о. В силу симметричности отношения достаточно доказать секвенции ¬1 ¬1, (1 2 ) (1 2 ), ( 2 ) (1 2 ) и (1 2 ) (1 2 ), а доказуемость этих секвенций устанавливается следующими деревьями:

Формула исчисления ИС называется подформулой формулы исчисления ИС, если является подсловом слова. Место, которое занимает подформула в формуле, называется вхождением в формулу.

П р и м е р 1.3.1. Формула A имеет два вхождения в формулу, имеющую вид A (A B C) D. Следующие формулы образуют множество всех подформул формулы : A, B, C, D, B C, A B C, Теорема 1.3.4. (теорема о замене). Пусть формула исчисления ИС, ее подформула, а формула получается из заменой некоторого вхождения на формулу. Тогда если, то Д о к а з а т е л ь с т в о. Если =, то доказывать нечего. Если =, то используем индукцию по числу шагов построения формулы. Предполагая, что пропозициональная переменная, снова получаем =. Индукционный переход осуществляется рассмотрением В каждом из этих случаев формула входит в 1 или 2. Поэтому эквивалентность вытекает из индукционного предположения и леммы 1.3.3.

§ 1.4. Нормальные формы В этом параграфе мы покажем, что преобразования формул алгебры логики, приводящие к построению дизъюнктивных и конъюнктивных нормальных форм, имеют место и в исчислении секвенций.

Лемма 1.4.1. Пусть, и формулы ИС. Тогда справедливы следующие эквивалентности:

(а) () (), () () (ассоциативность (законы дистрибутивности);

(ж) ¬¬ (закон двойного отрицания);

остальные утверждения читателю в качестве упражнения:

(), ()(); (), ()();

Напомним, что литерой называется любая атомарная формула A, обозначаемая через A1, или ее отрицание ¬A, которое обозначается через A0. Конъюнктом (дизъюнктом) называется литера или конъюнкция (соответственно дизъюнкция) литер. Конъюнкт или дизъюнкция конъюнктов называется дизъюнктивной нормальной формой (ДНФ), а дизъюнкт или конъюнкция дизъюнктов конъюнктивной нормальной формой (КНФ).

Следующая теорема является аналогом теоремы о приведении формул алгебры логики к дизъюнктивным и конъюнктивным нормальным формам.

Теорема 1.4.2. Любая формула ИС эквивалентна некоторой ДНФ и некоторой КНФ.

Алгоритм приведения формулы ИС к ДНФ аналогичен алгоритму приведения формул алгебры логики к ДНФ и опирается на лемму 1.4.1.

1. Выражаем согласно пункту (з) леммы 1.4.1 все импликации, участвующие в построении формулы, через дизъюнкции и отрицания.

2. Используя законы де Моргана (лемма 1.4.1, п. (е)), переносим все отрицания к переменным и сокращаем двойные отрицания по закону двойного отрицания (лемма 1.4.1, п. (ж)).

3. Используя закон дистрибутивности ( ) ( ) ( ), преобразуем формулу так, чтобы все конъюнкции выполнялись раньше дизъюнкций.

В результате применения пп. 1–3 получается ДНФ данной формулы.

Приведение формулы к КНФ производится аналогично приведению ее к ДНФ c применением закона дистрибутивности ( ) ( § 1.5. Семантика исчисления секвенций Пусть X некоторое множество, fX отображение, которое каждой пропозициональной переменной ставит в соответствие некоторое подмножество множества X. Расширим по индукции отображение fX до отображения множества формул ИС в булеан P(X) множества X согласно следующим соотношениям:

Любое такое отображение fX, действующее на множестве формул ИС, называется интерпретацией ИС в X.

Каждой секвенции S следующим образом ставится в соответствие некоторое утверждение fX (S) о подмножествах X:

Теорема 1.5.1. Для любой интерпретации fX ИС и любой доказуемой в ИС секвенции S справедливо утверждение fX (S).

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

Покажем, как проверяются указанные переходы на примере первого правила вывода i= Проверка остальных переходов аналогична и предоставляется читателю.

Следствие 1.5.2. Исчисление ИС непротиворечиво.

Д о к а з а т е л ь с т в о. Пусть X непустое множество, fX произвольная интерпретация ИС, A некоторая атомарная формула.

Покажем, что формула A ¬A не доказуема в ИС. Действительно, fX (A ¬A) = fX (A) (X \ fX (A)) =, откуда с учетом непустоты множества X следует, что утверждение fX ( A ¬A) ложно. Тогда по теореме 1.5.1 секвенция A ¬A не доказуема.

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

Определим теперь так называемую главную интерпретацию ИС, которая позволяет составлять таблицы истинности формул. Возьмем в качестве множества X одноэлементное множество {}. Тогда для любой атомарной формулы A значение fX (A) равно, т.е. fX (A) = 0, или fX (A) равно {}, т.е. fX (A) = 1 (напомним, что 0 =, а 1 = {}). Придавая переменным x и y значения f{} (x) f{} (y) из множества {0, 1}, получаем таблицы истинности для логических операций Пусть A1,..., Ak пропозициональные переменные, f отображение множества элементарных формул в {0, 1}. С помощью таблиц истинности логических связок функция f однозначно продолжается на множество формул (A1,..., Ak ), которые строятся из пропозициональных переменных A1,..., Ak и логических связок. При этом для любой формулы, равной (A1,..., Ak ), значение f () снова равно или 1. Если f () = 1 (f () = 0), то говорят, что формула истинна (ложна) на наборе (f (A1 ),..., f (Ak )).

Функция f : {0, 1}k {0, 1}, которая каждому набору (1,..., k ) {0, 1}k сопоставляет значение истинности формулы, называется истинностной функцией формулы. Очевидно, что таблица истинности функции f совпадает с таблицей истинности формулы.

Напомним, что формула называется тождественно истинной (тождественно ложной), если функция f тождественно равна единице (тождественно равна нулю).

{0, 1}, если на этом наборе хотя бы одна формула из ложна или формула истинна. Секвенция называется истинной на наборе (1,..., k ) {0, 1}k, если на этом наборе некоторая формула из ложна. Секвенция по определению ложна на любом наборе, а истинность секвенции совпадает с истинностью формулы.

Секвенция S называется тождественно истинной, если S истинна на любом наборе (1,..., k ) значений истинности переменных A1,...

..., Ak, среди которых содержатся все переменные, входящие в формулы из S.

Теорема 1.5.3. (теорема о полноте). 1. Формула ИС доказуема в ИС тогда и только тогда, когда тождественно истинна.

2. Секвенция S ИС доказуема в ИС тогда и только тогда, когда S тождественно истинна.

По теореме о полноте для того чтобы установить, доказуема ли секвенция 1,..., n (или 1,..., n ), достаточно составить таблицу истинности формулы 1 (2... (n )...) (или 1 (2... (n A0 ¬A0 )...)) и проверить ее тождественную истинность. Как известно, существует единый алгоритм построения таблиц истинности, и, значит, ИС разрешимо.

Следствие 1.5.4. Тогда и только тогда выполняется, когда равны истинностные функции f и f.

Д о к а з а т е л ь с т в о. Предположим, что. Тогда по лемме 1.3.2 доказуема формула ( ). По теореме о полноте получаем тождественную истинность этой формулы, что равносильно соотношению f = f.

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

Из следствия 1.5.6 вытекает, что отношение эквивалентности на формулах алгебры логики и отношение эквивалентности совпадают:

П р и м е р 1.5.1. Так как ¬(¬¬), то ¬(¬¬).

Замечание 1.5.5. Пусть множество всех формул ИС с пропозициональными переменными из множества I. Рассмотрим алгебру F =,,, ¬, A ¬A, A ¬A, где A некоторая фиксированная переменная. Тогда фактор-алгебра F/ является булевой алгеброй, называемой алгеброй Линденбаума для ИС.

Схема аксиом называется независимой в исчислении, если хотя бы один ее частный случай не доказуем в исчислении без этой схемы.

Правило вывода называется независимым в исчислении, если оно не является допустимым в исчислении, полученном удалением этого правила. Исчисление называется независимым, если все его схемы аксиом и правила вывода независимы.

Теорема 1.5.6. Исчисление ИС независимо.

§ 1.6. Исчисление высказываний гильбертовского типа В этом параграфе мы построим исчисление ИВ, в котором в отличие от ИС не используется понятие секвенции, правило вывода одно, а схем аксиом несколько.

Формулами ИВ называются формулы ИС.

Аксиомами ИВ являются следующие формулы для любых формул Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.

Единственным правилом вывода в ИВ является правило заключения (modus ponens): если и выводимые формулы, то также выводимая формула. Символически это записывается так:

Например, если высказывания AB и AB (A C) выводимы, то высказывание A C также выводимо согласно правилу заключения.

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

П р и м е р 1.6.1. Покажем, что формула выводима в ИВ.

Для этого построим вывод данной формулы:

));

2) в схеме аксиом 1 формулу заменим на. Получаем ( 3) из 1 и 2 по modus ponens заключаем ( (( ) )) 4) в схеме аксиом 1 заменяем на. Получаем (( 5) из пп. 3 и 4 по правилу вывода справедливо.

Теорема 1.6.1. (теорема о дедукции). Если,, то, где набор некоторых формул 1,..., n.

Д о к а з а т е л ь с т в о. Рассмотрим минимальный вывод 1,..., k формулы = k из формул 1,..., n и. Если k = 1, то =, аксиома или входит в. В первом случае в силу примера 1.6. формула выводима в ИВ из. Во втором и третьем случаях последовательность, ( ), будет выводом в ИВ из Предположим, что k > 1 и формула получается из формул i и j = i (где i, j < k) по правилу заключения. Поскольку i < k и j < k по индукции можно считать, что i и (i ). Используя аксиому и дважды применяя к этой формуле правило заключения с формулами i и (i ), получаем сначала формулу ( (i )) ( ), а затем формулу. Тем самым, выводимость формулы из доказана.

Применение теоремы о дедукции позволяет во многих случаях сокращать доказательство формул.

П р и м е р 1.6.2. Покажем, что формула ( ( )) доказуема в ИВ для любых формул и ИВ. По теореме о дедукции достаточно показать,. Построим вывод формулы из гипотез и :

1) из аксиомы ( ) и гипотезы получаем формулу ( 2) из аксиомы ( ) и гипотезы выводим формулу ( 3) применяя правило заключения к формуле ( ) и аксиоме 4) из заключения пп. 2 и 3 выводится формула ( );

5) из гипотезы и заключения п. 5 получаем формулу.

Следствие 1.6.2. Тогда и только тогда 1,..., n, когда Следующая теорема устанавливает эквивалентность доказуемости в ИС и доказуемости в ИВ.

Теорема 1.6.3. (теорема об эквивалентности ИС и ИВ) 1. Секвенция 1,..., n доказуема в ИС тогда и только тогда, когда формула выводима в ИВ из формул 1,..., n.

2. Секвенция 1,..., n доказуема в ИС тогда и только тогда, когда формула A ¬A выводима в ИВ из формул 1,..., n.

Из теоремы 1.6.3. вытекает непротиворечивость и разрешимость ИВ. Непосредственно проверяется независимость схем аксиом ИВ.

Множество формул называется противоречивым, если в ИВ справедливо A ¬A. Если противоречивое множество формул, будем обозначать этот факт через.

Утверждение 1.6.4. Формула выводима в ИВ из множества формул тогда и только тогда, когда множество {¬} противоречиво: {¬}.

§ 1.7. Алгоритмы проверки общезначимости и противоречивости в ИВ В этом параграфе мы рассмотрим некоторые основные методы, которые используются для исследования множеств формул исчислений ИС и ИВ на тождественную истинность и противоречивость.

1. Алгоритм Квайна. Напомним, что формула от пропозициональных переменных A1, A2,..., Ak является тождественно истинной, общезначимой или (что то же самое) доказуемой, если булева функция f : {0, 1}k {0, 1}, соответствующая формуле, тождественно равна 1. Для проверки значений функции f используется так называемое семантическое дерево, т. е. бинарное корневое дерево, удовлетворяющее следующим условиям:

каждое ребро помечено литерой Ai j ;

литеры, выходящие из одной вершины, контрарны: Ai, ¬Ai ;

ребра соответствуют литере одной и той же пропозициональной переменной Ai тогда и только тогда, когда они находятся на одинаковом расстоянии от корня (рис. 1.1).

Семантическое дерево имеет 2k висячих вершин и для проверки общезначимости необходимо пройти 2k маршрутов от корня до этих вершин.

Алгоритм Квайна позволяет проходить не все семантическое дерево, а только его часть. Он состоит в том, что пропозициональным переменным Ai, упорядоченным в набор (A1, A2,..., Ak ), последовательно придаются значения 0 и 1 и анализируются таблицы истинности формул, содержащих меньшее число переменных.

П р и м е р 1.7.1. Проверить общезначимость формулы Упорядочим пропозициональные переменные в набор (A, B, C). Придадим первой переменной A значение f (A) = 1. Тогда формула преобразуется следующим образом: (((1 B) C) (1 B)) (1 C) ((B C) B) C. В полученной формуле переменной B придадим значение f (B) = 1. Тогда преобразованная формула примет вид ((1 C) 1) C C C, т. е. будет общезначимой. В случае f (B) = 0 имеем ((0 C) 0) C 0 C, что также общезначимо. Рассмотрим теперь случай f (A) = 0. Имеем Таким образом, все возможные случаи приводят к тождественно истинным формулам. Следовательно, формула тождественно истинна. На рис. 1.2, а изображено семантическое дерево, соответствующее формуле, а на рис. 1.2, б часть семантического дерева, которая фактически использовалась для проверки общезначимости.

Алгоритм редукции решает ту же задачу проверки общезначимости формулы, но используется в том случае, когда в формуле содержится достаточно много импликаций. Идея алгоритма состоит в попытке нахождения значений пропозициональных переменных формулы, при которых значение функции f равно 0, на основе того, что импликация является ложной в том и только в том случае, когда посылка истинна, а заключение ложно.

П р и м е р 1.7.2. Проверить тождественную истинность формулы Предположим, что формула ложна при некотором наборе значений переменных A, B, C. Тогда истинностная функция f по этим значениям переменных дает следующие значения формул: f ((AB) C) = 1, f (A (B C)) = 0. Тогда из второго равенства получаем f (A) = 1, f (B C) = 0, откуда имеем f (B) = 1, f (C) = 0. Однако при этих значениях справедливо f ((A B) C) = 0. Получили противоречие. Таким образом, формула тождественно истинна.

Метод резолюций в ИВ. Пусть D1 = D1 A, D2 = D2 ¬A дизъюнкты. Дизъюнкт D1 D2 называется резольвентой дизъюнктов D1 и D2 по литере A и обозначается через resA (D1, D2 ). Резольвентой дизъюнктов D1 и D2 называется их револьвента по некоторой литере и обозначается через res(D1, D2 ), res(A, ¬A) 0. В последнем случае нуль будет отождествляться с формулой A¬A. Если дизъюнкты D1 и D2 не содержат контрарных литер, то резольвент у них не существует.

resC (D1, D2 ) не существует.

Предложение 1.7.1. 1. Если резольвента res(D1, D2 ) существует и не равна нулю, то секвенция D1, D2 res(D1, D2 ) доказуема.

2. Если резольвента res(D1, D2 ) равна нулю, то доказуема секвенция D1, D2.

Пусть S = {D1, D2,..., Dm } множество дизъюнктов. Последовательность формул 1, 2,..., n называется резолютивным выводом из множества S, если для каждой формулы i (i = 1,..., n) выполняется какое-то из следующих условий:

существуют j, k < i такие, что i = res(j, k ).

Теорема 1.7.2. (теорема о полноте метода резолюций). Множество дизъюнктов S противоречиво в том и только в том случае, когда существует резолютивный вывод из S, заканчивающийся символом 0.

Отметим, что метод резолюций можно использовать для проверки выводимости формулы из данного множества формул 1,..., n.

Действительно, условие 1,..., n равносильно условию 1,..., n, ¬, что в свою очередь равносильно условию, где = тогда Таким образом, задача проверки выводимости 1,..., n сводится к проверке противоречивости множества дизъюнктов S = {D1, D2,..., Dm }, что равносильно существованию резолютивного вывода 0 из S.

П р и м е р 1.7.4. Проверить методом резолюций доказуемость секвенции Согласно утверждению 1.6.4 нужно проверить на противоречивость множество формул Приведем все формулы из S к КНФ: S {¬A ¬B C, ¬(C D) Отсюда получаем множество дизъюнктов S = {¬A ¬B C, ¬C ¬D E, F D, F ¬E, A, B, ¬F }. Построим резолютивный вывод из S, заканчивающийся 0:

6) res(F, ¬F ) = 0.

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

Отметим, что метод резолюций достаточен для обнаружения возможной выполнимости данного множества дизъюнктов S. Для этого включим в множество S все дизъюнкты, получающиеся при резолютивных выводах из S. Из теоремы о полноте метода резолюций вытекает Следствие 1.7.3. Если множество S состоит из всех элементов множества дизъюнктов S, а также всевозможных резольвент всех своих элементов, то S выполнимо тогда и только тогда, когда 0S.

Двойственным к правилу резолюций является правило согласия.

Пусть K1 = K1 A, K2 = K2 ¬A конъюнкты. Положим Пусть S = {K1, K2,..., Km } множество конъюнктов. Последовательность формул 1, 2,..., n называется выводом из S по правилу согласия, если для каждой формулы i (i = 1,..., n) выполняется какое-то из следующих условий:

существуют j, k < i такие, что i = res(j, k ).

Теорема 1.7.4. Множество конъюнктов S = {K1, K2,..., Km } общезначимо (т.е. выполняется |= K1 K2...Km ) тогда и только тогда, когда существует вывод из S по правилу согласия, заканчивающийся символом 1.

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

Дизъюнкт D называется хорновским, если он содержит не более одной позитивной литеры.

П р и м е р 1.7.5. Хорновскими дизъюнктами являются следующие дизъюнкты: ¬A ¬B ¬C D, ¬A ¬B ¬Q, ¬A, B.

В общем случае хорновские дизъюнкты имеют вид ¬A1...¬An B (что эквивалентно формуле (A1...An ) B) или ¬A1...¬An.

Хорновский дизъюнкт вида ¬A1 · · · ¬An B называется точным.

При этом переменные A1,..., An называются фактами, а переменная B целью. Хорновский дизъюнкт вида ¬A1... ¬An называется негативным. Дизъюнкт D = B называется унитарным позитивным дизъюнктом.

Если S множество хорновских дизъюнктов, то невыполнимость множества S проверяется следующим образом. Выбираем в S унитарный позитивный дизъюнкт P и дизъюнкт D из S, содержащий ¬P. После этого заменяем S на (S \ {D}) {res(D, P )} и продолжаем процесс до тех пор, пока S не будет содержать 0 или не найдется дизъюнктов P и D указанного вида. Если на заключительном шаге множество дизъюнктов будет содержать 0, то исходное множество S противоречиво, в противном случае S непротиворечиво.

П р и м е р 1.7.6. Проверить на противоречивость множество дизъюнктов S = {P ¬R ¬T, Q, R, T ¬P ¬R, T ¬Q, ¬P ¬Q ¬R}.

Для доказательства противоречивости запишем дизъюнкты из S в таблицу и применим описанный алгоритм, записывая результат каждого следующего шага в таблицу. Литеры, использующиеся на данном шаге, будем подчеркивать.

На шаге 4 получаем 0, являющийся резолютивным выводом из S.

Следовательно, множество S невыполнимо.

§ 1.8. Логические задачи Аппарат исчислений высказываний позволяет решать так называемые “логические” задачи. При этом самым трудным моментом является построение “модели” задачи, т. е. выделение элементарных высказываний и сведение задачи к проверке некоторых свойств высказываний, возникающих из условий задачи.

П р и м е р 1.8.1. На следствии по делу о похищении автомобиля были допрошены четыре гангстера Андре, Боб, Стив, Том. Андре сказал, что машину похитил Боб, Боб утверждал, что виноват Том.

Том заверил следователя, что Боб лжет. Стив настаивал, что автомобиль угнал не он. Следователю удалось установить, что только один из гангстеров сказал правду. Кто похитил автомобиль?

Р е ш е н и е. Обозначим высказывания “Андре украл”, “Боб украл”, “Стив украл”, “Том украл” через A, B, S и T соответственно. Тогда показания гангстеров имеют вид B, T, ¬T, ¬S. Поскольку секвенция T ¬T доказуема, или, что то же самое, формула T ¬T тождественно истинна, то одно из утверждений T или ¬T обязательно истинно.

Значит, Андре и Стив сказали ложь. Так как утверждение Стива “¬S” ложно, то автомобиль украл Стив.

§ 1.9. Задачи и упражнения 1. Построить выводы секвенций в ИС:

2. Доказать допустимость правил (а) – (о) из предложения 1.2.2.

3. Доказать выводимость в ИВ:

4. Выводимы ли в ИВ следующие формулы:

5. С помощью алгоритма Квайна и алгоритма редукции доказать тождественную истинность аксиом ИВ.

6. С помощью алгоритма Квайна и алгоритма редукции проверить общезначимость следующих формул:

7. Методом резолюций проверить следующие соотношения:

8. Проверить на противоречивость множество хорновских дизъюнктов {AB 9. Состоялся розыгрыш футбольного кубка между командами “Пламя”, “Рекорд”, “Стрела” и “Трактор”. Было высказано три прогноза: победит “Пламя” или “Рекорд”; не победит “Пламя”; не победит ни “Рекорд”, ни “Трактор”.

Известно, что подтвердился только один прогноз. Какая команда выиграла После изучения главы 1 выполняется задача 1 контрольной работы.

Она решается аналогично примерам 1.2.1, 1.7.1, 1.7.2 и 1.7.4.

Глава

ЛОГИКА И ИСЧИСЛЕНИЕ ПРЕДИКАТОВ

В построенной выше логике высказываний в качестве исходных элементов рассматриваются некоторые элементарные высказывания, из которых строятся более сложные высказывания, называемые формулами. При этом не анализируются структура и состав высказываний, а учитываются лишь значения истины или лжи, которые они могут принимать. Однако имеется много мыслей, которые не могут быть рассмотрены таким простым способом. Например, приведем следующее умозаключение:

Каждый человек смертен.

Сократ человек, следовательно, он смертен.

Очевидно, рассмотренное рассуждение интуитивно корректно. Однако, введя следующие обозначения:

P : Каждый человек смертен, Q: Сократ человек, R: Сократ смертен, мы получаем формулу P Q R, которая не доказуема в ИВ. Указанное несоответствие между утверждениями имеет место потому, что в логике высказываний не используется структура высказываний P, Q и R. В этой главе мы введем логику предикатов (логику первого порядка) и исчисления предикатов, которые позволяют преодолевать подобные трудности и дают возможность проводить формализацию бльшей части повседневного и математического языка. Аналогично исчислению секвенций и исчислению высказываний мы будем рассматривать два их расширения секвенциальное исчисление предикатов данной сигнатуры (ИПС ) и исчисление предикатов гильбертовского типа ИП. Построение исчислений предикатов данной сигнатуры мы начнем с понятий синтаксиса и семантики формулы.

§ 2.1. Формулы сигнатуры. Истинность формулы на алгебраической системе Зафиксируем некоторую сигнатуру и счетное множество V = {vi | i }, элементы которого будем называть переменными и обозначать буквами x, y и z, возможно, с индексами. Алфавит исчисления предикатов сигнатуры (ИП ) состоит из следующих групп символов:

1. Предикатные и функциональные символы, образующие сигнатуру.

2. Символы переменных, составляющих множество V.

3. Символ равенства:.

4. Логические связки: ¬,,,.

5. Кванторы:,.

6. Вспомогательные символы: левая скобка (, правая скобка ), запятая,.

Обозначим через T () множество всех термов сигнатуры, в определении которых используются лишь переменные из V. Очевидно, любой терм из T () является словом алфавита ИП.

Введем понятие атомарной формулы сигнатуры :

1) если t1, t2 T (), то (t1 t2 ) атомарная формула;

P (t1, t2,..., tn ) атомарная формула;

3) никаких атомарных формул, кроме построенных по пп. 1, 2, нет.

Формула сигнатуры определяется следующим образом:

1) атомарная формула есть формула;

x, x формулы;

3) никаких формул, кроме построенных по пп. 1, 2, нет.

Символы,, использованные в определении, называются соответственно квантором всеобщности и квантором существования. Запись x (соответственно x) читается “для всех x” (“существует x”).

Все соглашения относительно расстановок скобок, принятые для формул исчисления высказываний, остаются в силе и для формул логики предикатов. Кроме того, вместо записей x1... xn и x1... xn будем использовать записи x1,..., xn и x1,..., xn. Формула сигнатуры называется бескванторной, если она не содержит кванторов.

= {Q, R, P, меньше } со следующими интерпретациями:

Q(x) x рациональное число, R(x) x вещественное число, P (x) x простое число, меньше(x, y) x < y.

Формула x (Q(x) R(x)) означает, что любое рациональное число является вещественным, а формула xy (меньше(x, y) P (y)) для любого элемента x найдется бльший элемент y, являющийся проо стым числом.

2. Рассмотрим сигнатуру = {A(1), B (1), Сократ(0) } со следующими интерпретациями: A(x) x человек, B(x) x смертен, константный символ “Сократ” известный древнегреческий философ. Формула x (A(x) B(x)) читается как “Каждый человек смертен”, а формула A(Сократ) B(Сократ) означает, что Сократ смертен, если он является человеком.

3. Любая бескванторная формула сигнатуры нульместных предикатов может рассматриваться как формула исчисления высказываний. Например, таковой является формула A B ¬C сигнатуры = {A(0), B (0), C (0) }.

Определим множество SF() подформул формулы сигнатуры :

1) если атомарная формула, то ее единственная подформула и SF() = {};

2) если имеет вид ¬1, или x 1, или x 1, то подформула формулы это либо, либо подформула формулы 1 и SF() = SF(1 ) {};

3) если имеет вид 1 2, или 1 2, или 1 2, то подформула формулы это либо, либо подформула формулы 1, либо подформула формулы 2 и SF() = SF(1 ) SF(2 ) {}.

П р и м е р 2.1.2. Пусть x (y (x F (z, y)) ¬P (z)) формула сигнатуры = {F, P }. Тогда x (y (x F (z, y)) ¬P (z)), y (x F (z, y)) ¬P (z), y (x F (z, y)), (x F (z, y)), ¬P (z), P (z) все подформулы формулы.

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

Заметим, что в записи формулы возможно наложение области действия вхождения одного квантора с данной переменной на область действия другого квантора с той же самой переменной. Например, в формуле x (P2 (x, y) x P1 (x)) вхождение переменной x в P1 (x) находится одновременно под кванторами x и x. Поскольку число переменных, образующих множество V, бесконечно, мы будем избегать подобных коллизий введением новых переменных для меньших областей действия вхождений кванторов. Так, вместо формулы x (P2 (x, y) x P1 (x)) будет рассматриваться, например, формула x (P2 (x, y) z P1 (z)).

Говорят, что вхождение переменной x в формулу связано в, если оно находится в области действия некоторого вхождения квантора в формулу, имеющую вид x или x ; в противном случае это вхождение называется свободным в. Переменная x называется свободной (связанной), если некоторое вхождение x в свободно (связано).

П р и м е р 2.1.3. Рассмотрим следующие формулы сигнатуры S = {P1, P2 }:

Переменная x в первой формуле является свободной, во второй и свободной, и связанной, в третьей связанной; переменная y во всех формулах свободна.

Предложением или замкнутой формулой сигнатуры называется формула сигнатуры, не имеющая свободных переменных.

П р и м е р 2.1.4. Формула x, y (x + y y + x) является предложением сигнатуры {+}, формула zx (y P2 (x, y) ¬P1 (x)) предложением сигнатуры {P1, P2 }, а формула x (P2 (x, y) P1 (x)) предложением не является.

Запись (x1,..., xn ) будет означать, что все свободные переменные формулы содержатся в множестве {x1,..., xn }.

Дадим индуктивное определение истинности формулы (x1,..., xn ) сигнатуры на элементах a1,..., an A в алгебраической системе A = A; (запись A |= (a1,..., an ) будет означать, что формула истинна на элементах a1,..., an A в системе A):

1) если t1, t2 T (), то A |= (t1 (a1,..., an ) t2 (a1,..., an )) значения термов t1, t2 в системе A на элементах a1,..., an A совпадают;

2) если P (k) предикатный символ сигнатуры, t1,..., tk T (), (a1,..., an );

(a1,..., an );

Если не выполняется A |= (a1,..., an ), то будем говорить, что формула ложна на элементах a1,..., an в системе A, и писать A |= (a1,..., an ).

П р и м е р 2.1.5. Рассмотрим формулу (x, y) функциональной сигнатуры {+(2), 0(0) }, имеющую вид (x + y 0). Для алгебраической системы A = Z; +, 0 тогда и только тогда имеет место A |= (m, n), A |= (n) для любого целого числа n, поскольку у любого целого числа имеется к нему противоположное и так же целое число. Следовательно, A |= xy (x + y 0). Отметим, что A |= yx (x + y 0), так как нет единого целого числа, противоположного ко всем целым числам.

П р и м е р 2.1.6. 1. Записать формулу (x), истинную в ; +, · тогда и только тогда, когда x четно.

Искомая формула (x) имеет, например, вид y (x y + y).

2. Записать формулу (x, y, z), истинную в ; +, · тогда и только тогда, когда z наименьшее общее кратное чисел x и y.

что z делит все общие кратные x и y, т. е. является наименьшим из всех общих кратных:

Итак, (x, y, z) имеет вид u, v ((z u·x)(z v·y))w (u, v ((w Формула (x1,..., xn ) сигнатуры называется тождественно истинной или общезначимой (тождественно ложной или противоречивой), если для любой алгебраической системы A = A; и любого кортежа элементов (a1,..., an ) An выполнено A |= (a1,..., an ) (A |= (a1,..., an )). Если тождественно истинное предложение, то пишем |=.

Формула (x1,..., xn ) называется выполнимой в системе A, если A |= (a1,..., an ) для некоторых a1,..., an A.

П р и м е р 2.1.7. 1. Формула (x x) общезначима, поскольку A |= (a a) для любой системы A = A; и любого элемента a A. По этой же причине формула ¬(x x) тождественно ложна.

поскольку Z; +, 0 |= xy (x + y 0) и N; +, 0 |= xy (x + y 0).

Тем самым предложение описывает одно из характерных свойств, отличающих систему Z; +, 0 от системы N; +, 0.

истинна, так как Z; · |=, а M2 (Z); · |=, где M2 (Z) множество матриц порядка 2 с элементами из Z.

в системе A = {1, 2}; P, Q, где P = {1}, Q = {(1, 1), (1, 2)}. Составим таблицу истинности предикатов P и Q:

где P (a) = 1 A |= P (a), Q(a, b) = 1 A |= Q(a, b). По таблице истинности предикатов P и Q составляем таблицу истинности формулы P (x) Q(x, y):

из которой следует, что A |= x (P (x)Q(x, 1)), поскольку A |= P (1) Q(1, 1), а также A |= x (P (x) Q(x, 2)), так как A |= P (1) Q(1, 2).

Таким образом, A |= ¬(1) и A |= ¬(2), т. е. A |= (1) и A |= (2).

Следовательно, формула не выполнима в системе A.

5. Докажем выполнимость формулы x, y, u, v (P (x, y) ¬P (u, v)) предикатной сигнатуры = {P (2) }.

Действительно, рассмотрим двухэлементную алгебраическую систему A = {a, b}, P c интерпретацией P = {(a, b)}. Тогда по определению выполняется A |= P (a, b) и A |= P (b, a), т.е. A |= P (a, b) ¬P (b, a). Тем самым в системе A истинна формула (x, y, u, v) P (x, y) ¬P (u, v) на наборе элементов (a, b, b, a). Тогда A |= x, y, u, v (P (x, y) ¬P (u, v)), т.е. данная формула выполнима.

Как и раньше, для формул и через ( ) будем обозначать формулу ( ) ( ).

Предложение 2.1.1. 1. Для любой формулы сигнатуры следующие формулы общезначимы:

2. Для любой формулы сигнатуры формула x x ¬ противоречива.

Заметим, что на основании примера 2.1.5 общезначимость формулы yx xy в общем случае утверждать нельзя. В следующем примере также иллюстрируется отсутствие общезначимости указанной формулы для случая = P (x, y).

Следующая теорема позволяет создавать общезна- чимые и противоречивые формулы на основе фор- Рис. 2. мул ИВ.

Теорема 2.1.2. Пусть (A1,..., An ) общезначимая (противоречивая) формула ИВ, 1,..., n формулы сигнатуры. Тогда в результате подстановки формул 1,..., n вместо всех соответствующих вхождений пропозициональных переменных A1,..., An образуется общезначимая (противоречивая) формула (1,..., n ) сигнатуры.

Теорема 2.1.3. Если f изоморфизм системы A на систему B, (x1,..., xn ) формула сигнатуры системы A, то для любых a1,..., an A свойство A |= (a1,..., an ) эквивалентно свойству B |= (f (a1 ),..., f (an )).

Множество формул сигнатуры с множеством свободных переменных X называется выполнимым, если существует система M = M ;, элементы ax M для каждого x X такие, что для любой формулы (x1,..., xn ) выполнимо M |= (ax1,..., axn ). Система M называется моделью множества формул, и этот факт обозначается через M |=.

П р и м е р 2.1.9. Рассмотрим следующее множество формул сигнатуры {}, описывающих линейные порядки: lo = {x (x x), (x y)), x, y ((x y) (y x))}. Очевидно, что множество lo имеет как конечные, так и бесконечные модели. Например, {0}; |= lo, где = {(0, 0)}, N; |= lo. Добавив к множеству lo две формулы z) (z y) ¬(z y))), получаем множество dlo, описывающее бесконечные плотные линейные порядки. Моделями множества dlo являются в точности бесконечные линейно упорядоченные множества, у которых между любыми двумя различными элементами имеется некоторый промежуточный. Примерами таких моделей служат Q; и § 2.2. Секвенциальное исчисление предикатов Зафиксируем некоторую произвольную сигнатуру и определим секвенциальное исчисление предикатов сигнатуры (ИПС ).

Алфавит ИПС получается из алфавита ИП добавлением символа следования, т.е. A(ИПС ) = V {, ¬,,,,,, (, ),,, }.

Формулами ИПС будут формулы сигнатуры.

Секвенциями ИПС называются конечные последовательности следующих двух видов, где 1,..., n, формулы ИПС :

t1,..., tn термы сигнатуры и формула сигнатуры. Запись ()x11,...,tnn будет обозначать результат подстановки термов t1,..., tn вмеx сто всех свободных вхождений в переменных x1,..., xn соответственно, причем, если в тексте встречается запись ()x11,...,tnn, то предполаx гается, что для всех i = 1,..., n ни одно свободное вхождение в переменной xi не входит в подформулу вида y 1 или y 1, где y переменная, входящая в ti. Вместо записи ()x11,...,tnn мы будем иногда писать (t1,..., tn ). При этом, наряду с тем, что переменные x1,..., xn в записи (x1,..., xn ) будут всегда предполагаться попарно различными, среди t1,..., tn могут быть равные термы.

П р и м е р 2.2.1. 1. Обозначим через формулу x R(x, y, z), через t1 терм F1 (y, z, u), через t2 терм F2 (F3 (z), w). Результат подстановки ()y,z 2 равен x R(x, F1 (y, z, u), F2 (F3 (z), w)), а результат подt1,t становки ()y,z 1 равен x R(x, F1 (y, z, u), F1 (y, z, u)). Заметим, что реt1,t зультат последовательной подстановки может не совпадать с результатом одновременной подстановки. Например, формула (()y1 )z2 равна tt x R(x, F1 (y, F2 (F3 (z), w), u), F2 (F3 (z), w)) и не совпадает с формулой ()y,z 2.

недопустима, поскольку после подстановки терма t вместо свободной переменной y в формуле x R(x, F (y, x, u), z) вхождение переменной x в терм t становится связанным.

Аксиомами ИПС являются следующие секвенции:

1), где формула сигнатуры ;

2) (x x), где x переменная;

3) (t1 q1 ),..., (tn qn ), ()x11,...,tnn ()x11,...,qnn, где t1,..., tn, q1,..., qn термы сигнатуры, формула, удовлетворяющая условиям на записи ()x11,...,tnn и ()x11,...,qnn.

Правила вывода ИПС задаются следующими записями, где, произвольные (возможно пустые) конечные последовательности формул ИПС,,, произвольные формулы ИПС.

двух случаев).

9. (удаление ¬, или доказательство от противного).

12. (утончение, или правило лишней посылки).

13., где переменная x не входит свободно в формулы из (введение справа).

мулы из (введение слева).

Понятия линейного доказательства в ИПС, доказательства в виде дерева в ИПС, доказуемой в ИПС секвенции (теоремы ИПС ) и доказуемой в ИПС формулы определяются аналогично соответствующим понятиям ИС на основе аксиом 1–3 и правил вывода 1–16. Также аналогично предложению 1.2.1 устанавливается Предложение 2.2.1. Секвенция S имеет доказательство в ИПС в виде дерева тогда и только тогда, когда S П р и м е р 2.2.2. Приведем доказательство в виде дерева секвенции для любой формулы (x, y):

Следующая теорема является синтаксическим аналогом теоремы 2.1.2 и позволяет преобразовывать доказуемые формулы ИС в доказуемые формулы ИПС.

Теорема 2.2.2. Пусть (A1,..., An ) доказуемая формула ИС, 1,..., n формулы сигнатуры. Тогда в результате подстановки формул 1,..., n вместо всех соответствующих вхождений пропозициональных переменных A1,..., An образуется доказуемая в ИПС формула (1,..., n ).

Предложение 2.2.3. Для любой формулы, удовлетворяющей условиям на запись ()x11,...,tnn, в ИПС доказуемы следующие секвенx ции:

(а) x1,..., xn ()x11,...,tnn ;

(б) ()x11,...,tnn x1,..., xn.

Определение допустимого правила в ИПС совпадает с соответствующим определением допустимого правила в ИС с заменой ИС на ИПС.

В следующем предложении расширяется список допустимых правил, составленный для ИС.

Предложение 2.2.4. В ИПС допустимы правила (а)–(о) из предложения 1.2.2, а также правила (1 )t1,...,tn,..., (k )x11,...,tnn ()x11,...,tnn Д о к а з а т е л ь с т в о допустимости правил (а)–(о) в ИПС совпадает с доказательством допустимости соответствующих правил в ИС.

Для доказательства допустимости правила (п) применим k раз правило 7, начиная с секвенции 1,..., k, и получим доказуемость в ИПС секвенции Затем, применяя k раз правило 13, получаем доказуемость секвенции Из доказуемости последней секвенции и секвенции (а) предложения 2.2.3 по правилу сечения выводим секвенцию Из последней секвенции и аксиомы (1 )x11,...,tnn (1 )x11,...,tnn по правилам 8 и 12 получаем секвенцию Аналогично применяя еще k 1 раз правило 8, выводим требуемую секвенцию (1 )x11,...,tnn,..., (k )x11,...,tnn ()x11,...,tnn.

Следующее дерево устанавливает допустимость правила (р):

Покажем, что для отношения на множестве термов доказуемы обычные свойства равенства (рефлексивности, симметричности и транзитивности), т.е. доказуемо в ИПС, что отношение эквивалентности.

Предложение 2.2.5. Для любых термов t, q, r T () следующие секвенции доказуемы в ИПС :

Д о к а з а т е л ь с т в о. Доказуемость секвенции (t t) устанавливается применением допустимого правила (п) из предложения 2.2.4:

Для доказательства секвенции (б) рассмотрим аксиому (t q), (z (z t)z, которая равна секвенции (t q), (t t) Выпишем дерево, которое с участием этой аксиомы представляет доказательство свойства симметричности:

Доказуемость секвенции (в) устанавливает следующее дерево:

секвенция ИПС, все свободные переменные формул которой содержатся среди x1,..., xn. Будем говорить, что секвенция S истинна на элементах a1,..., an A в алгебраической системе A и писать A |= S(a1,..., an ), если выполняется одно из следующих условий:

следует A |= (a1,..., an );

на элементах a1,..., an A в алгебраической системе A.

Если секвенция S не истинна на элементах a1,..., an A в алгебраической системе A, то будем говорить, что S ложна на элементах a1,..., an A в A. В частности, секвенция ложна на любой алгебраической системе.

Секвенция S = S(x1,..., xn ) в ИПС называется тождественно истинной, если S истинна на любых элементах a1,..., an A в любой алгебраической системе A = A;.

В дальнейшем нам предстоит доказать теорему о полноте для исчисления предикатов, установленную К. Гделем и утверждающую, что класс доказуемых в ИПС секвенций совпадает с классом тождественно истинных секвенций ИПС. Одна часть этого утверждения это Теорема 2.2.6. (теорема о непротиворечивости ИПС ). Если секвенция S доказуема в ИПС, то S тождественно истинна. В частности, не все формулы ИПС доказуемы в ИПС.

Д о к а з а т е л ь с т в о проводится индукцией по высоте дерева доказательства секвенции S. Тождественная истинность аксиом ИПС очевидна. Проверку сохранения тождественной истинности при переходе по правилам 1–16 мы проведем на примере правила оставив рассмотрения остальных правил читателю в качестве упражнения. Итак, пусть секвенция, ()x тождественно истинна, т.е. в предположении истинности в системе A = A; на каких-то элементах a1,..., an A всех формул из и формулы ()x мы имеем A |= (a1,..., an ). Если в системе A на каких-то элементах a1,..., an A истинны все формулы из и формула x, то, в частности, будет справедливо A |= ()x (a1,..., an ). Значит, по условию будет верно A |= (a1,..., an ). Следовательно, секвенция, x тождественно истинна.

Эквивалентность формул в ИПC § 2.3.

Формулы и сигнатуры называются эквивалентными в ИПС (и пишут ), если секвенции и доказуемы в ИПС.

В силу леммы 1.3.2 условие равносильно доказуемости секвенции ( ). Аналогично лемме 1.3.3 доказывается, что отношение является эквивалентностью на множестве формул сигнатуры. При этом отношение не зависит от выбора сигнатуры, содержащей все сигнатурные символы формул и. Поэтому в дальнейшем мы будем часто говорить о доказуемости в ИПС без упоминания конкретной сигнатуры.

доказуемы в ИПС с использованием лишь правил 1–12.

An ) формулы ИС, построенные из пропозициональных переменных, 1,..., n формулы сигнатуры, (1,..., n ), (1,..., n ) формулы сигнатуры, получающиеся из и соответственно подстановкой формул i вместо пропозициональных переменных. Если имеет место в ИС, то P.

Таким образом, для любых формул, и сигнатуры справедливы все утверждения лемм 1.3.4 и 1.4.1 с заменой на P. Например, Замечание 2.3.2. В ИП справедливо утверждение, аналогичное замечанию 1.5.5. Если множество всех формул сигнатуры с переменными из множества J, то фактор-алгебра F/ алгебры F =,,, ¬, ¬(x x), (x x) является булевой алгеброй.

Предложение 2.3.3. В ИПС выполнимы все следующие эквивалентности, в которых предполагается, что переменная x не входит свободно в формулу :

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

При этом в пункте (а) мы будем использовать допустимое правило, которое легко выводится с помощью закона двойного отрицаравенство (()x )y =.

Теорема 2.3.4. (теорема о замене). Пусть формула сигнатуры, ее подформула, а формула получается из заменой некоторого вхождения на формулу сигнатуры. Тогда если Д о к а з а т е л ь с т в о. Если =, утверждение тривиально.

Если =, воспользуемся индукцией по числу шагов построения формулы. Предполагая, что атомарная формула, снова получаем =. Индукционный переход осуществляется рассмотрением = x 1, = x 1. В каждом из этих случаев формула входит в 1 или 2. Поэтому в первых четырех случаях эквивалентность вытекает из индукционного предположения и аналога леммы 1.3.3. Тогда в силу индукционного предположения остается рассмотреть случаи, когда формула имеет вид x или x, а секвенции и доказуемы. По симметричности и достаточно вывести секвенции x x и x x. Доказательство этих секвенций устанавливается следующими деревьями:

§ 2.4. Нормальные формы В этом параграфе мы определим аналоги ДНФ и КНФ, имеющие место в исчислении предикатов, и укажем алгоритмы приведения произвольных формул ИПС к соответствующим формам.

Будем говорить, что бескванторная формула сигнатуры находится в дизъюнктивной (конъюнктивной) нормальной форме (сокращенно ДНФ и КНФ соответственно), если получается из формулы ИС, находящейся в ДНФ (КНФ), подстановкой вместо пропозициональных переменных некоторых атомарных формул сигнатуры.

Будем говорить, что формула сигнатуры находится в пренексной (предклазуальной) нормальной форме (сокращенно ПНФ и ПКНФ соответственно), если имеет вид где Q1,..., Qn кванторы, а находится в ДНФ (КНФ). При этом формула называется дизъюнктивным (конъюнктивным) ядром, а слово Q1 x1... Qn xn кванторной приставкой формулы.

Теорема 2.4.1. Для любой формулы сигнатуры существует формула сигнатуры, находящаяся в ПНФ (ПКНФ) и эквивалентная формуле.

Д о к а з а т е л ь с т в о. Для приведения формулы к ПНФ (ПКНФ) на основании теоремы о замене используются эквивалентности, описанные в предложении 2.3.3, а также эквивалентность ( ) (¬ ). Сначала формула преобразуется в эквивалентную ей формулу, не содержащую символа импликации. Затем формула последовательным вынесением кванторов (при этом, если необходимо, переименовываются связанные переменные) приводится к виду Q1 x1... Qn xn, где Qi {, }, 1 i n, бескванторная формула. Наконец, формула приводится к ДНФ (КНФ), как показано в § 6.4 и в § 1.4.

П р и м е р 2.4.1. Считая формулы и атомарными, привести к пренексной и предклазуальной нормальным формам формулу x y (x, y) x y (x, y).

Избавясь от импликации, получаем Используя пп. (а, б) предложения 2.3.3 и теорему о замене, получаем Так как в формуле x y (x, y) переменные x, y являются связанными, то по пп. (в, г) предложения 2.3.3. имеем Пусть u, v некоторые новые переменные. Тогда по пунктам (ж, з) предложения 2.3.3 получаем откуда Формула ¬(x, y) (u, v) находится в ДНФ и в КНФ одновременно, а значит, формула находится и в ПНФ, и в ПКНФ.

§ 2.5. Теорема о существовании модели В этом параграфе мы сформулируем основные теоремы исчисления предикатов: теорему Мальцева Гделя о существовании модели для любого непротиворечивого множества формул, теорему Гделя о полноте и теорему Мальцева о компактности.

Множество формул сигнатуры называется противоречивым или несовместным, если для некоторых формул 1,..., n в ИПС доказуема секвенция 1,..., n. Множество формул сигнатуры, не являющееся противоречивым, называется непротиворечивым или совместным.

Формула сигнатуры называется логическим следствием множества формул сигнатуры, если в ИПС доказуема секвенция 1,..., n для некоторых формул 1,..., n из.

Из допустимого правила (з) (правила выведения из противоречия) вытекает, что любая формула сигнатуры (и, в частности, тождественно ложная формула ¬(x x)) является логическим следствием противоречивого множества формул сигнатуры. С другой стороны, любая модель множества формул является моделью для любого его логического следствия. Таким образом, противоречивое множество формул не может иметь модели. Верно и обратное утверждение:

Теорема 2.5.1. (теорема о существовании модели). Если совместное множество формул сигнатуры, то имеет модель мощности, не превосходящей max{, ||}.

Следствие 2.5.2. (теорема Гделя о полноте). Любая тождествене но истинная секвенция ИПС доказуема в ИПС.

Д о к а з а т е л ь с т в о. Аналогично доказательству теоремы о полноте для ИС (теорема 1.5.5) утверждение для секвенций сводится к проверке доказуемости тождественно истинных формул. Итак, пусть (x1,..., xn ) произвольная тождественно истинная формула, все свободные переменные которой содержатся среди переменных Предположим, что формула не доказуема. Установим тогда непротиворечивость множества, состоящего из предложения x1,..., xn ¬.

Действительно, предполагая его несовместность, получаем доказуемость секвенции x1,..., xn ¬, из которой по правилу контрапозиции выводим ¬x1,..., xn ¬. Тогда в силу предложения 2.3.3 доказуема секвенция x1,..., xn, откуда по предложению 2.2.4 (пункт (p)) выводится секвенция, что противоречит предположению о недоказуемости формулы.

Из совместности множества {x1,..., xn ¬} в силу теоремы о существовании модели найдется алгебраическая система A, для которой A |= x1,..., xn ¬. Последнее соотношение означает, что найдутся элементы a1,..., an A, опровергающие предположение о тождественной истинности формулы.

Таким образом, по теореме Гделя проверка доказуемости формулы сводится к проверке ее тождественной истинности. Однако в отличие от ИВ в общем случае не существует алгоритма распознавания доказуемости формул ИПС, т. е. ИПС неразрешимо. Тем не менее если в формуле “записать”, что каждая переменная может принимать конечное число значений, то перебором всех возможных систем можно установить, является ли формула тождественно истинной или нет. В § 2.8 будет описан метод резолюций в исчислении предикатов, который, как и метод резолюций в ИВ, позволяет определять невыполнимость формул.

Множество формул называется локально выполнимым, если любое конечное подмножество 0 множества выполнимо.

Следствие 2.5.3. (теорема Мальцева о компактности). Каждое локально выполнимое множество формул сигнатуры выполнимо.

Д о к а з а т е л ь с т в о. Допустим, что выполнимо любое конечное подмножество формул множества, а само невыполнимо. Тогда по теореме о существовании модели оно противоречиво, т. е. найдутся такие формулы 1,..., n, что доказуема секвенция 1,..., n.

Следовательно, нашлось несовместное, а значит, невыполнимое конечное множество формул из. Полученное противоречие доказывает теорему компактности.

Следствие 2.5.4. Если для любого n множество формул сигнатуры имеет модель мощности n, то имеет бесконечную модель.

xn (¬(x1 x2 ) ¬(x1 x3 )... ¬(xn1 xn )) | n }. По предположению для любого n множество {x1,..., xn (¬(x x2 ) ¬(x1 x3 )... ¬(xn1 xn ))} выполнимо. Значит, множество локально выполнимо. По теореме компактности получаем выполнимость множества. Но может иметь только бесконечные модели.

Следовательно, найдется бесконечная модель M множества, которая, в частности, является моделью для.

§ 2.6. Исчисление предикатов гильбертовского типа Зафиксируем произвольную сигнатуру и определим исчисление предикатов гильбертовского типа, относящееся к сигнатуре (ИП ).

Затем мы установим эквивалентность исчислений ИП и ИПС подобно тому, как была показана эквивалентность исчислений ИС и ИВ.

Формулами ИП будут формулы сигнатуры. Секвенций в ИП нет.

Аксиомами ИП являются следующие формулы для любых формул,, сигнатуры, переменных x, y, z и термов t T (), удовлетворяющих условиям на записи ()x, ()z, ()z :

13) (x x);

Формулы 1–14 называются схемами аксиом ИП.

Правила вывода ИП :

где в правилах 2 и 3 переменная x не входит свободно в.

Понятия доказательства формулы ( ) и вывода формулы из множества гипотез ( ) в ИП определяются аналогично соответствующим понятиям в ИВ.

Предложение 2.6.1. Для любых формул и сигнатуры в ИП справедливы следующие соотношения:

Д о к а з а т е л ь с т в о. Для доказательства соотношения (а) рассмотрим некоторое доказуемое предложение, например, для произвольного предложения сигнатуры (доказательство формулы повторяет с заменой на доказательство из примера 1.6.1).

Применяя правило 1 к гипотезе и аксиоме ( ), выводим формулу. Поскольку переменная x не входит свободно в, по правилу 2 из выводим x. Поскольку предложение доказуемо, по правилу 1 выводим формулу x.

Доказательство соотношения (б) состоит в выводе формулы (x мощью аксиом 1 и 2.

Доказательство соотношения (в) заключается в выводе формулы x из гипотезы ()x и аксиомы ()x x также по правилу 1 с помощью аксиом 1 и 2.

Соотношение (г) получается применением правила 1 к гипотезе ()x t и аксиоме ()t x.

Теорема 2.6.2. (теорема о дедукции). Если {, } множество формул сигнатуры, то в ИП из, следует.

k формулы = k из {}. Если k = 1 или k получается по правилу 1, то повторяем доказательство теоремы 1.6.1. В силу минимальности вывода формулы остается рассмотреть случай, когда получается из k1 по правилам 2 или 3. При этом по индукционному предположению установлено соотношение k1.

Пусть формула = (1 x 2 ) получается из формулы k1 = (1 2 ) по правилу 2, где по определению вывода переменная x не входит свободно в формулы из {, 1 }. Так как (1 2 ) 1, 2, следующая последовательность формул дополняется до вывода формулы из :

Пусть теперь формула получается по правилу 3, т.е. k1 = ( x 1 ( 2 ) (x 1 2 ), следующая последовательность формул дополняется до вывода формулы из :

Таким образом, как и в исчислении высказываний, в силу теоремы о дедукции проверка выводимости 1,..., n в ИП равносильна проверке доказуемости в ИП формулы (1 (... (n )...)).

предложении 2.6.1., по теореме о дедукции в ИП доказуема формула x для любой формулы сигнатуры.

Теорема 2.6.3. (теорема об эквивалентности ИПC и ИП ). 1.

Секвенция 1,..., n доказуема в ИПC тогда и только тогда, когда формула выводима в ИП из формул 1,..., n.

2. Секвенция 1,..., n доказуема в ИПC тогда и только тогда, когда формула ¬(x x) выводима в ИП из формул 1,..., n.

Из теоремы 2.6.3 вытекает непротиворечивость ИП. Непосредственно проверяется независимость схем аксиом ИП.

§ 2.7. Скулемизация алгебраических систем В этом параграфе мы определим конструкцию, предложенную Скулемом и позволяющую расширять сигнатуру данной алгебраической системы так, чтобы появилась возможность “убирать” кванторы у формул. Необходимость такого преобразования объясняется тем, что работать с формулами, содержащими кванторы, значительно трудней, чем с бескванторными. В следующем параграфе будет изложен метод резолюций в исчислении предикатов, использующий скулемизацию.

Алгебраическая система A = A; называется обогащением алгебраической системы A = A ;, если A = A, и совпадают интерпретации всех сигнатурных символов из в системах A и A.

Если система A сигнатуры является обогащением системы A сигнатуры, то A называется обеднением алгебраической системы A и обозначается через A.

системы B.

Пусть некоторая сигнатура, S сигнатура, полученная из добавлением:

а) новых константных символов c для каждой формулы сигнатуры, имеющей вид x0 (x0 );

б) новых n-местных функциональных символов f для каждой формулы = x0 (x0, x1,..., xn ) сигнатуры, имеющей n > 0 свободных переменных.

Тогда сигнатура S называется скулемизацией сигнатуры.

Через S() обозначим множество следующих предложений сигнатуры S, называемых аксиомами Скулема:

а) x0 (x0 ) (c ) для каждой формулы = x0 (x0 ) сигнатуры ;

каждой формулы = x0 (x0, x1,..., xn ) (n > 0) сигнатуры.

Согласно аксиомам Скулема из существования элемента, который можно подставить вместо переменной x0 в формулу, следует возможность подстановки значения некоторой функции f (константы c ), зависящего от оставшихся свободных переменных.

Если A алгебраическая система сигнатуры, то любое ее обогащение AS = A; S, являющееся моделью множества S(), называется скулемизацией системы A. Возникающие при обогащении константы и операции, соответствующие символам c и f, называются скулемовскими константами и скулемовскими функциями.

Отметим, что в отличие от S и S() скулемизация AS не определяется однозначно, поскольку из существования элементов, которые можно подставлять вместо переменных x0, вообще говоря, не следует их единственность.

П р и м е р 2.7.2. Рассмотрим алгебраическую систему A = {0, 1};

P, R(2) с интерпретациями PA = {0, 1}, RA = {(0, 0), (0, 1), (1, 1)}.

В скулемизации AS для формулы x P (x) константный символ c может быть проинтерпретирован как 0 или как 1, поскольку A |= P (0) и A |= P (1). Для функционального символа f, где x0 R(x0, x1 ), возможны интерпретации f = {(0, 0), (1, 0)} или f = {(0, 0), (1, 1)}.

Предложение 2.7.1. Любая алгебраическая система A имеет некоторую скулемизацию AS.

В следующем параграфе при работе с методом резолюций нам предстоит с помощью скулемизации снимать кванторы с формул, находящихся в предклазуальной нормальной форме. Говорят, что формула находится в клазуальной нормальной форме, если она получается из формулы, находящейся в предклазуальной нормальной форме, удалением всех кванторов существования с одновременной заменой соответствующих переменных на термы, определяемые аксиомами Скулема, и последующим удалением всех кванторов всеобщности.

П р и м е р 2.7.3. 1. В примере 2.4.1 найдена формула находящаяся в ПКНФ. С помощью скулемовских функций f1 (x) и f2 (x), заменяющих переменные y и u соответственно, эта формула преобразуется к следующей формуле, находящейся в КлНФ:

2. Формула сигнатуры {P (4), Q(3), R(3) } находится в ПКНФ и приводится к следующей КлНФ с помощью скулемовской константы c, заменяющей переменную x, и скулемовской функции f (y, z, u), заменяющей переменную v:

(P (c, y, z, u) ¬Q(z, u, f (y, z, u))) R(c, z, f (x, z, u)).

§ 2.8. Метод резолюций в исчислении предикатов Зафиксируем некоторую сигнатуру.

Подстановкой сигнатуры называется конечное множество вида {t1 /x1,..., tn /xn }, где ti терм сигнатуры, отличный от переменных xi (1 i n), и все переменные x1,..., xn различны. Подстановка, которая не содержит элементов, называется пустой и обозначается через.

Мы будем использовать греческие буквы для записи подстановок.

F1 (F2 (c2 ))/z} подстановки сигнатуры = {F1, F2, c1, c2 }.

Пусть = {t1 /x1,..., tn /xn } подстановка сигнатуры, W множество формул (термов) сигнатуры. Тогда W множество формул (термов) сигнатуры, полученных из формул (термов) множества W заменой в них одновременно всех вхождений xi (1 i n) на термы ti (1 i n). При этом предполагается, что выполняются все условия на записи формул ()x11,...,tnn, W.

Если W = {} или W = {t}, где формула, t терм сигнатуры, то вместо {} и {t} будем писать и t соответственно.

сигнатуры = {c1, c2, F, F1 }, t = F1 (x, y, z), = (F (x) F1 (x, c1, z)). Тогда t = F1 (c1, F (c2 ), y), = (F (c1 ) F1 (c1, c1, y)).

Пусть = {t1 /x1,..., tn /xn } и = {q1 /y1,..., qm /ym } подстановки сигнатуры. Тогда композиция подстановок и () есть подстановка, которая получается из множества {t1 /x1,..., tn /xn, q1 /y1,..., qm /ym } вычеркиванием всех элементов tj /xj, для которых tj = xj, и всех элементов qi /yi, таких, что yi {x1,..., xn }.

П р и м е р 2.8.3. Пусть = {t1 /x1, t2 /x2 } = {F (y)/x, z/y}, = {q1 /y1, q2 /y2, q3 /y3 } = {c1 /x, c2 /y, y/z} подстановки сигнатуры = {c1, c2, F (1) }. Тогда {t1 /x1, t2 /x2, q1 /y1, q2 /y2, q3 /y3 } = {F (c2 )/x, y/y, c1 /x, c2 /y, y/z}. Так как t2 = y, то y/y должно быть вычеркнуто.

Так как x, y {x, y}, то c1 /x, c2 /y также должны быть вычеркнуты.

Таким образом, = {F (c2 )/x, y/z}.

У п р а ж н е н и е. Доказать: 1) ассоциативность композиции подстановок, т. е. ( ) µ = ( µ) для любых подстановок,, µ;

2) = для любой подстановки.

Подстановка сигнатуры называется унификатором для множества {1,..., k } формул сигнатуры, если 1 =... = k. Множество формул {1,..., k } сигнатуры называется унифицируемым, если для него существует унификатор сигнатуры.

П р и м е р 2.8.4. Множество {P (c1, y), P (x, F (c2 ))} формул сигнатуры = {c1, c2, P (2), F (1) } унифицируемо, так как подстановка = {c1 /x, F (c2 )/y} является его унификатором.

Унификатор для множества {1,..., k } формул сигнатуры называется наиболее общим унификатором (НОУ), если для каждого унификатора сигнатуры этого множества существует подстановка сигнатуры такая, что =.

Пусть W = {1,..., k } непустое множество атомарных формул сигнатуры. Множеством рассогласований в W называется множество термов {t1,..., tk }, где ti входит в i и начинается с символа (который есть либо сигнатурный символ, либо переменная), стоящего на первой слева позиции в i, на которой не для всех формул 1,..., k находится один и тот же символ.

П р и м е р 2.8.5. Пусть W = {P (x, F (y, z)), P (x, c), P (x, F (y, F1 (z)))} всех трех формулах первые четыре символа P (x, совпадают, а на пятом месте в первой и второй формулах стоят разные символы: F, c.

Таким образом, множество рассогласований в W {F (y, z), c, F (y, F1 (z))}.

Алгоритм унификации предназначен для распознавания того, является ли данное конечное непустое множество атомарных формул унифицируемым, и нахождения НОУ для этого множества в случае его унифицируемости.

Пусть W конечное непустое множество атомарных формул. Алгоритм унификации для множества W :

Шаг 2. Если Wk одноэлементное множество, то остановка: k НОУ для W. В противном случае найдем множество Dk рассогласований для Wk.

не входящая в терм tk, то перейти к шагу 4. В противном случае остановка: множество W не унифицируемо.

что Wk+1 = W k+1 ).

Шаг 5. Присвоить k значение k + 1 и перейти к шагу 2.

Теорема 2.8.1. Если W конечное непустое унифицируемое множество атомарных формул, то алгоритм унификации будет всегда заканчивать работу на шаге 2 и последняя подстановка k будет НОУ для W.

П р и м е р 2.8.6. Найти НОУ для множества W = {P (c, x, F2 (F1 (y))), P (z, F2 (z), F2 (u))}.

2. Так как W неодноэлементное множество, то 0 не является НОУ для W. Множество рассогласований для W0 есть D0 = {c, z}.

3. В D0 существует переменная x0 = z, которая не встречается в терме t0 = c. Поэтому переходим к шагу 4.

{P (c, x, F2 (F1 (y))), P (c, F2 (c), F2 (u))}.

5. Присваиваем k = 1.

6. Так как W1 неодноэлементное множество, множество рассогласований для W1 есть D1 = {x, F2 (c)}.

7. Из D1 находим, что x1 = x, t1 = F2 (c).

F2 (F1 (y))), P (c, F2 (c), F2 (u))}.

9. Присваиваем k = 2.

10. Так как W2 неодноэлементное множество, множество рассогласований для W2 есть D2 = {F1 (y), u}.

11. Из D2 найдем, что x2 = u, t2 = F1 (y).

W2 {F1 (y)/u} = {P (c, F2 (c), F2 (F1 (y))), P (c, F2 (c), F2 (F1 (y)))} = {P (c, F2 (c), F2 (F1 (y)))}.

13. Множество W3 одноэлементно. Поэтому 3 = {c/z, F2 (c)/x, F1 (y)/u} НОУ для W.

П р и м е р 2.8.7. Определить, унифицируемо ли множество W = {P (F1 (c), F2 (x)), P (y, y)}.

2. Так как W0 неодноэлементное множество, множество рассогласований для W0 есть D0 = {F1 (c), y}.

3. Из D0 находим, что x0 = y, t0 = F1 (c).

F2 (x)), P (F1 (c), F1 (c))}.

5. Присваиваем k = 1.

6. Так как W1 неодноэлементное множество, множество рассогласований для W1 есть D1 = {F2 (x), F1 (c)}.

7. В D1 нет элемента, который был бы переменной. Поэтому множество W не унифицируемо.

Литерой сигнатуры называется атомарная формула или отрицание атомарной формулы сигнатуры. Дизъюнктом сигнатуры называется литера сигнатуры или дизъюнкция литер сигнатуры.

Примеры дизъюнктов сигнатуры = {P (1), F1, F2, c(0) } P (F1 (x)), ¬P (F1 (x)), P (F1 (x)) ¬(F1 (x) F2 (x, y)), P (F2 (F1 (x), z)) ¬P (F2 (x, y)) (x c).

n). Предположим, что множество формул {1,..., n } имеет НОУ.

Тогда 1 или соответственно ¬1 называется склейкой.

Полученную формулу в дальнейшем будем обозначать через.

П р и м е р 2.8.8. В формуле = P (x) P (F (y)) ¬P2 (x) подформулы P (x) и P (F (y)) имеют НОУ = {F (y)/x}. Следовательно, = P (F (y)) ¬P2 (F (y)) склейка.

Пусть 1, 2 два дизъюнкта, не имеющих общих переменных, L1, L2 литеры в 1 и 2 соответственно. Если литеры L1 и L2 ¬L имеют НОУ, то дизъюнкт, получаемый из дизъюнкта 1 вычеркиванием L1 и L2, называется бинарной резольвентой 1 и 2, а литеры L1 и L2 называются отрезаемыми литерами. Если 1 = L1 и 2 = L2, то полагаем бинарную резольвенту 1 и 2 равной 0.

Если 1 и 2 имеют общие переменные, то, заменив в формуле эти общие переменные на переменные, не встречающиеся в 1 и 2, получим формулу 2, которая не имеет общих переменных с формулой 1. Бинарной резольвентой формул 1 и 2 называется бинарная резольвента формул 1 и 2.

П р и м е р 2.8.9. Найти бинарную резольвенту формул Заменив переменную x в 2 на y, получим 2 = ¬P1 (c) P3 (y).

Выбираем L1 = P1 (x), L2 = ¬P1 (c). Так как ¬L2 L2 = P1 (c), то L и L2 имеют НОУ = {c/x}. Бинарная резольвента формул 1 и получается из 1 2 = P1 (c)P2 (c)¬P1 (c)P3 (y) вычеркиванием P1 (c) и ¬P1 (c). Следовательно, P2 (c) P3 (y) бинарная резольвента 1 и 2, а P1 (x) и ¬P1 (c) отрезаемые литеры.

Резольвентой дизъюнктов 1 и 2 (res(1, 2 )) является одна из следующих бинарных резольвент:

бинарная резольвента 1 и 2 ;

бинарная резольвента склейки 1 и 2 ;

бинарная резольвента 1 и склейки 2 ;

бинарная резольвента склейки 1 и склейки 2.

P1 (F1 (y)), 2 = ¬P (F (F1 (c1 ))) P2 (c2 ).

Склейка 1 есть 1 = 1 {F (y)/x} = P (F (y)) P1 (F1 (y)). Бинарная резольвента 1 и 2 есть P1 (F (F1 (c1 ))) P2 (c2 ). Следовательно, res(1, 2 ) = P1 (F (F1 (c1 ))) P2 (c2 ).

Пусть S множество дизъюнктов сигнатуры. Резолютивный вывод формулы из S есть такая конечная последовательность 1,..., k дизъюнктов, что k = и каждый дизъюнкт i или принадлежит S, или является резольвентой дизъюнктов, предшествующих i.

Универсальным замыканием формулы (x1,..., xn ) называется предложение x1,..., xn (x1,..., xn ).

Теорема 2.8.2. (теорема о полноте метода резолюций). Если S множество дизъюнктов сигнатуры, то множество универсальных замыканий формул из S невыполнимо тогда и только тогда, когда существует резолютивный вывод нуля из S.

П р и м е р 2.8.11. Доказать невыполнимость множества формул Построим резолютивный вывод 0 из W :

7 = res(2, 5 ) = res(2, 5 {z/y}) = ¬P1 (z, z, u) ¬P3 (c1, u) P3 (c1, z);

П р и м е р 2.8.12. Выполнимо ли множество предложений {1, 2 }?

Если множество выполнимо, построить систему, на которой предложения 1 и 2 истинны:

Приведем формулы 1, 2 к предклазуальной нормальной форме:

1 y x, z ((¬P1 (x, z) P2 (x)) (¬P1 (x, z) P3 (y)) P4 (y)), 2 x y ((¬P4 (x) ¬P3 (x)) P1 (x, y)).

Введением символов скулемовской константы c и скулемовской функции F получаем, что выполнимость множества формул {1, 2 } сигнатуры = {P1, P2, P3, P4 } равносильна выполнимости множества формул {x, z ((¬P1 (x, z) P2 (x)) (¬P1 (x, z) P3 (c)) P4 (c)), сигнатуры = {c, F (1) }, что в свою очередь равносильно выполнимости множества формул Действительно, пусть множество формул {1, 2 } выполнимо. Тогда существует алгебраическая система A = A, и c A, для которых A |= x z (¬P1 (x, z) P2 (x)) x z (¬P1 (x, z) P3 (c )) P4 (c ) и A |= x (¬P4 (x) ¬P3 (x)).

Кроме того, для любого a A найдется элемент в A, который обозначим через G(a), такой, что A |= P1 (a, G(a)), т. е. A |= x P1 (x, G(x)).

Тогда в системе A = A,, где c является интерпретацией c, G интерпретацией F, истинны формулы из (2.2), а значит, и формулы из (2.1).

Напротив, если все формулы из (2.1) истинны в системе A = A,, то, очевидно, формулы (2.2) и 1, 2 будут истинны и в системе A = Приведем формулы из (2.2) к КлНФ и исследуем на выполнимость с помощью метода резолюций получившееся множество дизъюнктов {¬P1 (x, z) P2 (x), ¬P1 (x, z) P3 (c), P4 (c), ¬P4 (x) ¬P3 (x), Имеем res(¬P1 (x, z) P3 (c), P1 (x, F (x))) = P3 (c), res(P3 (c), ¬P4 (x) ¬P3 (x)) = ¬P4 (c), res(¬P4 (c), P4 (c)) = 0.

Построили резолютивный вывод нуля. Следовательно, множество дизъюнктов (2.3) невыполнимо. Тогда и множество предложений (2.1) невыполнимо, что равносильно невыполнимости множества предложений {1, 2 }.

П р и м е р 2.8.13. Выполнимо ли множество предложений {1, 2, 3 }? Если выполнимо, построить систему, на которой эти предложения истинны: 1 x (P1 (x) y(P2 (y) P3 (x, y))), Приведем формулы 1, 2, 3 к ПКНФ:

2 x y (¬P1 (x) ¬P4 (y) ¬P3 (x, y)), 3 x (¬P2 (x) ¬P4 (x)).

Из полученных формул получаем следующие формулы, находящиеся в КлНФ:

(P1 (c) (¬P2 (y) P3 (c, y)), (¬P1 (x) ¬P4 (y) ¬P3 (x, y)), (¬P2 (x) ¬P4 (x)).

Так же, как в примере 2.8.12, строим множество дизъюнктов:

Исследуем это множество на выполнимость с помощью метода резолюций:

res(P1 (c), ¬P1 (x) ¬P4 (y) ¬P3 (x, y)) = ¬P4 (y) ¬P3 (c, y), res(¬P2 (y) P3 (c, y), ¬P4 (y) ¬P3 (c, y)) = ¬P2 (y) ¬P4 (y). (2.5) Других резольвент для множества (2.4) нет, поэтому резолютивный вывод 0 из (2.4) не существует. Рассмотрим множество, составленное из констант, входящих в формулы (2.4), т. е. множество {c}. Определим на {c} предикаты P1, P2, P3, P4 так, чтобы множество формул из (2.4) и (2.5) выполнялось на системе {c}; P1, P2, P3, P4. Из (2.5) следует, что необходимо потребовать c P4, или c, c P3 и c P2.

Положим c P4, c, c P3, c P2. Из (2.4) следует, что необходимо потребовать c P1. Таким образом, на системе {c}; P1, P2, P3, P4, c выполняются все формулы из (2.4). Более того, на ней истинны все формулы из (2.4) с навешанными на них кванторами всеобщности по переменным x, y, что равносильно истинности формул 1, 2, 3 на системе {c}; P1, P2, P3.

П р и м е р 2.8.14. Выполнимо ли множество предложений {1, 2 }?

Если выполнимо, построить систему, на которой эти предложения истинны:

1 u x z y (P3 (z)((P2 (x, z)¬P1 (u))¬((P3 (y) P1 (y)) P1 (u)))), Преобразуем формулы 1 и 2 к предклазуальной нормальной форме:

1 u x z y (P3 (z) (P2 (x, z) ¬P3 (y) P1 (y)) ¬P1 (u)), 2 x, y (¬P2 (x, y) ¬P3 (x)).

Исследуем на выполнимость множество дизъюнктов которое получается из преобразованных формул после введения символов скулемовской константы c и скулемовской функции F. Имеем res(¬P1 (c), P2 (x, F (x)) ¬P3 (y) P1 (y)) = P2 (x, F (x)) ¬P3 (c), res(P2 (x, F (x)) ¬P3 (c), ¬P2 (x, y) ¬P3 (x)) = ¬P3 (c), res(P2 (x, F (x)) ¬P3 (y) P1 (y), ¬P2 (x, y) ¬P3 (x)) = ¬P3 (y) P1 (y), res(¬P3 (y) P1 (y), P3 (F (x))) = P1 (F (x)), Таким образом, резолютивного вывода 0 из множества (2.6) не существует. Построим алгебраическую систему A = A; P1, P2, P3, F, c, в которой будут истинны формулы (2.6) и (2.7) с навешанными на них кванторами всеобщности по переменным x, y. Ясно, что c A.

Так как A |= x(¬P3 (c) P3 (F (x)), то F (c) = c. Положим A {c, c } и F (c) c. Так как A |= xP3 (F (x)), то необходимо, чтобы F (c ) = c и c P3. Из (2.7) следует, что c P3. Поскольку A |= x, y (P1 (F (x)) ¬P2 (F (x), y)), полагаем c P1, (c, c) P2, (c, c ) P2. Предикаты P1 и P2 доопределяются произвольно. Таким образом, в системе {c, c }; P1, P2, P3 такой, что c P1, (c, c), (c, Следующий пример показывает, как формализуются предложения и методом резолюций эффективно доказываются теоремы при переходе к соответствующим формализациям.

П р и м е р 2.8.15. Установить, что из посылки “Студенты суть граждане” следует заключение “Голоса студентов суть голоса граждан”.

Пусть формулы S(x), C(x) и V (x, y) означают “x студент”, “x гражданин” и “x есть голос y” соответственно. Тогда посылка и заключение запишутся следующим образом:

x (y(S(y) V (x, y)) z(C(z) V (x, z))) (заключение).

Формула, соответствующая посылке, эквивалентна дизъюнкту ¬S(y) C(y). Поскольку имеем три дизъюнкта, определяющие отрицание заключения:

Доказательство заканчивается следующим образом:

res(¬S(y) C(y), S(b)) = C(b), res(C(b), ¬C(z) ¬V (a, z)) = ¬V (a, b), res(V (a, b), ¬V (a, b)) = 0.

§ 2.9. Логические программы Приведенный метод резолюций служит основой языков логического программирования, главным отличием которых от “процедурных” языков является то, что программа не указывает, как что-либо следует делать для решения задачи, а описывает некоторые элементы и связи между ними (модель определенной сигнатуры) и ставит цель, т.е. задает вопрос об этой системе (на формальном языке это означает проверить истинность предложения на данной системе или найти элемент, удовлетворяющий заданной формуле). При этом компьютер самостоятельно ищет стратегию для решения поставленных вопросов.

Логическая программа представляет собой конечный набор выражений, каждая из которых имеет один из следующих видов:

где P (t1,..., tn ), Q(s1,..., sk ), Q1 (s1,..., sk ),..., Qm (s1,..., sk ) атомарные формулы сигнатуры. При этом в конце каждого выражения ставится точка. Выражения первого вида называются фактами, а второго правилами.

Каждый факт интерпретируется отношением между объектами, а правило (2.9) читается как “если истинны Q1 (s1,..., sk ),..., Qm (s1,..., sk ), то истинно Q(s1,..., sk )”. Формула Q(s1,..., sk ) называется заголовком правила (2.9). Правила позволяют выводить новые факты из уже имеющихся.

Таким образом, логическая программа состоит из конечного числа фактов и правил:

В фактах описывается алгебраическая система, для которой с помощью правил выводятся некоторые ее свойства.

Логическая программа задает множество следствий, которые являются результатом программы. Таким образом, выполнение логической программы это вывод следствий.

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

Семантика логической программы представляется в двух видах логическая семантика и процедурная семантика. Определим сначала логическую семантику.

Каждому факту (2.8) поставим в соответствие предложение где x1,..., xs все переменные, входящие в формулу P (t1,..., tn ).

Каждому правилу (2.9) поставим в соответствие предложение где y1,..., ys все переменные, входящие в формулы Q1 (s1,..., sk ), Запрос (2.10) получит в соответствие формулу где кванторы существования связывают все переменные.

Пусть 1,..., a предложения, соответствующие всем фактам, 1,..., b всем правилам. Тогда значение пары в логической семантике есть утверждение о том, что секвенция доказуема. Для того чтобы выяснить, так ли это, применяется метод резолюций.