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

Структурные правила естественноговывода. Логические правила естественного вывода. Дополнительные правила естественноговывода: присоединение посылки; закон противоречия; двойное отрицание; доказательство отпротивного; удаление конъюнкции справа. Обобщенное правило введения дизъюнкции.ÌÃÒÓÌÃÒÓ2.2. Правила естественного выводаÌÃÒÓÔÍ-12ÌÃÒÓ16ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓПравила, обозначенные в теореме, — элементарные следствия из определения понятия вы”вод из гипотез“ и лишь фиксируют очевидное.Отметим также очевидный факт, что мы можем произвольно вводить аксиомы в списокΓ гипотез или выводить аксиомы из списка, не меняя сути. первое вытекает из правила добавления гипотез, а второе утверждение можно получить как формальное следствие правиласечения:Γ`XΓ, Y ` X`YСледующая теорема вводит так называемые логические правила естественного вывода, описывающие некоторые общепринятые приемы проведения математических доказательств.1)2)3)6)7)ÔÍ-12J Первые два правила — это теорема о дедукции и правило modus ponens в применении квыводу из гипотез.

В самом деле, объединив выводы из Γ формул X и X → Y , получимпоследовательность, в которой есть эти формулы. Применив modus ponens, получим Y , которуюдобавим в конец последовательности формул. Получим вывод Y из Γ.Для доказательства правила 3 для произвольно заданных формул X и Y используем какуюлибо аксиому T и аксиому T → X → (T → Y → (T → X ∧ Y )) схемы 5. Из выводимости формул XÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓ8)ÌÃÒÓ5)Γ, Y ` X(введение импликации, теорема о дедукции);Γ`Y →XΓ ` X; Γ ` X → Y(удаление импликации, modus ponens);Γ`YΓ ` X; Γ ` Y(введение конъюнкции);Γ`X ∧YΓ, X, Y ` Z(удаление конъюнкции);Γ, X ∧ Y ` ZΓ`XΓ`Xи(введение дизъюнкции);Γ`X ∨YΓ`Y ∨XΓ, X ` Z; Γ, Y ` Z(удаление конъюнкции, правило разбора случаев);Γ, X ∨ Y ` ZΓ, X ` Y ; Γ, X ` ¬Y(введение отрицания);Γ ` ¬XΓ ` ¬¬X(удаление отрицания).Γ`XÔÍ-12Теорема 2.3.

Для любого списка формул Γ и любых формул X, Y , Z верны следующиеутверждения:ÌÃÒÓÔÍ-12Γ`X(правило добавления гипотез);Γ, ∆ ` XΓ, Y, Y, ∆ ` X3)(правило сокращения гипотез);Γ, Y, ∆ ` XΓ, Y, Z, ∆ ` X4)(правило перестановки гипотез);Γ, Z, Y, ∆ ` X∆ ` Y ; Γ, Y ` X(правило сечения).5)Γ, ∆ ` X2)ÌÃÒÓÌÃÒÓТеорема 2.2.

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

При этом соответствующий вывод на самом деле не строится, а лишь формулируетсязаключение о существовании такого вывода.4)ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓÔÍ-12и Y из списка Γ следует выводимость формул T → X и T → Y . Дважды удаляя импликацию ваксиоме схемы 5, получим выводимость T → X ∧ Y . Еще раз удаляя импликацию (T выводима),получаем выводимость X ∧Y . Указанную последовательность шагов можно представить в видедереваΓ`X ∧YΓ`TΓ`T →Y →(T →X ∧Y )Γ`T →YÌÃÒÓÌÃÒÓΓ`T →X ∧Y`TΓ`T →X →(T →Y →(T →X ∧Y ))Γ`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 . Остается соединить два этихвывода с выводом Γ, X, Y ` Z для получения нужного вывода Γ, X ∧ Y ` Z. Соответствующеедерево вывода имеет следующий вид:Γ, X ∧ Y ` ZÔÍ-12ÔÍ-12ÌÃÒÓ18ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙΓ, X ∧ Y ` XÌÃÒÓÌÃÒÓΓ, X ∧ Y, X ∧ Y ` ZΓ, X, X ∧ Y ` ZΓ`X ∧Y →XΓ, X, X ∧ Y ` YΓ, X, Y ` Z`X ∧Y →XΓ, X ` X ∧ Y → Y(здесь использовано упрощенное правило 2 видаΓ`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ÔÍ-12ÔÍ-12`X ∧Y →YΓ ` 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Γ ` ¬¬X → XΓ ` ¬¬X` ¬¬XОтметим, что из схемы 11 вытекает правило, обратное к правилу 8:Γ`X.Γ ` ¬¬XÌÃÒÓΓ`XÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Правило 8 опирается на схему аксиом 10 и доказывается следующим деревом:ÌÃÒÓÔÍ-12ÌÃÒÓ19Остановимся на правиле 7, которое вытекает из схем 9, 10, 11.

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

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

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

