Новиков Ф.А. Дискретная математика для программистов (860615), страница 30
Текст из файла (страница 30)
Аксиомы — три конкретныеформулы:Ai: (а -> (6а));А2 : ((а - (Ь -> с)) - ((а - Ь) -> (а - с)));((-.Ь - - - а ) -((-.б -а ) - > Ь)).Правила вывода:1. Правило подстановки: если формула В является частным случаем формулы 1то В непосредственно выводима из А.2. Правило Modus ponens: если набор формул Л, В, С является частным случаем набора формул а, (а —» Ь), Ь, то формула С является непосредственновыводимой из формул А и В.ЗАМЕЧАНИЕЗдесь а, (а —> b), b — это три конкретные формулы, построенные с помощью переменныха, b и связки —>.4.3.5. Производные правила выводаИсчисление высказываний L — это достаточно богатая формальная теория, в которой выводимы многие важные теоремы.ЗАМЕЧАНИЕВыводимость формул в теории L доказывается путём предъявления конкретного вывода, то есть последовательности формул, удовлетворяющих определению, данному вразделе 4.2.2.
Для удобства чтения формулы последовательности вывода выписываются друг под другом в столбик, слева указываются их номера в последовательности, асправа указывается, на каком основании формула включена в вывод (то есть является лиона гипотезой, или получена из схемы аксиом указанной подстановкой, или получена изпредшествующих формул по указанному правилу вывода и т.
д.).154Глава 4. Логические исчисленияТЕОРЕМА 1b£ДОКАЗАТЕЛЬСТВО1. (Л —> ((Л2.3.4.5.Л -> Л.ВЫВОД:А)А))Ац { А - Л / В } .((Л - ((Л —• Л) —• Л)) - ((Л - (Л((Л —• (Л —> Л)) —• (Л —> Л))Л —> (Л —• Л)Л -> ЛТЕОРЕМА 2(Л-Л)))А2;{А^А/В,А/С}.M P ; 1, 2 .Лх; Л/В.M P ; 4, 3.•Л Ь ^ В —• Л .ДОКАЗАТЕЛЬСТВОВЫВОД:1. Лгипотеза.2. Л —> (В —• Л)Ль3. В - ЛMP; 1,2.•Всякую доказанную выводимость можно использовать как новое (производное)правило вывода.
Например, последняя доказанная выводимость называется правилом введения импликации:4.3.6. ДедукцияВ теории £ импликация очень тесно связана с выводимостью.ТЕОРЕМА(дедукции) Г, ЛВ тогда и только тогда, когда Г 1-£ Л —> В.ДОКАЗАТЕЛЬСТВО[ Необходимость ] Пусть Е\,..., Еп — вывод В из Г, Л. Еп = В. Индукцией по г(1 ^ г ^ п) покажем, что Г I-J: Л —> Ei. Тем самым теорема будет доказана. База:г = 1. Возможны три случая.1.
Пусть Ei — аксиома. Тогда рассмотрим вывод Ei, Е\ —» (Л —• Е\), А —> Е\.ИмеемЛ —> Bi.2. Пусть Ei е Г. Тогда рассмотрим вывод Ei, Е\ГЬ£A^Ei.(АЕ\), АЕ\. Имеем3. Пусть Ei — А. Тогда по первой теореме предыдущего подраздела Ь^ Е\а значит, \-ц АЕ\.Е\,1554.3. Исчисление высказыванийВ любом случае ГА —> Е\. Таким образом, база индукции доказана. Пустьтеперь Г \-ц А —* Ei для всех i < к. Рассмотрим Ек. Возможны четыре случая:либо Ек — аксиома, либо Ек € Г, либо Ек = А, либо формула Ек получена поправилу Modus ponens из формул Ei и Ej, причём i,j < к и Ej = Ei —> Ек. Дляпервых трёх случаев имеем Г Ь^ А —• Ек аналогичным образом.
Для четвёртогослучая по индукционному предположению имеется вывод Г l-£ А —> Ei и выводГА —> (Ei —> Ек). Объединим эти выводы и достроим следующий вывод:П.(А -(EIЕК)) ^ ( ( A - ^ E I ) ^ ( A ^ E K ) )п+1.п + 2.(Л —> Ei) —> (Л —> Ек)А ^ ЕкА2; {ЕГ/В,£FC/C}.MP; j, п.MP; г, п + 1 .Таким образом, Г 1-£, А —»• Ек для любого /г, в частности, для /с = п. Но Еп = В,то есть Г hx: А —» В.[ Достаточность ] Имеем вывод Г Ь^ А —> В, состоящий из п формул. Достроимего следующим образом:п.п + 1.п + 2.ААВВ.гипотеза.MP; п + 1, п.Таким образом, имеем Г, А\-ц В.•ЗАМЕЧАНИЕСхема аксиом Аз теории L не использовалась в доказательстве, поэтому теорема дедукцииимеет место не только для теориино и для любых теорий, в которых выполненыаксиомы А\ и Л2 и действует правило отделения.СЛЕДСТВИЕ 1ДОКАЗАТЕЛЬСТВОСЛЕДСТВИЕ2ДОКАЗАТЕЛЬСТВО2.3.4.5.6.7.А ВВСЛВСЛВ,ВА-> В , ВА\~л В тогда и только тогда, когда I Л —> В.Г: =•0.А —> В,ВС he А -> С.Вывод:гипотеза,гипотеза,гипотеза.M P ; 3, 1.С,А\~л СА^СMP; 4, 2.1-5.по теореме дедукции.•156Глава 4.
Логические исчисленияЗАМЕЧАНИЕЭто производное правило называется правилом транзитивности.СЛЕДСТВИЕ 3Л -> ( ВДОКАЗАТЕЛЬСТВО1.2.3.4.5.6.7.ААВВСАЛ—С), В h£А ->С.ВЫВОД:гипотеза,гипотеза.MP; 2, 1.Сгипотеза.MP; 4, 3.1-5.(В —> С), В, А 1-£ С(В —• С), В Ь,с А —> С по теореме дедукции.(5-С)•ЗАМЕЧАНИЕЭто производное правило называется правилом сечения.4.3.7. Некоторые теоремы исчисления высказыванийМножество теорем теории £ бесконечно.
Здесь приведены некоторые теоремы,которые используются в дальнейших построениях.ЗАМЕЧАНИЕКаждая доказанная теорема (то есть формула теории, для которой построен вывод) можетиспользоваться в дальнейших выводах на правах аксиомы.ТЕОРЕМАа)В теории £ выводимы следующие теоремы:— Л —» Л.Б ) HE Л — -1-1Ав) he - А —» (А —• В).г) \-L (-пВ - - А ) —• ( А —• В).д)(А -> В)(-.В - -А),e j Ь,с, Л —• ( - В - - ( Л - В)).ас;(А —> В) —> ((-Л —• В) —> В).1574.3. Исчисление высказыванийДОКАЗАТЕЛЬСТВО[ в ; h e —Л —• А ]1.2.3.(-Л —Л) -> ((-Л-Л —> ->Л(-пЛ —Л) Л4.5.—Л——I «А -» Л-.Л)Л))А3; {Л/В, -Л/Л}.первая теорема 4.3.5; {-Л/Л}.Сл. 3;{-Л -> —Л/Л,^Л -/1/П. Л/Г'}.Л1; {-i-Л/Л, -Л/В}.Сл.
2; {—Л/Л, -Л -> —Л/В, Л/С}.[б)he Л ^ — Л ]1.2.3.4.5.( — Л - -Л) ->.-> ( ( — л —> Л) —• —Л)— Л -> -Л( — Л Л) — ЛЛ->(-.-.-.Л^Л)Л —» —ЛЛз; {—л/В}.а; {-Л/Л}.MP; 2,1.Л 1; {—Л/В}.Сл. 2; {—-^Л/В, Л/Л, —Л/С}.1.2.3.4.5.6.7.8.9.10.11.12.-пЛЛЛ^(-В^Л)-Л(-В-Л)->В —> Л-iB -> -Л(-В -> -Л) -> ((-В Л) - В)(-В -> Л) ВВ-Л, Л В-Л 1-£ Л —» Вhe —>Л —• (Л —• В)гипотеза.гипотеза.Л1; {-iB/B}.Л1;{-пЛ/Л,-В/В}.MP; 2, 3.MP; 1, 4.Л3.MP; 6, 7.MP; 5, 8.1-9.теорема дедукции.теорема дедукции.[ г ) Ы (->В —> -Л) —• (А —• J3) ]1.2.3.4.5.6.7.-1В —> ->ЛЛ(-В -Л) ((-В —• Л) —> В)Л^(-В^Л)(-В^Л)^ВЛ ВВ8.->В -+->A,A\-L9.10.В-1В —> ->Л 1-£ Л —> ВI £ (->В —• -Л) —> (Л —> В)гипотеза.гипотеза.л3.Л1; {-iB/B}.MP; 1,3.Сл.
2; {->В -» Л/В, В/С}.MP; 2, 6.1-7.теорема дедукции.теорема дедукции.158[ д)1.2.3.4.5.6.7.8.9.Глава 4. Логические исчисления(А -> В) -> (-.В - -iA) ]А —• Б— А —> А— А -> ВБ —» — Б—А - — Б(—Л - — Б ) — ( - Б — -А)- Б - -ЛА —• В Ь,с - Б —» -пЛ(Л —> Б) —> ( - Б —• ->А)гипотеза.а.Сл. 2; { Л / 5 , — Л / Л , В/С}.б; {В/А}.Сл. 2; {—Л/Л, — Б / С } .г; { - Л / Б , - Б / Л } .MP; 5, 6.1-7.теорема дедукции.[ejbc А->(-.В->-.(А-»Я))]1.2.3.4.5.6.7.8.АА —> ББА, А —> Б Ь,с БА Ьх (А —> Б) —> БА((А —» Б) —> Б)he ( ( А В ) - > £ ) - >->- - ( А -> Б))b £ А - ( - Б - - ( А - Б))гипотеза.гипотеза.MP; 1, 2.1-3.теорема дедукции.теорема дедукции.д;{А-+В/А}.Сл. 2; {((Л —>£)—• В)/В;( - Б - - ( А - Б))/С}.[acjhc (А —> £?) —> ((-А —> В) — Б) ]1.2.3.4.5.6.7.8.9.10.11.12.А —• Б- Л —> Б(А — Б) — ( - Б-А)- Б - -A( - А —• В) —> ( - Б - —А)- Б — —A( - Б - —А) - ( ( - Б - - А ) - Б)( - Б -» - А ) —• ББА —• Б, - А —> Б 1-£ БА —• Б l-£ ( - А —> Б) —> ВI—xi.
(Л —> Б) —• ((-Л —• Б) —• Б)гипотеза.гипотеза.а.MP; 1, 3.д; {-А/Л}.MP; 2, 5.А 3 ; {-А/А}.MP; 6, 7.MP; 4, 8.1-9.теорема дедукции.теорема дедукции.•1594.3. Исчисление высказываний4.3.8. Множество теорем исчисления высказыванийПусть формула А содержит переменные ai,...,an,и пусть задана некотораяинтерпретация / формулы А, то есть переменным а\,...,апприписаны истинностные значения. Обозначимд , Def \а,г,11е с л и ai=Т,если щ = F;, Def j А,-1lе с л и 1(A)^'если=Т,ПА) = Fв дайной интерпретации.ЛЕММАA'i,...,A'nДОКАЗАТЕЛЬСТВО\~л А'.Индукция по структуре формулы А.[Переменная] Пусть А = а. Тогда aа и ->а-*а.[Отрицание] Пусть А = - Б и I — произвольная интерпретация формулы А.Возможны два случая: 1(B) — Т или 1(B) = F. Пусть 1(B) = Т.
Тогда 1(A) = Fи А' = - А = -1-1 В. По индукционному предположению А'х,..., А'п 1-£ В. Но|-£ В —> -1-1В по теореме 4.3.7, б, следовательно, А\,...,А'п— Б = А'.Пусть теперь 1(B) — F. Тогда 1(A) = Т и А' — А — ->В. По индукционномупредположению А[,..., А'п->В = А'.[Импликация] Пусть А = (В —> С) и / — произвольная интерпретация формулыА. По индукционному предположению А\,...,А'пВ' и А\,...,А'пС'.Возможны три случая: 1(B) = F или 1(B) — Т и 1(C) = Т или же 1(B) = Т и1(C) = F.Пусть 1(B) = F. Тогда независимо от значения 1(C) имеем: 1(A) = Т и В' == - Б , А' = А. Но А\,...,А'п- Б , Ь £ - Б — ( Б — С) по теореме 4.3.7, в,следовательно, А\,..., А'пБ —> С = А!.Пусть 1(B) = Т и 1(C) = Т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
