Элементы логики предикатов (стр. 2 )

Примеры

Пример 2.5

Привести формулы к ПНФ:

а) ;

б) .

Решение

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

а)

.

б)

.

Задачи

2.8. Привести к ПНФ:

а) ;

б) ;

в) ;

г) ;

д) ;

е) ;

ж) ;

з)

.

Контрольные вопросы

1.  Дайте общее определение предиката. Что такое «местность» предиката? тождественно-истинный предикат? тождественно-ложный предикат?

2.  Как определяются логические операции над предикатами?

3.  Чем отличается формула логики высказываний от формулы логики предикатов?

4.  Что такое интерпретация формулы логики предикатов? Параметр формулы? Замкнутая формула?

5.  Что называют коллизией переменных?

6.  Какие формулы логики предикатов называют равносильными? Конгруэнтными? Тождественно-истинными? Тождественно-ложными?

7.  Дайте определение кванторов существования и всеобщности в случае одноместного и многоместного предиката.

8.  Попробуйте доказать свойства кванторов.

9.  Какие понятия формального языка выполняют роли, аналогичные тем, которые в естественном языке выполнятся: подлежащим? Сказуемым? Дополнениями? Местоимением? Союзами?

10.  Что такое терм? Функциональная сложность терма?

11.  Что такое формула? Логическая сложность формулы?

12.  Что такое предваренная нормальная форма?

3. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ И ИСЧИСЛЕНИЕ
ПРЕДИКАТОВ

3.1. Общее представление об исчислении высказываний

Сводка теории

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

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

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

Существует много вариантов формализации логики высказываний. Опишем подробнее один из них; назовем его «теория L». Формальная (аксиоматическая) теория L считается определенной, если выполнены следующие условия:

1) Задано некоторое счетное множество символов теории L (языка теории). Основные символы теории L суть: пропозициональные буквы , ..., , ... ; логические связки , Ú, , Ø ; скобки (, ).

Конечные последовательности символов теории называются выражениями теории L.

2) Имеется подмножество выражений теории L, называемых формулами теории и определяемых индуктивно с помощью следующих двух пунктов:

i)   пропозициональные буквы суть формулы L;

ii) если A и B – формулы, то формулами являются и следующие выражения: , , , .

3) Выделено некоторое множество формул, называемых аксиомами теории L, в рассматриваемом варианте теории их десять:

, (ив1)

, (ив2)

, (ив3)

, (ив4)

, (ив5)

, (ив6)

, (ив7)

, (ив8)

, (ив9)

(ив10)

Здесь – конкретные пропозициональные переменные, так что (ив1) – (ив10) есть список из десяти конкретных формул языка L.

4) Принимаются правила вывода, по которым можно из уже установленных теорем получать новые. В теории L – два таких правила вывода.

Первое правило имеет вид (MP) .

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

Второе правило имеет вид: (S) .

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

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

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

Примеры

Пример 3.1

Вывести в теории L теорему (AA).

Решение

Возьмем в качестве примера первой формулы вывода аксиому (ив2). Применим к ней правило подстановки в виде:

( A, (A A), A).

Получим

((A ((A A) A))((A (A A))(A A))). (а)

Из аксиомы (ив1) подстановкой ( A, (AA)) получим:

(A((A A) A)). (б)

Применим правило (MP) к (а) и (б):

((A (A A))(A A)). (в)

Из аксиомы (ив1) подстановкой ( A, A) получим:

((A(A A))). (г)

Применяя (МР) к (в) и (г), окончательно получим:

(A A). (д)

Пример 3.2

Построить вывод в ИП для формулы (AA).

Решение

Для удобства вывод запишем сначала в виде столбцов формул, а затем в виде дерева. Столбцы формул:

А((А А) А), (а)

это пример схемы аксиом (ип1);

(А(( А А) А))(( А( А А))( А А)), (б)

это пример схемы аксиом (ип2);

(А( А А))( А А), (в)

получается по (MP) из (а) и (б);

А( А А), (г)

это пример схемы аксиом (ип1);

А А (д)

получается из (в) и (г) по (MP).

Соответствующее дерево вывода имеет вид:

Задачи

3.1. Являются ли выводами в ИВ следующие последовательности формул:

а) ;

б) , , ;

в) , , В?

3.2. Вывести в ИВ формулы:

а) ;

б) .

3.2. Общее представление об исчислении предикатов

Сводка теории

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

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