Укажем некоторыепростейшие следствия правил естественного вывода.ÔÍ-12ÌÃÒÓΓ, X, T ` XÌÃÒÓÌÃÒÓ(2.1)Γ, Y ` XΓ`XÌÃÒÓΓ`Y →XÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Γ`X, называемое присоединением посылки, вытекает изПример 2.2. а. ПравилоΓ`Y →Xправила введения импликации и правила добавления гипотез:ÌÃÒÓÔÍ-12ÌÃÒÓ20(закон противоречия) вытекает из правила введения отрицанияΓ`YΓ ` ¬¬YΓ, ¬Y ` XΓ, ¬Y ` ¬XΓ, ¬Y ` XΓ, ¬Y ` ¬XΓ`XΓ ` ¬XΓ`XÔÍ-12ÔÍ-12может быть получено из схемы аксиомв. Правило введения двойного отрицанияΓ ` ¬¬X11. Его можно также вывести из правил естественного вывода:Γ ` ¬¬XΓ, ¬X ` XÌÃÒÓÌÃÒÓΓ ` X; Γ ` ¬Xб. ПравилоΓ`Yдобавлением гипотез:ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙΓ, ¬X ` ¬XΓ`XΓ, X, ¬Y ` ¬YΓ, X ` YΓ`X ∧YΓ`X ∧Yд. Правилаиудаления конъюнкции справа вытекают из правила удалеΓ`XΓ`Yния конъюнкции (но также могут быть получены из схем аксиом 6 и 7). Например, первое изэтих правил получается применением правила сечения и правила удаления конъюнкции:Γ`XΓ, X, Y ` XВторое правило удаления конъюнкции справа можно получить аналогично. #Правила естественного вывода и их следствия позволяют доказать выводимость широкогокруга секвенций. Однако отметим, что наиболее тяжело устанавливаются выводимости видаΓ ` X ∨ Y . Правило введения дизъюнкции сводит задачу к выводу более сильного утвержденияΓ ` X или Γ ` Y .Пример 2.3. На практике для доказательства утверждения вида X ∨ Y можно рассуждатьтак: пусть X не верно, т.е. истинно ¬X.

Докажем, что тогда истинно Y .“ Этому варианту”Γ, ¬X ` YΓ, ¬Y ` Xрассуждений соответствуют правилаи, которые можно получить и в исΓ`X ∨YΓ`X ∨Yчислении высказываний. Для этого достаточно использовать правило введения отрицания иÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Γ`X ∧YÌÃÒÓÌÃÒÓΓ, X ∧ Y ` XÔÍ-12ÔÍ-12Γ, X, ¬Y ` YÌÃÒÓÌÃÒÓΓ, X ` Yг.

Полезно правилодоказательства от противного, которого вытекает из правилаΓ, ¬Y ` ¬Xвведения отрицания:Γ, ¬Y ` ¬XÌÃÒÓΓ, ¬(X ∨ Y ) ` XΓ, ¬(X ∨ Y ) ` ¬XΓ, ¬(X ∨ Y ) ` ¬¬XΓ, X ` X ∨ YΓ, ¬X ` X ∨ YΓ, X ` XΓ, ¬X ` YЭто правило назовем обобщенным правилом введения дизъюнкции.2.3. Глобальные свойства теории NВыводимые формулы и тавтологии. Непротиворечивость теории N . Полнота теории N .Разрешимость теории N . Независимость аксиом в теории N .Теорема 2.4. Любая формула, выводимая в теории N , является тавтологией. #Итак, множество формул, выводимых в теории N содержится в множестве всех тавтологий.На самом деле оба множества совпадают. Чтобы это доказать, установим одно вспомогательноеутверждение.

Как и в случае булевых функций для произвольной пропозициональной переменной x введем обозначение xσ , σ ∈ B, полагая, что x1 = x и x0 = ¬x.ÔÍ-12J Доказательство строится индукцией по построению формулы. В этом случае базис индукцииотносится к элементарным формулам, т.е. к переменным. Пусть Y = x и задано истинностноезначение α. При α = 1 имеем xα = x, Y = x, и севенция xα ` Y истинна, поскольку и левая,и правая части секвенции — одна и та же формула. При α = 0 имеем xα = ¬x, ¬Y = ¬x, иистинной является секвенция xα ` ¬Y .Чтобы доказать шаг индукции, необходимо в предположении, что утверждение верно дляформул Z и W , установить его истинность для формул (Z ∨ W ), (Z ∧ W ), (Z → W ) и (¬Z).Пусть z1 , .

. . , zn — общий список переменных формул Z и W .Рассмотрим случай Y = Z ∧ W . Для заданного набора α значений α1 , . . . , αn введемобозначение Γ = xα1 1 , . . . , xαnn . Предположим, что на наборе α истинностные функции fZ иÌÃÒÓТеорема 2.5. Пусть Y — формула, построенная на переменных x1 , . . . , xn , f (ξ1 , . . . , ξn ) —истинностная функция формулы Y , αi ∈ B, i = 1, n, — набор истинностных значений дляпеременных x1 , . . . , xn . Если f (α1 , .