1.3.2. Исчисление секвенций

Исчисление секвенций (ИС) – это формальная система, в которой в алфавит языка логики высказываний добавлен символ следования, обозначаемый ├, который читается «выводимо» или «доказуемо». Правила вывода ├  ( выводима из ) применяются непосредственно к формулам, а не к таблицам истинности, позволяя из истинности одних формул делать вывод об истинности других формул. Символы ,  в правиле вывода обозначают одну или несколько формул;  называется условием, а   следствием. Если в условии или следствии формул несколько, то они записываются через запятую. Представляют интерес только такие правила вывода, с помощью которых на основании истинности всех формул, входящих в условие правила вывода, можно при любой интерпретации сделать заключение об истинности всех формул, входящих в следствие правила вывода. Обычно такие правила называют состоятельными.

Понятие формулы в исчислении высказываний определяется, как и в логике высказываний. Если U₁, U₂, ... , U_k , B, Gформулы, то выражения вида U₁, U₂, ... , U_k ├ B называются секвенциями. Далее будем рассматривать секвенции вида:

• U₁, U₂, ... , U_k ├ B, где k>0, читается «из U₁, U₂, ... , U_k следует В»,

• ├ В, читается «В доказуема»,

• U₁, U₂, ... , U_k ├ «система U₁, U₂, ... , U_kпротиворечива».

Правилом вывода называется выражение вида , где  произвольные секвенции;  называется непосредственным следствием из множества секвенций по данному правилу вывода.

Исчисление секвенций определяется схемой аксиом A├ A и множеством правил вывода.

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

Вывод в ИС  это конечная последовательность секвенций такая, что для каждого i (1£i£k) есть либо аксиома, либо непосредственное следствие из предыдущих секвенций по правилам вывода.

Секвенция называется выводимой в ИС, если существует вывод в ИС, оканчивающийся .

Правило называется допустимым в ИС, если из выводимости следует выводимость секвенции Σ.

Опишем механизм, порождающий все тавтологии.

Для большей наглядности формулировок рассмотрим кроме формул также последовательности формул и секвенции вида Г├ Ф, где Гпоследовательность формул, возможно пустая, Фформула. Высказывание входит в секвенцию, если оно входит в левую или правую часть секвенции.

Истинность секвенции: секвенция истинна, если при любых логических значениях всех входящих в нее высказываний из истинности всех формул, входящих в левую часть секвенции, следует истинность формулы в правой части секвенции. Секвенция с пустой левой частью истинна, если правая часть тождественно истинна. Остальные секвенции назовем ложными. Например, секвенция (А®В), (В®С), (С®Х) ├ (А®Х) истинна. Напротив, секвенция (Х Ú (У®Х)) ├Z - ложна.

Истинность секвенции

Ф₁ Ф₂ ... Ф_S ├ Ф

равносильна тому, что формула (Ф₁(Ф₂  .. (Ф_S Ф) ...) - является тавтологией.

Любая секвенция вида Ф├ Ф, где Ф  формула, истинна. Эта секвенция является единственной аксиомой исчисления секвенций.

Пусть символы Г₁, Г₂, Г_3, Г – означают конечные последовательности формул, возможно пустые, U, A, B, C –произвольные формулы. Основные правила вывода в исчислении секвенций:

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

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

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

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

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

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

7. Введение :

8. Удаление :

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

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

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

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

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

14. Сечение:

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

Далее для обозначения используемых правил вывода применяются сокращения: ввΔ, удΔ, сокращ., перест., сеч.  для обозначения правил: введениеΔ, удалениеΔ, сокращение, перестановка, сечение  соответственно, Δ{&, , , }.

Примеры.

1. Вывести секвенцию ├ (UU).

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

Σ₁: U ├ U; Далее, воспользовавшись правилом (5) (введение), получаем: Σ₂: ├ (UU).

2. Вывести секвенцию (UB), (BC), U|–C.

Σ₁: U ├ U (аксиома),

Σ₂: (UB) ├ (UB) (аксиома),

Σ₃: U, (UB) |– B (правило 6, Σ₁, Σ₂),

Σ₄: (B C) ├ (BC) (аксиома),

Σ₅: U, (UB), (BC)├ C (правило 6, Σ₃, Σ₄),

Σ₆: (UB), U, (BC) ├ C (правило 12, Σ₅),

Σ₇: (UB), (BC), U ├ C (правило 12, Σ₆).

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

Построим прямое дерево вывода.

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

5. Доказать, что допустимо правило вывода

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

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

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

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

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

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

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

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

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

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

Рассмотрим пример обратного вывода. Докажем, что секвенция

(UB) |- ((G&U)(G&B)) выводима.

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

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

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

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

Примеры

1. Доказать выводимость секвенции

Из теории булевых функций известно, что Это соотношение будет использовано в дальнейшем выводе.

2. Вывести секвенцию

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

Ниже приведено доказательство для левой секвенции. Доказательство правой секвенции строится аналогично.