Математическая логика. Шапорев С.Д (1019113), страница 16
Текст из файла (страница 16)
Мвгемвшчвск ял пм доказуема". Правило широко распространено и известно очень давно. на латыни оно называется шобщ рспепз. )ксионш) называется всякое выражение, полученное из схемы аксиом 1-!Ч подстановкой вместо переменных х, у, т конкретной формулы. Лнггешгым доказаегельстивоы 1выеодолг) в нс ~ислсинн высказываний называешя конечная последовательношь секвенций Х,, Х„ ,Х,, такая, что для кюкдаю 1, 1 < э б к, Х, есть либо аксиома, либо непосредственное счедствие предыдущих секвенций по применяемым в исчислении правилам вывода.
Секвеиция Х называется долот)смой л исчислении высказываний или теоремой исчисления, если существует доказатсвьство Х,,Х ,,.,,Хь, у которого Х, =Х. Формула А нюываетсв доказукыой, если доказуема секвенция ~- Л. Очевидна, что всякал секвенция является деревом; если 1)„т)з,...,т)г— 2)„2)„...,В, деревья и Х вЂ” ссквенция, то '' * "* — ь — также дерева.
Одна и та жс Х секвенци» мазкет входить в дерево несколько раз. Дерево моягет иметь много начальных секвенций, но заключительная секвенпия только одна. Дерево т) называется докатолгетгьсвмон в исчислении высказываний в ниле дерева, если все его начальные секвенцни — аксиомы, а переходы— применения допустимых правил вывода. Если Х является заключителыюй секвенцией доказательства О в виде деревж то О называется докозошельстваи Х в ваде дерева илн деревом вмво)о Х в исчислении высказываний. Схема секвенций называется доказуемой в исчислении высказываний, если ее добавление к исчислению в качестве схемы аксиом не раснгнряет множество доказуеммх секвенций. Это эквивалентно тому, что вое частные случаи этой схемы будут доказуемы в исчислении высказываний.
2.2. Некоторые дополнительные производные правила вывода Из списка перечисленных тринадцати правил вывода (2.1.2) некоторые практически всегда применвются при доказательстве теорем. Рассмогрни доказательство еше нескольких правил вывода. Онн получаются с помощью Глана д исчислена аи х алканий лрааил подстановки и простого закжочения и лотгому ляля~гноя лрсизаолн ы ми от них.
Правило олнаарсмснной подстаиааки ПУсть Л вЂ” доказУсмаа фоРмУла; хилз...г —. нсРсмснныс, з В, В„, „— любые формулы исчислсния яысказыаапий Гасла рсзультат з" сдноарсмснной лодстаноаки а А аь~еьчо х„х„, т„соозастстасино формул )-л ВИВ, В„яалястся доказуемой формулой, т.с.. Способ л,я, .л, — )(А) доказательства ачеаидсн.Формула яыяодится примсиснисм правила простой иодстаионки наслслсяагсльно ко нссм лерсмснным ло порядку. 2. Правило сложного заялючсния Если формулы ЛиЛ„,Л, и А, — +(А, — ь(А,— ь(..,(Ая — ьв).))) доказусмы, то и формула В даказусма. з.
с )-Л,;)-Л,;...,)-ЛА-А - (Лг — (Л, -З(...(Л, — В).,))) Дейсгаггтельно, если па услоаию доказусмы формулы Л, н гч ь(Л вЂ” ь(А — з[..(Л„-»В).))). то по правилу простого закюочсння будет аыяалима формула А, -+(Л, — «(...(Л, — з В)...)). Панса, аналоги ~но рассуждая, заключаем по если яыаодимы А, и Аз -+ (А, — ь (...(А„-ь В)..)). то выводима и формузга А» — з (..
(А, — у В) ..). Продолжая такие рассуждения л раз, лолучнм, что формула В доказуема 3. Правило силлогизма бони локазусмы формулы Л вЂ” ьВ н  — ьС, то доказусма н формула ~-Л-ьВ;~-В- С Л вЂ” ьС,т,с ~ — Л -ь С Хгл» локазагсльстаа зажмем дяс пераыс аксиомы и сделаам я иих соотасгс снующие зямспы К первой аксиоме примсиим слеггуюшую а г'л нодстаиоаку: — )(х — ь (у .+ х)) и ) — ( — ь С) — ь (А -ь (В -ь С)) Чесо З Мвг метичесяаялогик Вторую аксиому преобразуем так де,г — ) (х -э (у е х)) -з ((х -ь у) -+ (х -+ х)) и / — (А -+ (В -ь С)) -ь -ь ((А -+ В) — ь (А -з С)).
По правилу простого закчючени»: )- В -з С ~-(В -ь С) -ь (А е (В -+ С) ) )- А -+ ( — ь С) аналогично Наконец, применяя еще раз правила простого заключения, находим ~-А -ь В; ~-(А -е В) ь (А -ь С) . Итак, формула А-ь С выводима при ~ — А — ьС данных предположениях. 4. Правила когпрпозиции.
Если доказуема формула А -+ В, то доказуема и формула В -+ А, т. е. )- А -ь В )- В -ь А Правило доююмваеюя очень просто с использованием только одной формулы из спгюка аксиом исчисления высказываний, а именно девятой аксиомы (х ь у) ь (» -+ х). Сделаем в ней следуюшую замену переменных; А,е — ) ((х — ау) — ь(у-+х))м~-(А — ьВ)е( — ьА). По правилу простого заключения ~ — А — ь В; ~ — (А ь В) -ь (В -+ А) ~ —  — «А т, е, искодиая формула доказана. Г„зав д Иснигленне енсяазнеанил гог й, Правило снятия двойного отрицания. Всюг доказуема формула А -+ В, то доказуема формула А — ь В, наоборот, ~А — >В езди доказуема А — ь В, то доказуема формула А -ь В, т.
е. и ~А+В ~АьВ )-А-ьВ Вгюпользуемся десятой и одинналцатой аксиомами и проведем в них аналогичные подстановки ~ — ))х — ьх)н~ — А — ьА, — )(х-ех)м — Вь — А-+В;~ — В-+В Тогда по условию и по правилу силлогизма , н ~ — А — ьВ А -ь А; ~- А -ь В )-А-ь В Докаэательства лля пяти привсленных правил могут быть записаны е виде деревьев: Г)-А(хпхз,...,х ) Г(- А(В,, х,,..., х„) Г)- А(Вн Вз,..., В„) Я Г)-~, — В,Г~-А„. Г~ —  — + С, Г) — (В ь С) — ь (А ь (В ь С)) ----- -,Г)-ф, 3 Г~- Л вЂ” ь В) ь А -ь С Г) — А -+ В Г1- А — + С где Ф, = (А е (В -ь С)) — ь ((А ь В)ь (А -ь С)). Честь !. Ыагмчлпже скал линяя гаг 1~- Л вЂ” ь В, 1~ — (Л вЂ” ь В) -е (В -ь А) Г~ — А — УВ,Г-В-+В 21-А-+В,Г~ — А — ьА 5.
или Г(- Л-з В Г)-Л-ов Приемы доказательств, подобные уже приведенным, применяются ллл получении правил вывода из совокупности формул. Пусть à — произвольная конечная совокупность формул, т.с. Г=(А!,Аз,...,А„). Выеодв ю соеокуляосяш формул называется всякая конечна» последовательность формул, любой член которой удовлепюряет следующим условиям. Г, т.е.
формула А,п Г иыводима из Е Есекая ( — В 2. Всякая локвзуемая формула выводима из Г, т. е. или Ло Л„... А„~ — В )- В и- 3. Если С и С ь В выводимы из совокупности формул Г, то В также Г'!-С;Г( — С -+ В выводина из Г, т. е. — формула, аналогичная правилу Г(- В простого заключении. Очевидно, что класс формул, выводимых из Г, совпадает с классам доказуемых формул (сн.розд. 2.22 если Г содержит только доквзуемыс формулы. Если же Г содержит хотя бы одну недоказуемую формулу, то класс формул, выводимых из Г, шире класса доказуемык формул. Из определения выводимой формулы и вывода из совокупности формул следукгг очевидные свойства вьпюда: !.
Всякий начальный отрезок вывода из Г есть вывод изГ. 2. Между двумя соседними членами вывода из Г можно вставить любой аз~вод из Г. 3. Всякий член вывода из Г является формуяой из Г. щз Пива д нсмю нневнскаенваннй Если Г,С Г,то всякий вывод из Г, явияетсн выводом из Г. Для того щобы формула Л была вьщодима из Г, необходимо и дютаточио, чтобы существовал вынод А из Г 1. Правила расширения.
л—, т. е есгш А вывадиыа из Г,то она вьоюдима и из Гьз%, где Г,йг~ — А' Г и И' — некоторые канечныс совокупности формул. Пусть Г, = Гьз И', гогла Г с Г, и вывод из Г есть лы вод из Гы т. е. если 1~ — Л, то и Г,~ — А, чга локазывает данное правило нывода. Г, С~ — А; 1~- С 2. Правила удаве~~ив выводимой гипотезы Это правило локазывается включением в вывод нз Г вывода нз С. Пусть совокупность формул Г С =- з1ВнВ„,В„„А), а Г= згС,.Сз, С,„,С).
Если в первом выеадс нет С, то он яаляещя золько выволом из Г и Г~-А. Если же в ВоВ„...,В„„А присуютвуег С, та вместо С в Внйз..В„,,Л всщвин СнСт,...С„„С Это мозкно слелать в соответствии с определением «ывола, тогда получим вывод толька из Г и !1 — А. 3. Правило удалени» имоликащш. 11 — С -ь А Это правило обратное теореме делукции . . .
Здесь лано Г, С1 — Л Г~ — С вЂ” ь А, т. с, существует вывод из Г ~акого типа Г ЛнА„...,Л оС'-ьА. Перейдем таперь к объединению формул Г, С = Гщ С 'Го~да к предыдущему выводу можно присоединить формулу С. т е. Г,С;.'1,Л„...,хйч С-»А,С. По тогда по правияу ! — С;~ — С~А заключения — т с. Г,С:Л„Л„„,А ч,С вЂ” «АС,Л. Это доказывает исходное правило удалении имлликации лростого рдссмотрим сщ» несколько правил, прн доказательстве каторьах децользую гся свойстна вывода. Чаем Г. Мвюмямчееяая лолэив рассмотрим теперь несколько примеров на выводимость формул.
° Пример П Показать выводнмость формулм А ч В -+ А г, В . Воспользуемся сначала восьмой аксиомой (х — э 2) — э((у — э 2) -+(хи у — э 2)), сделав в ней следугоп2уго лв,я е замену: ) ((х — э 2)-э ((у — э 2) -+ (х ч у -э 2))). уз Получим доказуемую формулу )- (А -Э А л В) -э ((В -э А л В) — э (А и В -+ А л В)) . Аналогичные операции проведем с третьей и четвертой аксиомамн ! я,е А,е — ) (злу-эх)м(-АлВ-э А, ~- ) (злу-ту)м(-Алв-эВ ,г г и примении к двум последним формулам правило контрпозицин: (Ф~(Фз(ФЗ )-л в-+л в где Ф, = Л -э Л лВ, Фз =  — э Л л В, Ф,=(Л вЂ” эЛлВ) (Г — эЛлВ)) — эГЛч — эЛлВ) Итак, формула АчВ-+АлВ доказуема. Она является одной из форм закона двойственности в алгебре логики. Примеру.Докюеть, что Г= (А)(- В -э А — секвенция.
Имеем Г; Г(-А. Возьмем первую аксиому х — э(у -э х) и сделаем в ней подстановку )(х — э(у-+х)), получим доказуемую формулу ьу А -+ (В -э С) . Теперь по правилу простого заключения сразу ) — А;~-А-э(В -+А) получаем конечный результат ЮВ-эА Глвы 2 Исчисление высказываний Пример 3. Доказюь, чго Г = (А — ь В, В~ — А — секвенция. лелятую Воспользуемся теперь второй аксиомой, провеля в ией слелуюнГую г,л.л замену псрсменныя — ) ((х -ь (у — г л)) -ь ((х -ь у) ь (л -ь г))) =— — ~-(С -ь (А -г В)) -з НС вЂ” ь А) — ь (С' -з О)) Егце один раз ~подоя ролепь ~ — С вЂ” з (А-е О);~ — (С вЂ” ь (А — г В)) — ь ИС-е А) — з(С -ь О)) ( — (С вЂ” ь А) — з (С вЂ” г В) )-А Примеру.Дгзквзать следующее правило вывода — .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
