Игошин Математическая логика и теория алгоритмов (1019110), страница 32
Текст из файла (страница 32)
Продумайте самостоятельно эти взаимосвязи. б) Строим последовательность формул, которая также выводом не является, а служит лишь обоснованием возможности по- 128 [использована гипотеза]; [теорема 15.8, а]; [лемма 15.7, ьс (2), (1)]; строения такого вывода, но которую можно дополнить до вывода без принципиальных трудностей: (1): ( — Г-+-Г) -+ ((- - Г-» Г) -» Г)) [аксиома (АЗ)]; (2): — Г-» - Г [теорема 15.8, а]; (3): (- . à — »Г) — » Г [правило МР: (1), (2)]; (4): Г-+ ( — à — » Г) [аксиома (А1)]; (5): Г-» Г [лемма 15.7, гд (4), (3)]. в) В двух предыдущих доказательствах теорема о дедукции применялась опосредованно через лемму 15.7.
В настоящей задаче происходит прямое применение этой теоремы. Это делается следующим образом. Покажем сначала, что — Г, Г»- 6. Приводим соответствующий вывод, обосновать который предлагается самостоятельно (это уже действительно вывод, но пока еще вывод из гипотез — вывод формулы 6 из гипотез — Г, Г): (1): -Г; (2): Г; (3): Г-+ (-6-» Г); (4): — à — » (- 6 — » — Г); (5): -6-» Г; (6): -6-+ -Г; (7): (- 6 -+ — Г) -+ ((- 6 -+ Г) -+ 6); (8): (-6 — » Г) -+ 6; (9): 6. Итак, Г, Г»- 6. Тогда по теореме о дедукции Г»- à — » 6. Применяя еше раз теорему о дедукции, получаем»--à — » (à — » 6). г) Покажем, что — 6 — » Г, Г»- 6.
Для этого строим соответствующий вывод (обоснуйте его самостоятельно): (1): -6-+ -Г; (2): Г; (3): (-6-»-Г) -+ ((-6-» Г) -+ 6); (4): (-,6 — » Г) -+ 6; (5): Г-+ ( 6-» Г); (6): 6-» Г; (7): 6. Итак, 6-+ Г, Г»- 6. Применив теперь дважды теорему о делукции, получаем требуемый результат. д) Покажем сначала, что à — » 6»- — 6-» —,Г. Строим последовательность формул, которая выводом не является (снова обращаемся к лемме 15.7 и еще к доказанным выше теоремам), но может быть дополнена до такового: (1): Г-+ 6 (2): Г-» Г (3): Г-» 6 »И шин 129 (4): 6 -> 6 [теорема 15.8, б]; (5): Г-э 6 [лемма 15.7, ьл (3), (4)]; (6): (- 6-+ р) — ~ ( р — > 6) [теорема !5.8, г]; (7): — Г-~ 6 [правило МР: (5), (6)], Применив теорему о дедукции, получаем требуемое утверждение. е) По правилу МР имеем Г, г" — + 6 ~- 6.
Тогда по теореме о дедукции г" ~- (г" — ~ 6) -+ 6. Применяем еще раз теорему о дедукции: ь- г — ~ ((г — ~ 6) — ~ 6). Далее, по пункту д) настоящей теоремы имеем (взяв в качестве г формулу Г-+ 6, а в качестве 6— саму 6): ((Г-~ 6) — ~ 6) — ~ (-,6-+ (Р-+ 6)). Из этих двух последних утверждений на основании леммы 15.7, а получаем ~- г" — > — >(- 6-э -(г — > 6)).
ж) Покажем сначала, что Р-+ 6, Р-~ 6 ~ — 6. В самом деле, строим соответствующую последовательность (определите самостоятельно, что это — вывод из гипотез или обоснование возможности его построения): (1): Р-~ 6; (2): Р-> 6; (3): (г — э 6) -+ (-6-+ г"); (4): - 6 -+ - Г; (5): (-Х-э 6) -э (-6 — э г"); (6): -6 -+ — Г; (7): (- 6 — э — г") -+ ((- 6 -+ - г") -+ 6); (8): (- 6 -+ — г") — э 6; (9): 6. Итак, г — > 6, — Р-э 6 ~- 6. Следовательно, по теореме о дедукции г" — ~ 6 ь- ( г" — э 6) -+ 6.
Еще раз применяя теорему о дедукции, получаем: (г"-> 6) -+ ((- Р-+ 6) -> 6). Производные правила вывода. Аксиоматическая теория высказываний развита довольно глубоко: теорема о дедукции, вскрыв важное свойство выводимости, оказалась мощным средством, облегчающим доказательства того, что та или иная формула является теоремой формализованного исчисления высказываний.
Следующим шагом на этом пути служит выявление дальнейших закономерностей процесса выведения одних формул из других и формулировка таких закономерностей в виде правил вывода. Получаемые вторичные правила вывода носят название производных правил вывода. Разделим их на две группы и сформулируем их в двух теоремах: в одной — производные правила введения логических связок, в другой — производные правила удаления таких связок.
Для формулировки правил будет использоваться символическая запись. Например, правило Г ~-Г; Г ~ — Г -э 6 Г ь-6 состоит в следующем: «Если Г ~ — г и Г ь- г"-+ 6, то Г ь- 6». 130 Теорема 15.9 (правила введения логических связок). Справедливы следующие производные правила вывода, называемые правилами введения логических связок (где à — некоторое, возможно и пустое, множество формул): а) введение импликации (-»-вв): Г» — à — »б' б) введение конъюнкции (л-вв): Г»- Г; Г»-6 Г» — Гл6 в) введение дизъюнкции ( г-вв): Г»-6 Г»-Г Г» — Г гб* Г» — Гчб' г) введение отрицания (приведение к абсурду) ( -вв): Г, Г»-6; Г,Г»- 6 Доказательство.
а) Данное правило есть не что иное, как теорема о дедукции (теорема 15.4). б) Обосновать правило предлагается самостоятельно. Напомним только, что запись Г л б, согласно определению, означает -(à — »- 6). в) Обоснуем первое правило. При доказательстве теоремы 15.8, в показано, что Г, Г»- 6, или Г, Г»- 6. Отсюда, по теореме о лелукции, заключаем, что Г»- à — » 6, т.е. на основании опрелеления логической связки дизъюнкции Г»- Гч 6.
Поэтому если Г»- Г, то отсюда, в силу теоремы 15.3, в, заключаем, что Г»- Г г 6, Обосновать второе правило введения дизъюнкции предлагается самостоятельно. г) Пусть дано, что Г, Г»- 6 и Г, Г»- 6. Тогда, по теореме о делукции, Г»- Г-» би Г»- à — » 6. Выпишем одну за другой обе последовательности формул, представляющие собой выводы формул à — » б и Г-» б из множества посылок Г: (с») Г» б; (а+ )3) à — » 6. 131 Продолжим полученную последовательность следующим образом: (и+ ]3+ 1) (Г-~ 6) — ~ ( 6 -~ Г) [использована теорема 15.8, д]; (а+ ]3+ 2) 6 -ч Г [МР: (сс), (а+ ]3 -ь 1)]; (и+]3+ 3) (-6-э Г) -+ ( Г-э 6) [теорема 15.8, д]; (и+ ]3 -ь 4) Г-+ 6 [МР: (а+ ]3+ 2), (а+ ]3+ 3)]; (сс+ [3+ 5) (Г-> 6) — э ( 6 -+ Г) [теорема 15.8, д]; (а+ [3+ 6) 6 — э Г [МР: (и+ ]3), (а+ ]3 + 5)]; (а+ ]3+ 7) (- 6 — ~ —,Г) -~ (-, à — ч — 6) [теорема 15.8, д]; (а+р+8) Г ~ 6 [МР: (и+ ]3 + 6), (и+ [3 + 7)]; (а+]3+9) .
б-э 6 [теорема 15.8, а]; (а+ ]3+ 10) Г-+ — 6 [лемма 15.7 а: (а+ р+ 8), (а+ ]3+ 9)]; (о+]3+11) (- Г-э- 6) -ь(( à — э — 6) -э-Г)[аксиома(АЗ)]; (а+]3+ 12) (- Г-+ -6) — э Г [МР: (а+ ]3 ч-4), (и+]3+!1)]; (а+ [3+ 13) Г [МР: (и+ ]3 + 10), (а+ ]3 + 12)]. Тем самым доказано, что Г ь- .Г. П Теорема 15.10 (правила удаления логических связок). Справедливы следующие производные правила вывода, называемые правилами удаления логических связок (где à — некоторое, возможно и пустое, множество формул): а) удаление импликации (-~-уд): Г ь- Г; Г ь- à — ~ 6 Гь-б б) удаление конъюнкции (н-уд): Гь-Гпб Гь-Гоб Гь-Г ' Гь-6 в) удаление коньюнкции (н-уд): Г,Г,6~ — Н Г,Глбь-Н ' г) удаление дизьюнкции (Генцем): Гь-Гч 6; Г,Гь-Н; Г,бь-Н Гь-Н д) удаление дизъюнкции (Клина): Г, Г>-Н; Г,бь-Н Г, Гг бь-Н 132 е) сильное удаление отрицании (сильное — уд): Г»-- Г Г» — Г ж) слабое удаление отрицания (слабое -уд): Г»-Г; Г»- — Г Г»-6 Доказательство.
а) Это правило получается непосредственно на основании правила вывода МР. б) Обоснуем второе из двух правил удаления конъюнкции, предоставив сделать обоснование первого правила самостоятельно. Пусть Г»- Гс, 6. Покажем, что Гл 6»- б. Напомним, что по определению конъюнкции запись Гл 6 означает — (à — » — 6). Поэтому нужно показать, что — (à — » — 6)»- 6.
Строим соответствуюший вывод: (1): -(à — » — 6) [использована гипотеза]; (2): — (Г-» — 6) — » ( 6 — » — (Г-» —,6)) [аксиома (А1)]; (3): -б-+-(à — »-6) [МР: (1), (2)]; (4): (- б -+ - (Г-+ — 6)) — » ((- б-+ (Г-+ — 6)) -+ 6) [аксиома (АЗ)]; (5): (-6-+ (à — »-6)) -+ б [МР: (3), (4)]; (6): -6 — »(à — »-6) [аксиома (А1)]; (7): б [МР: (5), (6)]. Итак, Г»- Гл б и Гл 6»- 6. Следовательно, по теореме 15.3, в заключаем, что Г»- 6. е) Пусть Г»- Г Ввиду теоремы 15.8, а имеем»- à — » Г, что на основании следствия 15.6 из теоремы о дедукции дает выводимость- Г» — — » Г Следовательно, из двух выводимостей Г»- Ги Г»- — » Г по теореме 15.3, о заключаем, что Г»- Г Остальные правила вывода рассматриваются в Задачнике (см. )Чь 8.19, 8.20). Там же в задачах Хь 8.21 и 8.22 приведены примеры доказательств с использованием производных правил вывода.
П й 16. Полнота и другие свойства формализованного исчисления высказываний Если при изложении материала 8 15 рассмотрение велось как бы изнутри аксиоматической теории высказываний в процессе Развития темы, то ознакомление с наукой об аксиоматической теории высказываний строят, опираясь на другой подход. установим ряд важных свойств этой теории: полноту, разрешимость, непротиворечивость. 133 Доказуемость формулы и ее тождественная истинность (синтаксис и семантика). В основе формализованного исчисления высказываний лежат понятия, относящиеся к так называемой области синтаксиса, т.е. понятия, представляющие собой некие абстрактные, лишенные смысла знаки и формальные действия с ними: алфавит, формула, аксиома, правило вывода, доказательство, теорема.
Эти понятия принято называть синтаксическими. В то же время алгебра высказываний, изложенная в гл.!, пронизана содержательным смыслом: за каждой пропозициональной переменной стоит конкретное высказывание нашего языка, каждая формула может превращаться в конкретное составное высказывание, некоторые формулы могут превращаться только в истинные высказывания (тавтологии) и т.д. В данной сфере, являющейся областью семантики, каждое понятие наполнено каким-то внутренним содержанием, смыслом. Понятия истины и лжи, тождественной истинности и тождественной ложности формул, равносильности и логического следования формул считают понятиями семантическими. Каково же взаимоотношение между формализованным исчислением высказываний и алгеброй высказываний, между синтаксисом и семантикой? Перекинуть мостик от одной области к другой и призвана теорема полноты, о которой пойдет речь в настоящем параграфе.