1626435694-d107b4090667f8488e7fa1ea1b3d0faa (844295), страница 46
Текст из файла (страница 46)
Доказательство теоремы о дедукции Л е м и а Л1: ) — А:» А. Д о к а з а т е л ь с т в о 1. ) — А:» (А:» А) по А1 при В=А, 2. ) — (А:» ((А:» А):» А)):» ((Аэ (А:» А)):» (А:» А)) по Л2 при В = А ~ А, С = А, 3. ',— (А:» (А~ А))~ (А:» А) по П1 с оС из А1 при В ° =А:»А иФ~Я изп 2. 4.
~ — А ~ А по П1 с ИС из и. 1 и ~Ф:» я из п. 3. ту Пусть формула В выводится из формул Аы..., А„. Распре- делим формулы, образующие дерево условного вывода, по ярусам. В первый ярус попадут все термннальнью вершины. В >сй ярус попадают вершины, имеющие среди предшественников хотя бы одну вершину ($ — 1)-го яруса. Теорема будет доказана иидук- цией по числу ярусов в дереве вывода. В первом ярусе находятся либо выводимые форыулы (аксиомы), либо формулы из списка Аы..., А„. Докажем, что любая 216 ГЛ- С. КРАТКОЕ ПОВТОРЕНИЕ МАТЕМАТИЧЕСКОЙ ЛОГИКИ формулаВиз1-го яруса удовлетворяеттеореме.
Если  — выводимая формула, то,взяв в П1 в качестве посылок В н В~ (А„:» =» В), получим в качестве заключения ) — А„~ В. Если В = А„, то по лемме Л1 получаем )-А„~ А„. Если В = А~ (г ~ и), то, взяв по аксиоме А1 выводимую формулу А~-» (А„:» А;) и А~ в качестве посылок правила П1, получим, что А~ )- А„~ Ао По определению условной выводимости получаем, что для формул В первого яруса справедливо Аы..., А„ь )-А„~ В. то Аь..., Амб 'Ф' (»А» А) ((»А»А) А) »А »А Л1 П1 гл 3)~((ь 3у~фч~~ гг)) П1 АР...,Амб' 7 А,,:.. (с"~~)) ((Вчф~Д Т1 ® тф~ (»А »А) А П1 Рнс.
6.3. деревья вывода в исчислении выспааываннй. Ам...,Ае, В)-Р Ат.— А» С) — Р. а) Метатеорома Т8: " ' А ~' и С )» ' о) Сенвенцнн Т10: ) А )- А. ап обозначение условного вывода, )3: применение метато- оремы, у: посылка условного вывода, 6: подстановка в схему аксиомы. Рассмотрим любую формулу В из г-го яруса и допустим справедливость теоремы для любой формулы из ярусов с меньшими номерами. Формула В получается применением правила П1 к посылкам А и А~ В, для которых по индуктивному допущению как А„:» А, так и А„л (А:» В) выводимы из Ам ..., Ао м Взяв в аксиоме А2 А„= А, А = В и В = С получим выводимую формулу (А„~ (А~ В)):» ((А„:» А)~ (А„~ В)). Ваяв зту формулу в качестве м!:» В1 и А„:» (А:» В) в качестве,ф в П1, э е.з.
исчисления Высклзывлннн получим Ап . ° " Ал-«) — (Ал-» А)~ (Ап~ В). Взяв снова в П1формулу (А„~ А)~ (А„~ В) в качестве ву=» Я и А„~ А в качествем!, получим заключение Ап..., А„г) — А„~ В. Теоре ма о дедукции доказана.~7~7 Теорема о дедукции, а также правила Т8 и Т9, являют собой примеры таких утверждений о выводимостн, которые доказываются не только записьЮ формального вывода в исчислении, но и некоторым общим и неформальным рассуждением о той или иной выводимости без ее конкретного изображения. Этот «второйэ слой логического рассуждения приводит к тому, что подобного рода утверждения называют метатеоремамн.
На рис. 6.3 изображено дерево условного вывода метатеоремы Т8 (прннцип доказательства разбором случаев) и секвенцин Т10 (снятие двойного отрицания). Построенные правила вывода позволяют сблизить аксиоматику исчисления высказываний с правилами равносильных преобразований логических формул. Понимая сокращенную запись (А) = (В) как схему формулы ((А)=» (В)) дс ((В)~ (А)), мы можем сформулировать / в исчислении известные свойства операции тождества, а также связь выводимости с общезначимостью. Т11: ) — А=А, Т12: А= — В» — В=А, Т13: А=В, В=С)-А=С, Т14. 'А, А= — В)-В, Т15.: ) — А )/ ~А.
Для Т13 требуется очевидная лемма о транзитивности импликации. Л2:А~В, В~С) — А~С„ которая, хотя и содержится неявно в аксиоме А2, получается не сразу из нее, а е помощью теоремы о дедукции: из трех посылок А, А =» В, В:3 С о помощью двукратного применения П1 выводится С, после чего по теореме о дедукции получаем условную выводимость А ~ С. Рис. 6.4 показывает вывод Т15 (закон исключенного третьего).
В отличие от исчисления равносильностей логических функций, правило подстановки в исчислении высказываний не аксиоматнзируется (правило П2 в Т), а доказывается в виде так называемой «теоремы о аамене». Т е о р е ма 9. Пусть С (А) — формула, в которой выделено вхождение формулы А, а С (В) — формула, которая получается $ ал.
исчислеиии ВысКАэыиаыий 219 (А В)ж(В А) ф Я П1 (П1) ~~Ит~~— (А»С) Ю) (В С) (А С) тз ((А"С) (В С))е((В-С)-(А СЭ а) С АСВ В СчА (А В)л(В 4) Ав (А-В) (В () АВ ЮКОВ)У 1СчВЪ ЦчА) (СиВ3 ~КМСиАЗР(В$4ЦРКчВ) (Сч43 С В АЗ С В . С А (д~фС А 47 А АВ АБ А7 В ВА АП В=(СчЯ П1 С (СуВ) 4-(С,А) '~й1~ СъДж В П1 Х П1 П1 ЩчВЗ ((СчА) (СчВА ф $ч(СчАЭ ((СчВ) (Сечи) чВ)-Фч4) (СчА) (СчВ) а44) М,Суй г ЧЧЦ ЧчА В ф Рис.
6.5. Вывод лемм из теоремы о земеле. е) А=В) — А'лСыВ~С. е) Аи— и В)-Суу'А=Сч/В. КЮ Гл. 6. кРАткои повтОРБние ИАткмАтическои лОГики С (А) имеет одну из следующих форм: С(А) =(М(А)):Э(Х), (Х):» (М (А)), (М(А)) 8с (Х), (Х) Й(М(А)), (М(А)) )/ (Х), (Х) ~/ (М (А)), $М(А); при этом глубина вхождения А в М (А) равна д, а, стало быть, по предположению индукции имеет место секвенция: А=В~ — М (А) =М (В). Сформулируем следующие Леммы: ЛЗ: А=В)-А:»С=В~С„ Л4: А=В)-С:»А=С:»В, Л5: А= — В) — А8сСшВЬС, Л6: А=В)-СЬА=СЬВ, Л7: А = В ) — А ~/ С еи В )/ С, Л8: А = В ) — С ~/ А ж С ~/ В, Л9: А=— В) — ~Ави ~В. Для примера доказательства нескольких из них даны на рис. 6.5.
После этого проведем для каждой из синтаксических форм для С (А) рассуждение по следующей схеме. Пусть С (А) = — М (А) рг(. По предположению индукции А=В)-М(А) = М(В). По соответствующей лемме имеем М (А) еи М (В) ) — М (А) рХ = М (В) рХ, что в силу транзитнвности свойства выводимости дает А = В )- )- С (А) вм С (В), что и требовалось доказать.тут7 Включение в исчисление знака тождества и обоснование его свойств позволяет доказать в исчислении в виде выводимых схем формул все тождественные равенства булевых функций (1) — (39) (с использованием формул вида В ~/ ) В и В й ) В вместо 1 и $ соответственно). Большая часть выводимостей получается прямым применением подходящих аксиом и правил вывода Т1 — Т10, 5 6.3.
исчислении ВыскАзыВАний 22т однако некоторые выводы достаточно длинны: пример доказательства дистрибутивного свойства конъюнкции по отношению к дизъюнкцни дан на рис. 6.6. АаВ ~Аы)чйаД я тс с1;,~7 т~ В,В,~~~~,В ~„СВ Аз4Вч4 В п~ ЧАС)~(Аайучй аСЪ Т1 рарчСВ ~ аВ)ч(4а ЯаВ)ч$ий4МЯчСЦ ЯЩВчС$ иЯЙВ~чЯЙС$ Ркс. 6.6. Вывод дкстрибутивиости конъюнкции отиоситолько дивъюккцки.
Полнота, непротиворечивость и независимость. Наше изучение исчисления высказываний подходит к концу. Наметим доказательство полноты исчисления т,. Пусть дана общезначимая формула А. С помощью цепочки тождественных преобразований с использованием теоремы' о замене мы получим выводнмость )- А — К, где Ка — совершенная нормальная дизъюнктивная форма. Поскольку А общезначима, Кь должна содержать полный набор элементарных конъюнкций, который очень просто с помощью тождественных преобразований представить в форме ~й-, Ч -1 Х,>В...
В~Х. Ч -1 Х.~. Тзз ГЛ. 6. КРАТКОЕ ПОВТОРЕНИЕ МАТЕМАТИЧЕСКОЙ ЛОГИКИ что в свою очередь преобразуется в выводимую формулу вида В ~/ ) В. По Т15 имеем (- В ~/ ) В, откуда по Т14 получаем выводимость А. Непротиворечивость вытекает из корректности и из того, что отрицание любой общезначимой формулы есть формула необщезначимая. Полнота в узком смысле устанавливается следующим рассуждением.
Пусть А — невыводимая в исчислении Ь формула. В силу полноты Ь А не общезначима. Пусть Х„..., Х „— переменные в формуле А и пп..., ΄— набор значений, на которых интерпретация А имеет значение 1. Заменим в А все вхождения переменной Х, формулой Х ~/ ) Х, если а, = 1, и ) (Х 1/ )Х), если с~ = Ь В результате мы получим формулу А', которая„ оставаясь невыводимой в Ь в), имеет к тому же тогкдественно ложную интерпретацию. Но тогда в 1 будет выводима ) А'. Включим теперь В в качестве схемы аксиомы в Ь, заменив ее переменные на метапеременные. Получим исчисление Ь', в котором будет выводима формула А.
Поскольку правила подстановки формул на место переменных в Ь' сохраняют силу, формула А" также окажется выводимой в Ь, что приводит к противоречию с выводимостью ) А'в Ь'. Точное доказательство полноты в узком смысле требует следующей теоремы. Т е о р е м а 10 (о подстановке). Пусть А(Х) — формула со всеми выделенными вхожденилзш переменной Х и А (В) — формула, полученная подегпановлой формулы В во все вхождения Х. Увода, если (- А (Х), то (- А (В). Д о к а а а т е л ь с т в о.
Рассмотрим дерево вывода В формулы А (Х) и выделим все вхождения переменной Х во все терминальные формулы. Каждая из зтих формул представляет собой аксиому, содержащую метапеременные Мд,..., Мю замененкые на какие-то их фиксированные значения С,(Х), ..., Се(Х). При замене всехвхожденийХ на В мыло-прежнему получим правильное применение аксиомы с метапеременнымн Мп..., Мю замененными на значения С,(В),..., Сь(В).
Проделавтакие жезамены во всех нетерминальных формулах вывода )л, мы получим правильное деревовыводаР с заключительной формулой А (В). с~ ~, Доказатйльсгво независимости аксиом и правил вывода в некотором исчислении, хотя и проходит обычно по общей схеме, но требует немалой изобретательности и хорошего понимания аксиоматики, как в ее содержательном смысле, так и в ее формальном (текстовом) представлении.
С каждой аксиомой (или правилом вывода) связывается некоторое конкретное свойство формул или их интерпретаций. Это свойство, с одной стороны, должно быть ч) Если бы А'оказалась зызодвмой, то, осуществив обратную подстановку, ны поаучпля бы выводнмость А $6.3. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ 223 нетривиальным, т. е. среди выводимых должны быть формулы как обладающие, так и не обладающие этим свойством. С другой стороны, подмножество М формул, выводимых без применения данной аксиомы, должно быть замкнутымпо отношению к свойству, т. е.
формулы из М должны все либо обладать, либо не обладать этим свойством. Тем самым обнаруживается неполнота Исчисления без данной аксиомы. Приведем два характерных примера доказательства независимости аксиом исчисления ) . Независимость аксиомы А9: ( ( А:» 1 В) ~ (( ) А:» В) ~А). Если А — формула, то Ь(А) — формула, полученная из А устранени- ем всех вхождений знйка ~. Например, Ь( ~Х~/ ~У):» ) 1Х) = (Х ~/ У) ~ Х.
Утверждается, что если А — любая формула, полученная за- меной метапеременных на их значения в любой иэ схем ак- сиом А1 — А8, то Ь(А) будет общезначимой формулой. Для этого достаточно убедиться, что для любой из этих схем: Ь(А) так же получается иэ данной схемы, как и А. Например,, для А5 имеем Ь((А)/ ~В) ~( ~С.:» ((А ~/ ~В) Ь ~С))) =(А)/ В):» :» (С ~ ((А ~/ В) й С)). Назовем свойство выводимой формулы А иметь общезначимую Ь(А) консервативностью А. Очевйдно, что если А и А:»  — консервативные формулы, то н В тоже будет консервативной. Итак, мы обнаружили, что множество формул, выводимых в исчислении Б без аксиомы А9, обладаег свойством консервативности. В то же время (если взять в А9 А В = А) формула Ь(( )А~ 1А):»(( ~А~А)~А))=(А~А):»((А~А):»А) не является общезначимой (равна $ при А = 1) и, стало быть,, формула ( ~А~ ~А)~(( ~А~А)~А) не выводима в 1 без А9.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
