Правила вывода в исчислении предикатов

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

В исчислении предикатных секвенций определены схема аксиом и множество правил вывода, в которых используются обозначения. U,B,D,G – произвольные формулы; Г1,Г2,Г3,Г4 – конечные последовательности формул, возможно, пустые; t – терм, свободный для x в формуле U(x); U(t) – результат подстановки терма t вместо всех свободных вхождений переменной х в формуле U(x); D – формула, не содержащая х свободно.

Правила 1-11, 17, 18 совпадают с правилами вывода в исчислении высказываний. Правила 12-16 вводят кванторы.

Формальная система ИПС содержит схему аксиом и множество правил вывода.

Схема аксиом: U├U.

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

1. Введение &: .

2. Удаление &: .

3. Введение Ú: .

4. Удаление Ú: .

5. Введение ®: .

6. Удаление ®: .

7. Введение отрицания: .

8. Удаление отрицания: .

9. Сведение к противоречию: .

10.Утончение: .

11.Расширение: .

12.Введение квантора общности, (|-"): . Здесь v не входит свободно в Г. Если x отлично от v, то x не входит свободно в U(v).

13.Удаление квантора общности: .

14.Введение квантора существования, (|-$): .

15.Введение квантора существования, ( $ |-): . Здесь v не входит свободно в Г и D.Если x отлично от v, то x не входит свободно в U(v), есть .

16.Правило обобщения (декларированное, но не следующее из теорем). Введение квантора общности ("├): (На основе правила обобщения ).

17.Перестановка: .

18.Сокращение: .

19.Правило сечения: .

Правила утончения (10), расширения (11), перестановки (17), сокращения (18) и сечения (19) называются структурными правилами техники естественного вывода.

Правила 1-8 и 12-16 - логические правила. Правила эти разбиваются на группы: для каждой логической связки и квантора-своя группа правил. Кроме того, внутри группы правила делятся на два вида: правила введения, указывающие, как доказывать формулу с данным логическим символом, и правила удаления, указывающие, как использовать формулу с данным логическим символом для доказательства других формул.

Рассмотрим некоторые из правил.

1. Правило введения импликации (вв®).

2. Правило удаления импликации (уд.®). Из секвенций Г├U; Г├(U®В) секвенцию Г├В получим с использованием правила модус поненс. . Это в точности теорема дедукции.

3. Правило введения дизъюнкции (вв.Ú). Имеем Г├U и ├(U®(UÚВ)) (это аксиома). По правилу модус поненс Г├(UÚВ).

4. Правило удаления дизъюнкции (уд.Ú). Из данных Г, U├G; Г,В├G по теореме о дедукции Г├(U®G) и Г├(В®G). Кроме того, имеем аксиому ├((U®G)®((B®G)®((UÚB)®G))). Дважды применяя модус поненс, получаем Г├((UÚB)®G). Из схемы аксиом имеем (UÚG) ├(UÚG). По правилу расширения получаем Г, (UÚG) ├(UÚG). По модус поненс Г,(UÚB) ├G.

5. Правило введения отрицания (вв.Ø) соответствует приведению к абсурду: чтобы установить ØU, достаточно, допустив U, получить противоречие, т.е. вывести В и ØВ одновременно.

6. Доказать истинность секвенции

("x(p(x)®q(x))), p(a) |- q(a).

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

1. (P(a)®Q(a)) |- (P(a)®Q(a); P(a) |- P(a) (аксиомы).

2. (P(a)®Q(a)), P(a) |- Q(a) (к (1) применено правило удаления импликации (6).

3. "x(P(x)®Q(x)), P(a) |-Q(a) (к (2) применено правило введения квантора общности (16).

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

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

2. если D₁ и D₂ суть деревья с нижними формулами вида А и А®В соответственно, то фигура

есть дерево формул. Мы говорим, что формула В получена в этом дереве из А и А®В по правилу MP.

3. если D₁ – дерево формул с нижней подформулой А и х переменная, то фигура есть также дерево формул. Мы говорим, что нижняя формула "хА получена из А по правилу обобщения.

Определение дерева формул закончено.

Пример 1. Рассмотрим пример дерева формул высоты 3:

.

Самая длинная ветвь этого дерева формул – это

.

Единственная открытая посылка этого дерева - .

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

Приведенный пример не является, таким образом, выводом. «Запрещен» переход

так как гипотеза ( ) содержит свободно переменную х.

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

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

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

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

Пример 2. Доказать истинность секвенции с использованием обратного вывода.

Доказательство начинается с целевой секвенции, расположенной в верхней строке. В записанной под ней строке содержится секвенция, из которой была получена эта верхняя секвенция. Справа обозначено примененное правило вывода. Использование в правиле (├$) терма u соответствует утверждению теоремы экзистенциальной конкретизации.

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

Доказательство от корня к листьям является более эффективным, чем от аксиом к доказываемой секвенции, так как существенно уменьшает число возможных выборов правил вывода на каждом шаге. Система Logische Kalkul – это классический пример, когда обратный вывод является более целесообразным с точки зрения уменьшения числа переборов для достижения результата. Другими словами, в отличие от прямого вывода, когда можно применять почти все правила, при обратном выводе возможностей выбора существенно меньше.

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

Дата добавления: 2014-11-08; просмотров: 1303; Нарушение авторских прав

Мы поможем в написании ваших работ!