3 - Исчисление высказываний. Введение. Основные положения теории N. Правила естественного вывода. Глобальные свойства теории N (Конспект лекций), страница 2

При этом конечная формула X любоговывода из гипотез Γ называется выводимой из гипотез Γ, что обозначается следующимобразом: Γ ` X.X → (X → X → X)ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓ2)Γ`X(правило добавления гипотез);Γ, ∆ ` X3)Γ, Y, Y, ∆ ` X(правило сокращения гипотез);Γ, Y, ∆ ` X4)Γ, Y, Z, ∆ ` X(правило перестановки гипотез);Γ, Z, Y, ∆ ` X5)∆ ` Y ; Γ, Y ` X(правило сечения).Γ, ∆ ` XÌÃÒÓ*По определению в выводе каждая формула есть либо аксиома, либо гипотеза, либо выводится из предыдущих по правилу modus ponens, т.е. формулы в выводе, строго говоря, могут повторяться.

Однако ясно, чтоповторения можно убрать, не нарушая связей в выводе.ÔÍ-12Правила, обозначенные в теореме, — элементарные следствия из определения понятия вы”вод из гипотез“ и лишь фиксируют очевидное.Отметим также очевидный факт, что мы можем произвольно вводить аксиомы в списокΓ гипотез или выводить аксиомы из списка, не меняя сути. Первое вытекает из правила до-ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓТеорема 3.2. Для любых списков формул Γ и ∆ и любых формул X, Y , Z истинны следующие секвенции:1) Γ, X, ∆ ` X (закон тождества);ÔÍ-12Следующая теорема устанавливает пять правил, называемых структурными правилами естественного вывода. Правила сформулированы не для формул языка алгебрывысказываний, а для секвенций. Они позволяют из уже известных выводимостей получатьновые.

При этом соответствующий вывод на самом деле не строится, а лишь формулируетсязаключение о существовании такого вывода.ÌÃÒÓÔÍ-12J Доказательство строится на анализе последовательности вывода. Фактически надо показать,что для любого вывода Z1 , Z2 , . . . , Zn = Y из гипотез Γ, X существует вывод из гипотез Γформулы X → Y . Доказательство проведем индукцией по длине вывода.При n = 1 конечная формула вывода Zn = Y есть либо аксиома, либо формула из списка Γ,либо формула X (правило modus ponens в данном случае не применялось, так как длина выводаменьше двух). В первом и втором случаях строим последовательность формул Y , Y → (X → Y )(аксиома схемы 1), X → Y (modus ponens), которая является выводом формулы X и спискагипотез Γ.

В третьем случае X = Y и формула X → Y совпадает с выводимой формулой X → X(см. пример 3.1). Таким образом, при n = 1 утверждение доказано.Предположим, что утверждение доказано для всех формул Y , имеющих вывод из гипотезΓ, X длины менее n. Рассмотрим произвольный вывод Z1 , Z2 , . . . , Zn = Y . Формула Y естьлибо аксиома, либо формула из списка Γ, либо X, либо получена по правилу modus ponens. Впервых трех случаях рассуждения те же, что и при n = 1 (в выводе можно оставить толькопоследнюю формулу и свести дело к n = 1).

Рассмотрим случай, когда Y получена по правилуmodus ponens из формул Zk и Zj . В этом случае одна из формул, например Zj , есть импликацияZk → Y . В соответствии с индукционным предположением из гипотез Γ выводимы формулыX → Zk и X → (Zk → Y ). Объединим два этих вывода, удалив из списка повторения формул,если они есть* . Дополняем полученное объединение следующими тремя формулами:X → Zk → (X → (Zk → Y ) → (X → Y )) (аксиома схемы 2);X → (Zk → Y ) → (X → Y ) (modus ponens);X → Y (modus ponens).В результате получаем вывод формулы X → Y из гипотез Γ. В соответствии с методом математической индукции утверждение теоремы доказано для конечной формулы любого выводаиз гипотез Γ, X.

IÌÃÒÓÌÃÒÓÌÃÒÓ26ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓСледующая теорема вводит так называемые логические правила естественного вывода, описывающие некоторые общепринятые приемы проведения математических доказательств.Теорема 3.3. Для любого списка формул Γ и любых формул X, Y , Z верны следующиеутверждения:Γ, Y ` X(введение импликации, теорема о дедукции);Γ`Y →XΓ ` X; Γ ` X → Y2)(удаление импликации, modus ponens);Γ`YΓ ` X; Γ ` Y3)(введение конъюнкции);Γ`X ∧YΓ, X, Y ` Z4)(удаление конъюнкции);Γ, X ∧ Y ` Z1)Γ`XΓ`Xи(введение дизъюнкции);Γ`X ∨YΓ`Y ∨XΓ, X ` Z; Γ, Y ` Z(удаление конъюнкции, правило разбора случаев);6)Γ, X ∨ Y ` Z5)Γ, X ` Y ; Γ, X ` ¬Y(введение отрицания);Γ ` ¬XΓ ` ¬¬X8)(удаление отрицания).Γ`X7)Γ`T →Y →(T →X ∧Y )Γ`TΓ`T →Y`TΓ`T →XΓ, T ` Y`T →X →(T →Y →(T →X ∧Y ))Γ, T ` XΓ`YΓ`XПравило 4 опирается на аксиомы X ∧ Y → X и X ∧ Y → Y .

Из этих аксиом по правилуmodus ponens получаем выводимости X ∧ Y ` X и X ∧ Y ` Y . Остается соединить два этихÔÍ-12Γ`T →X →(T →Y →(T →X ∧Y ))ÌÃÒÓΓ`T →X ∧YÔÍ-12J Первые два правила — это теорема о дедукции и правило modus ponens в применении квыводу из гипотез. В самом деле, объединив выводы из Γ формул X и X → Y , получимпоследовательность, в которой есть эти формулы. Применив modus ponens, получим Y , которуюдобавим в конец последовательности формул.

Получим вывод Y из Γ.Для доказательства правила 3 для произвольно заданных формул X и Y используем какуюлибо аксиому T и аксиому T → X → (T → Y → (T → X ∧ Y )) схемы 5. Из выводимости формул Xи Y из списка Γ следует выводимость формул T → X и T → Y . Дважды удаляя импликацию ваксиоме схемы 5, получим выводимость T → X ∧ Y . Еще раз удаляя импликацию (T выводима),получаем выводимость X ∧Y . Указанную последовательность шагов можно представить в видедереваΓ`X ∧YÌÃÒÓÔÍ-12ÌÃÒÓ`YÔÍ-12ÔÍ-12Γ, Y ` XÌÃÒÓÌÃÒÓбавления гипотез, а второе утверждение можно получить как формальное следствие правиласечения:Γ`XÌÃÒÓÔÍ-12ÌÃÒÓ27ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓΓ, X ∧ Y ` ZΓ, X ∧ Y, X ∧ Y ` ZΓ`X ∧Y →XΓ, X, X ∧ Y ` Y`X ∧Y →XΓ, X ` X ∧ Y → Y`X ∧Y →YΓ`X →Y). Аналогично доказывается правилоΓ, X ` Y5, но с использованием аксиом X → X ∨ Y и X → Y ∨ X, полученных по схемам 6 и 7.Правило 6 опирается на аксиому X → Z → (Y → Z → (X ∨ Y → Z)), полученную по схеме 8и выводится аналогично правилу 5:Γ, X ∨ Y ` ZΓ`X ∨Y →ZΓ`Y →ZΓ ` X → Z → (Y → Z → (X ∨ Y → Z))Γ`X →Z` X → Z → (Y → Z → (X ∨ Y → Z))Γ, X ` ZÌÃÒÓΓ ` Y → Z → (X ∨ Y → Z)Γ, Y ` ZПравило 8 опирается на схему аксиом 10 и доказывается следующим деревом:Γ ` ¬¬X → XΓ ` ¬¬X` ¬¬XΓ`XОтметим, что из схемы 11 вытекает правило, обратное к правилу 8:.Γ ` ¬¬XОстановимся на правиле 7, которое вытекает из схем 9, 10, 11.

