Математическая логика. Шапорев С.Д (1019113), страница 20
Текст из файла (страница 20)
е. Г, = (А,,Аз,..., 1„А)-. Ото равносильно условию, чта В~-, где В=А, а~ л...лА„А.. Тлаее 2. Мошсле ие енсказнынив гза Приведем формулу В к КНФ т е к виду В=С лС л...лСв. Тогда если В~-, то С, л Сз л... лС,„~ †. Таким образом, ждала проверки выводимссти (Ан Аз,..., А„)) — А сводится к проверке противоречивости мноэкества дизъюнктов з; = (С„Сз,...,С„,), а это равносильно существованию резолютивного вывода нуля из З, Пример 3. Проверим методом резолюций выводимость Г = (А — э В л С В -э Р С вЂ” э Е А — е Г 3-(Р л Е)ч Г.
Выводимщзь данной формулы ю Г по этому методу слеаует из противоречивости множества Г, =(А — эВлС, — эО,С вЂ” эЕ,А — э Г,ОЕчГ), Приведем всеформулыиз Г, кКНФ: г', = Дч ВС,Вч О,СчЕ,АчГ, Г л (О ч Е))= (А ч В)(А ч С) В ч 0 Сч Е, А ч Г, Г(0 ч Е)). Таким образом, множество дизъюнктов Р," =фдчВ,ЛчС,ВчО,С гЕ АчГ,Г,ОчЕ), Построим возможный резолютивный вывод нуля из Г,: й гезл(Л г В,Ач Г)= Вч Г; 2, гезл(АчС,гзчГ)=СчГ; 3. геле (В ч О, В и Г) = Оч Г; 4. ггзг(СчГ,СчЕ)=ГчГ; 5 гезк(ЕчГ,ОчЕ)=ОчГ; б, гезо (О ч Р', О и Г)= Г ч Г = Г; 7. гез(Г,Г)=0. На практике в общем случае метод резолюций не эффективен, т, к, число переборов резольвент может быть очень большим, оно экспаненцнально зависит от числа лизъюнктов и содерэкашихся в ннл переменных Метод успешно применяется к одному классу дизъюиктов — корцовским дизьюнктам.
Дизъюнкт А называется ксрлоеслкн, если оп содержит не более одной позитивной переменной, например Л ч В ч С, А ч С, А, В. В общем случае Ч Г Ы гвмвлынсная лагина Г34 хорновские дизьюнкты имеют вид А, чА, ч ... ч А„нли А,чА,ч...чА„ЧВ. Хорнавскнй дизъюнкт вида А,чАзч.,чА„ называется негоотвныч, а дизьюнкг Л, ч АЧ ч... ч А, г  — точным. Дизьюнкт А нвзываета» унитарным иозитиоиым А аьюинтом, Если à — множество хорновских дизъюнктав, то его проверка на противоречивость происходит следующим образом. В Г выбирается унитарный позитивный дизъюнкт В и дизъюнкт Си Г, содержащий В . Далее Г заменяется на ГгтгС'роуезеС,В)77.
Этот пропеса продолжается ла тех пор, пака либо Г не будет содержать б, либо не найдется дизъюнктов В н С указанного вида. В первом случае искодное множество Г противоречиво, во втором непротиворечиво. Пример 4. Проверим иа противоречивость множество Г=(А — г В Се О, — ь Е,Π— г Р,ЕГ А — ьС А7'=- = (А ч В, С 'г О, В ч Е Оч Р, Еч Р, Ач С, А).
Множество содержит только хорновские дизъюнкгы Применим к нему описанный алгоритм по шагаы: Е гезЯЛ, А и В) = В, (А, В, С ч О. В ч Е, О и Г, Гч Е А ч С); 2, тзе(В,ВЧЕ)=Е, (ЛВЕСчО,ОЧР,ЕчГАЧС); 3 гене(ЕЕчр)=Р, (ЛВ,Е,РСЧООчЕ,АчС); 4, гезггР,Очр)мО, ~АВ,ОЕРСчО,АЧС) 5. геня(А,ЛЧС)мС, (А,В,С,О,Е, Г,Сч Оуг 6. тел-(С,СчО)мО, (АВ,С,О,О,Е,Р) 7. гег(О, О)= О.
Множество Г противоречиво. 2.8. Проблемы аксиоматического исчисления высказываний Исчисление высказываний как всякел аксиоматическая теория для ыюего обоснования требует решения четырех нроблем: разрешимости, непративоречиваати, полноты, нсзависимоати. Рассмотрим их все кратко. !зз Глаэаэ Исчосл оо вм коэн олй Перш» проблема — проблеча разрешимости — шключается в там, что доллген существовать алгоритм, позволяющий лля любой зэданной формулы исчисления высказываний определять, является ли она доказуемой нлп нет Такай алгоритм сушсстьует.
Действительно, лнэбая формула исчисления высказыьаний может раасматриваться как формула алгебры высказываний, дпя контрой зга проблема решается с помощью теорем 1 9-1 12 )см. рагд !.13) Взора» проблема — непрашворсчивхть исчисления высккшваний. Фарьгачыбю аксиоыпичсскую теаршо ншь1вают лелрашиааречшой, шли не существует формулы А такой, па в исчисленииодновременно выводимы А и А. Теорема 2.8 Исчисление высказываний непротиворечиво.
Действительно, по теореме 2.4 всякая выволимая формула тждсствеггно потника. Отрицание этой формулы не является тождественно пстннной формулой. Следовательно, нп лля какой формулы А невозпожно. чтобы одновременно ~- А и ~- А Третья проблена — это проблема полноты. Она имеет два аспекта: полногу в узкоч и в широком смысле Аксиоматичсское исчисление называется лалчмн а узком смыаэе, если лобавленис к списку ега аксиом любой недоказуемой в ис ~калении формулы в качестве новой аксиомы приводит к противоречивому исчислению.
Теорема 2 9 Ис гислепне высказываний полно в узком смысле. Доказашелестеа Пусть А — произвольная невыводимая формула (по теареме 2.7 л качестве А можно взять любую ншождсснюнно истинную формулу), а хчх,...,х„— список ее переменных. Так как А — нсвыводичая формула, г ''' то сушествусг набор значений амат,...,а„переменных такой, что А(х„хг,...,х„~ = О. Пусп В,,В,,...,„— любые тождественно истинные формулы, зависяшпе ат переченньш х,, х„, к„рассмотрим слсдуюший набор формул )Воо, =1 В"', В",...,В,";, где В,' = ~ †' , и осуществим их подстановку г гс' к',ээ в Формулу А: ) А = А(В,"', В", В"" )и О Действительна, для Част 1.
Ыег магич сюялогляя любого набора а„оз,...,о„значений переменных Вг(~,х„...,х„) — 1, т. к,  — тождественно истинная формула. Тогда:Ц"'(х„~,...,х„~ — = с, и А!1лч,уц',...,В„'")=А!инат„..,а„)мб. тождественно истинная формула и, следовательно, по теореме 2.б выводима в исчислении высказываний. С другой стороны, если формулу А(х„х„...,х„) добавить к списку аксиом нсчислени», то она станет выводимой в новом исчислении «ак аксиома. дчд,,ел В новом исчислении формула А(Вч,бз ....В;,")= ) А(х,х„...,хк) получается в результате одновременной подстановки, т.е.
также будет выводимой, Следовательно, новое исчисление высказываний будет противоречивым,т. к. е нем ~ — А и ~-А. дксиоматическсе исчисление называется иолнын е глирокож смысле, если любая тождественно истинная формула в нем доказуема. Проблема полноты в широком смысле решается также положительно. Справедливость этого факта следует из теоремы 2.6. Наконец, последняя проблема — проблема нежвисимостн — заключается в независимости системы ее аксиом, т е.
в невыводимости любой из них из остальнык аксиом по правилам вывода данной системы. Оказывается, что система аксиом исчисления высказынаний независима. Этот факт довольна легко проверяется непосредственно, если явным образом определить множество, из которого принимшот значения переменные х, у, я. Теореме 210. Система аксиом исчислении выскюываиий июавнсима. Доказательство независимости всех одиннадцати аксиом исчисления высказываний довольно громоздко н основано на некоторых интерпретациях переменных и логических операций исчисления. Независимость самых простых аксиом можно доказать по следующей скеме. Допускается, что переменные в аксиомах могут принимать только два значения: ! н О.
Все логические операции , л,ч, -Ь, кроме одной, определяются так же, как и в гшгебре высказываний, причем ! играет роль истины, а б — лжи. Одну же из логических операций специаяьно определяют так, чтобы та аксиома, в которую эта операция входит и независимость «огород доказываеюя, не являлась тождественно равной !. йщва д П чмленнв высказываний гзу Ври такой инщрпретации все аксиомм кроне исслютуемой, принимают значение 1 Все формулы, выводиьгые из сово|супности аксиом, кроме исследуемой, также будут принимать значений 1 при всех значениях входящих в них парамез ров Ясно, что если така» интерпретация возможна, то исследуемая аксиома не зависит от остальных, т. к если бы она была выводиьга из остальных, то она, как и все формулы, ныводимые из совокупности аксиом, кроме исследуемой, прнниьмла бы только значение, равное 1.
2.Э. Практическое занятие йз 6. Эквивалентность формул исчисления высказываний и теорема о выводимости. Алгоритмы Квайна, редукций и резолюций 2 9.1. Вывести следующие секвенцни. а) ~ — АлВьч В л А; б) ) — Л ы В г-з В ы Л 2.9.2. Доказать, что в исчислении высказываний выводимы секвегщии; а) )- А я-з Л; б) (А я-з В) — (С ь А) «-з (С -ь В) . 2.9.3. Доказать, что следующие формулы выводимы в исчислении высказываний: а) ~ — Л ы В г-з А л В; б) Ая-з А. 2.9 4. Используя свойство монотонного возрасгания изн убыиапил функций, доказать выводимость следующих формул; а) А= х — з (х-ь(х — ч улх)); б) А= злу-ту-+ у 29В.
Используя свойство монотонного возрастани» дизыонкции но обеим переменным, доказать вьщоднмость формулы Чаще Г Лмг млочаглвялспям 2.9.6 Дана формула А= хоуч(х-+ у)лх и наборы значений переменных а) (1,!), б) (О,О). Записать вывод формул А или А из озствеютвующей совокупности формул. 297. Формула А= х, ч х ч х, задана на наборах а) (О 0 !) и б) (1 ОО) Вывести А или А нз соответствующей совокупности формул.
2.9.8. Формула А= (хь у) л (у-з з)-+ (х-ч х) задана на наборах а) (О, О, !) и б) (1,1,1). Записать вывод формулы А нли ее отрицания из множеств Г, =~У,з)!и Гг =(ЩУ Я). 2.9.9. Дана формул» А=ц их -+хз и наборы значений переменных а) (1,1,!), б) (1,0,1), в) (О, 1, 0). Записать вывод А или А из соответствующей совокупности форыул.