Фиксируем логико-математический язык первого порядка L. Аксиомами исчисления предикатов (ИП) в языке L называются формулы этого языка, имеющие один из следующих видов:

, (ип1)

, (ип2)

, (ип3)

, (ип4)

, ип5)

, (ип6)

, (ип7)

, (ип8)

, (ип9)

, (ип10)

, (ип11)

, (ип12)

, (ип13)

. (ип14)

Здесь A, B, C – произвольные формулы языка L, так что каждая строка приведенного списка задает схему аксиом ИП. Фиксируя A, B, C, из каждой из четырнадцати схем аксиом можно получить бесконечное семейство конкретных аксиом. Далее означает правильную подстановку терма вместо переменной с необходимыми переименованиями связанных переменных. Вместо будем иногда несколько неточно писать A(t). В схемах (ип12) и (ип14) формула C не содержит свободной переменной x.

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

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

(MP) , (Gen) .

Первое правило вывода носит традиционное латинское название – модус поненс (modus ponens). Второе правило называется правилом обобщения (Gen – от английского слова «generalization»). Оба правила сохраняют логические законы: если выше черты стоят тавтологии, то формула ниже черты также тавтология).

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

1) каждая формула A сама по себе является деревом формул, нижней формулой этого дерева формул считается по определению формула A;

2) если и – деревья формул с нижними формулами вида A и соответственно, то фигура есть дерево формул. Говорят, что формула B получена в этом дереве из A и по правилу (MP); нижней формулой результирующего дерева является формула B;

3) если – дерево формул с нижней формулой A и x – переменная, то фигура есть также дерево формул. Говорят, что нижняя формула этого дерева получена из A по правилу (Gen).

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

Деревом вывода, или просто выводом, в ИП называется дерево формул, удовлетворяющее некоторому дополнительному структурному требованию. А именно, если формула получена в выводе из формулы A по правилу (Gen), то переменная x не входит свободно в гипотезы, расположенные выше рассматриваемого вхождения формулы .

Если формула получена в дереве формул из формулы A по правилу (Gen), а формула B расположена в дереве формул выше рассматриваемого вхождения и содержит свободно x, то говорят, что переменная x варьируется в формуле B. Тогда структурное требование можно выразить следующим образом: в выводе параметры гипотез не варьируются, остаются свободными.

Структурное требование выполняется тривиально, если дерево формул не содержит правил (Gen), или если все гипотезы дерева формул суть замкнутые формулы, или если дерево формул вовсе не содержит гипотез.

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

Список Г может быть пуст. Тогда ГA означает, что имеется вывод A без гипотез; тогда пишут A и говорят: формула A выводима в ИП.

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

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

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

Ключевым фактом здесь является следующая теорема.

Теорема 3.1 (о дедукции)

Если Г, AB, то Г . Этот факт записывается в виде вспомогательного правила вывода:

Теорема о дедукции показывает, что для установления импликации
Г достаточно показать Г, AB, что часто бывает гораздо проще. В математической практике этому соответствует следующий пример рассуждения. Если нужно в некоторой ситуации установить, что , то допустим (введем гипотезу), что A верно, и докажем B, исходя из этой гипотезы.

Следующие правила называются структурными правилами техники естественного вывода:

1) закон тождества	AA;
2) правило добавления	ГA Г,BA;
3) правило перестановки	Г, B, C, DA Г, C, B, DA;
4) правило сокращения	Г, B, B, CA Г, B, CA;
5) правило сечения	ГA; B, AC Г, BC.

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

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

Логические операции и кванторы	Правила
Введение	Удаление
1) Импликация	Г, АВ ГAВ	ГA; ГAВ ГВ
2) Конъюнкция	ГA; ГВ Г A^B	Г, A, BC Г, A^BC
3) Дизъюнкция	ГA ГB ГAÚB Г AÚB	Г, AC; Г, BC Г, AÚBC
4) Отрицание	Г, AB; Г, AØB ГØA	ГØØA ГA

Логические операции и кванторы	Правила
Введение	Удаление
5) Общность	ГA(y) Гx A(x) (здесь y не входит свободно в Г, и если x отлично от y, то x не входит свободно в A(y));	Гx A ГA(x t)
6) Существование:	Г A(x t) Г x A	Г, A(y)C Г, x A(x)C (здесь y не входит свободно в Г и C, и если x отлично от y, то x не входит свободно в A(y), A(x) есть A(y x))
7) Эквивалентность	Г, AB; Г, BA ГAB	ГA; ГA B ГB ГB; ГAB ГA

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