Непосредственно из схемыΓ, X ` Y ; Γ ` ¬Yаксиом 9 вытекает более слабое правило:ÌÃÒÓÌÃÒÓΓ ` ¬XΓ ` ¬XΓ ` ¬Y → ¬XΓ ` X → Y → (¬Y → ¬X)ÔÍ-12Γ`XΓ ` ¬YΓ`X →YЧтобы получить нужное правило, необходимо в список Γ добавить аксиому X. Получим праΓ, X, X ` Y ; Γ, X ` ¬YΓ, X ` Y ; Γ, X ` ¬Yвило, или после сокращения одинаковых гипотез:. ОстаΓ, X ` ¬XΓ, X ` ¬XΓ, X ` ¬Xется обосновать правило, для чего используется схема аксиом 11.

Кроме того, как и вΓ ` ¬Xслучае правила 5 используется какая-либо аксиома T . Эта аксиома вводится в список гипотез,ÔÍ-12` X → Y → (¬Y → ¬X)ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Γ, X, Y ` ZÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓΓ, X, X ∧ Y ` Z(здесь использовано упрощенное правило 2 видаÔÍ-12ÌÃÒÓ28вывода с выводом Γ, X, Y ` Z для получения нужного вывода Γ, X ∧ Y ` Z. Соответствующеедерево вывода имеет следующий вид:Γ, X ∧ Y ` XÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓΓ ` ¬XΓ, X ` ¬TÌÃÒÓΓ ` ¬¬T(3.1)Γ, X ` ¬X` ¬¬T`T` T → ¬¬TТеорема полностью доказана. IÌÃÒÓΓ`XПример 3.2. а. Правило, называемое присоединением посылки, вытекает изΓ`Y →Xправила введения импликации и правила добавления гипотез:ÔÍ-12Как видно по комментариям в формулировке теоремы, логические правила естественноговывода есть двух видов: правила введения, которые позволяют доказывать формулу с даннойлогической связкой, и правила удаления, которые показывают, как использовать эту формулудля доказательства других формул.Правила естественного вывода (в первую очередь, теорема о дедукции) позволяют устанавливать выводимость в исчислении высказываний тех или иных формул, не строя конкретноговывода.

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

Как станетясно из дальнейшего изложения, выводимость формулы X равносильна тому, что секвенция` X выводима из правил естественного вывода.На практике при установлении истинности конкретных секвенций удобно использовать дополнительные правила, вытекающие из правил естественного вывода. Укажем некоторые простейшие следствия правил естественного вывода.ÌÃÒÓÔÍ-12ÌÃÒÓ29а затем дважды применяется слабый вариант доказываемого правила:Γ, X, T ` XÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙΓ, Y ` XΓ`XΓ ` X; Γ ` ¬Xб. ПравилоΓ`Yдобавлением гипотез:(закон противоречия) вытекает из правила введения отрицанияÌÃÒÓΓ ` ¬¬YΓ, ¬Y ` XΓ, ¬Y ` ¬XΓ, ¬Y ` XΓ, ¬Y ` ¬XΓ`XΓ ` ¬XÌÃÒÓΓ`Xв. Правило введения двойного отрицанияможет быть получено из схемы аксиомΓ ` ¬¬XΓ ` ¬¬XΓ, ¬X ` XΓ, ¬X ` ¬XΓ`XÌÃÒÓ11. Его можно также вывести из правил естественного вывода:ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Γ`YÔÍ-12ÔÍ-12Γ`Y →XÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ30Γ, X ` Yдоказательства от противного, которого вытекает из правилаг. Полезно правилоΓ, ¬Y ` ¬Xвведения отрицания:Γ, ¬Y ` ¬XΓ, X, ¬Y ` YΓ, X, ¬Y ` ¬YÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123.