1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 6
Текст из файла (страница 6)
Ясно, что дерево может иметьмного начальных секвенций, но заключительная секвенция-толькоодна. Часть дерева, состоящая из секвенций, расположенных непосредственно над некоторой чертой, под той же чертой, и самой черты,называется переходом.1)При написании конкретных деревьев знак ; часто будет опускаться.§ 1.3.Определение. ДеревоDназовем доказательством в ИВ в видедерева, если все его начальные секвенциидыприменения правил вывода-ной секвенцией доказательствадоказательствомПустьh-S25Система аксиом и правил выводааксиомы ИВ, а перехо-Если1-12.Sявляется заключительв ИВ в виде дерева, тоDD называетсяS в ИВ.в виде дерева или деревом выводафункция, определенная на секвенциях (точнее: на вхождениях секвенций) дереваи принимающая в качестве значенийDнатуральные числа, со следующими свойствами:1).
h( S) =2). ЕслиО, еслиSявляется заключительной секвенцией дереваD.So; ... ;Snsпереход в дереве-D,= ... = h(Sп) = h(S) + 1.h(So)Очевидно, что условияЧислоh(S)то1), 2)определяют функциюназовем высотой (вхождения) секвенцииМаксимальную высоту секвенций, входящих вдереваD,h однозначно.Sв деревеD.назовем высотойD.Предложение1.3.1СеквенцияSявляется теоремой ИВсуществует доказательство секвенцииДо к аз ат ель ст в оквенцииSS -S.Пустьв виде дерева.Sбудет доказательством сеD1, ... , Dn-1 Еелилинейное доS1, ...
, Bn-1, S -аксиома, тов виде дерева. Пусть" S 1, ... , S n-1ции{::::::}в ИВ в виде дерева.проведем индукцией по длине п линей(=*)ного доказательства секвенцииказательство в ИВ. ЕслиSSi1 ; ...S;доказательства секвен-S;k:;::: . ... , Zk., 1 "'z,,<п,-применение некоторого правила ИВ, то деревоDi1; ... ; Diksбудет доказательством секвенции({==)ПустьD -Sв виде дерева.доказательство секвенцииSв виде дерева.
Построим линейные доказательства для всех секвенцийПостроение будемS'в деревеD.вести обратнойиндукцией поНачальные секвенции в деревеDS'дереваD.высоте секвенциибудут линейнымиS1, ... , ВтL1, ... , Lm, то+1доказательствами. Если для всех секвенцийвысотыуже построены линейные доказательстваочевидно, чтоkпоследовательностьL1, ... ,Lm,S'будет линейным доказательством секвенцииS'высотыk.оГл.26Опр1.Исчисление высказыванийСхема секвенций Н называется доказуемой в ИВ, если ее добавление к ИВ в качестве схемы аксиом не расширяет множество доказуемых секвенций.
Ясно, что это эквивалентно тому, что все частныеслучаи схемы Н доказуемы в ИВ.ПримерСледующее дерево показывает доказуемость схемы1.3.2.Ф, '11 f- Ф Л '11: 1)ф f-фФ,Опр'11 f-Ф-правилоФ,'11f- Ф Л12'11,Фf-ФФ,wf-w-правило12-правило11-'11правило1.Правило вывода называется допустимым в ИВ, если добавлениеего к исчислению ИВ не расширяет множество доказуемых секвенций.В частности, правила1-12ИВ допустимы в ИВ.Конечная последовательность секвенцийнейным квазивыводом секвенцииSnSo, ...
, Snназывается лив ИВ, если каждая входящаяв нее секвенция является доказуемой в ИВ или получается из предыдущих по допустимому в ИВ правилу вывода. Деревоквазивыводом секвенциисеквенцияDSDназываетсяв ИВ в виде дерева, если всякая начальнаядоказуема в ИВ, заключительной секвенцией являетсяS,а переходы представляют собой применения допустимых в ИВ правилвывода.Очевидно, что всякая секвенция, для которой существует линейныйквазивывод или квазивывод в виде дерева, является доказуемой.В дальнейшем под доказательством (квазивыводом) в исчисленииИВ мы будем понимать доказательство (квазивывод) в виде дерева.Это мы делаем для более наглядного представления доказательства,а также потому, что поиск доказательства данной секвенции в видедерева существенно проще, чем поиск ее линейного доказательства.Ясно, что если в правиле ИВ переставить секвенции над чертой,то полученное правило будет допустимым в ИВ.
Так переделанныеправила мы не будем различать с исходными правилами.Для б Е {О, 1} через Ф" будем обозначать формулу Ф, если би формулу ~Ф, если бПредложение=1,= О.1.3.3(основные допустимые правила ИВ). Следующие правила являются допустимыми в ИВ:) '111, ... ,Фпf-ФX1, ... ,Xm f- Фа------,1)Вместо слов «применение правила k,> будем писать короче - «правило k•.§ 1.3.бг))Гf- \J!; Г, \J! f---Г, ФГf-Хf-27Система аксиом и правил выводаХв'Г1,Ф,\J!,Г2f-Х)Г1, Ф Л\J!, Г2 f- Х•Г Ф" f- \J! 6Jд) Г, ф(;-с:} f- ф"(i-б), где с, б Е {О, 1}.Г f- ·Ф'До к аз ат ель ст в о. Для установления допустимости правила вывода достаточно построить дерево секвенций, у которого переходыбудут применениями правил вывода ИВ, а начальными секвенциямибудут начальные секвенции данного правила и также, возможно, некоторые доказуемые секвенции.ДеревоГ, Ф, Фf- \J!f- Ф-+ \J!Г, ФГ, ФГ, Фf-Фf- \J!показывает допустимость правилаа') Г,Ф,Ф f- \J!Г, Ф f- \J! .Так как любую перестановку формул в последовательности можноосуществить, переставляя соседние формулы, то допустимость правила а) следует из допустимости правила а') с помощью правил11, 12.Покажем еще допустимость правил г) и д), оставляя правила б)и в) читателю в качестве упражнения.г).
Воспользуемся доказуемостью схемы Г, ··Ф, ·фf-J,установитькоторую предлагаем читателю в качестве упражнения:Г, Фf-Jf- J"Ф, Ф f- JГ, Ф, "ФГ,Г, "Ф, ·ФГ,"Фf-Ф-+JГ, "Фгf- JГ,"Фf-Фf-f-J·фДля доказательства допустимости правила д) мы воспользуемсяустановленной выше допустимостью правил а) и г), т.
е. построимсоответствующее дерево, у которого некоторые переходы будут применениями правила а) или г):Г, Ф"f-wбГ, \Jf(l-б), Ф"f-w(l-б) f--- w(l-б)\Jfб Г, ф"(l-б}, Ф"Г, ф"(l-б)' Ф"г, ф"(l-б}f-f-\Jf(l-б)f- Jф(l-с:}.о28Гл.Пример1.3.4.1.Исчисление высказыванийДокажем секвенциюf- Qo V ·Qo:·Qo f- ·Qo·Qo f- Qo V ·Qo ·(Qo V ·Qo) f- '(Qo V ·Qo)·(Qo V ·Qo), ·Qo f- J·(Qo V ·Qo) f- Qo·(Qo V ·Qo) f- Qo V ·Qo ·(Qo V ·Qo) f- ·(Qo V ·Qo)'(Qo V ·Qo) f- Jf--- Qo V ·QoЗамечание1.3.5.Заметим, что приведенное выше дерево не является доказательством в ИВ, так как второй переход не является применением ни одного из правил.
Однако ясно, что, дополнив это деревоприменениями правил11и12,можно получить доказательство. Вместонескольких применений правил11и12можно применять допустимоеправило а). В дальнейшем без оговорок будем пользоваться допустимыми правилами1* -1 О*,которые получаются из основных правил1-1 Озаменой вхождений Г над чертой на Г 1, .•. , Г п, а Г под чертой на Г п+ 1и добавлением условия {Г 1,будет таким:Г1, фf-... , Г п}~ {Г n+ 1}. Например, правило б*w; Г2, Х f- w; Гз f- ф V ХЯсно, что правило б* получается из правила6с Г= Г4 добавлениемследующих применений правила а):Упражнения1.Установить доказуемость в ИВ следующих схем:а) Ф"Ф;f-б) "Фв) Ф А2.f-Ф;W f--- W А Ф;г) ФV W f--- W V Ф;д)f-·J;е)J f-Ф для любого Ф.Доказать допустимость в ИВ следующих правил:е)Гf-Ф А ·фГ f- JГ f- JГ f- Ф; ж) Г f- Ф ; з) Г, ·Ф f- J§ 1.4. Эквивалентность формулЭквивалентность формул§ 1.4.Обозначим черезмножество всех формул ИВ,Foвсех пропозициональных переменных ИВ.
Пустьжение множестваVв29Fo.V - множествоso: V ---+ Fo - отобраДля формулы Ф ИВ через s(Ф) обозначим результат подстановки формулывместо каждой пропозициональнойso(P)переменной Риз формулы Ф. Ясно, что так определенное отображениеs: Fo ---+ Fo1)удовлетворяет следующим условиям:s(Фт\J!)2) s('Ф)= s(\J!)тs(\J!),где т Е {А, V,---+ };= ~s(Ф).Из этих условий индукцией по длине формулы Ф вытекает, чтодля любой формулы Ф ИВ словотакое отображение будемs( Ф)называтьбудет формулой ИВ. Всякоеподстановкой.Длярезультатаподстановки s(Ф) введем обозначение s(Ф) = (Ф):(P~(~.s(Pn)' котороесогласуется с обозначением ( Ф )~, введенным в § 1.2.Распространим отображение s на секвенции:3) s(Ф1, ... ,Фп f- \J!)= s(Ф1), ...
,s(Фп) f-s(\J!).По индукции можно определить продолжение s на деревья:4) ( D1; ... ;Dk) = s(D1); ... ;s(Dk)8Ss(S).Теорема1.4.1(о подстановке). Пустьотображение множестваТогда секвенцияs(S)вVFo, S -s: V---+ Fo -произвольноедоказуемая в ИВ секвенция.доказуема в ИВ.До к аз ат ель ст в о. Индукцией по высоте дерева будем доказывать, что еслиD - доказательство секвенции S в ИВ в виде дерева,s(D) - доказательство секвенции s(S) в ИВ. Если S - аксиома, тоs(S) также будет аксиомой.
Для доказательства индукционного шагадостаточно показать, что если D1 - применение одного из правил ИВ,то s(D 1 ) будет применением того же правила. Но это очевидно в силусвойств 1)-4). Например, еслиФо, Ф f- \J!; Фо, Х f- \J!; Фо f- Ф V ХФо f- \J!- применение правила 6, тотоs(Фо), s(Ф) f-s(\J!);s(Фо),s(X) f- s(\J!);s(\J!)s(Фо) f- s(Ф) Vs(X)s(Фо) f--также применение правила6.оТеорема о подстановке, иными словами, утверждает, что если в доказуемой секвенции вместо пропозициональных переменных подста-Гл.30Исчисление высказываний1.вить произвольные формулы, то полученная секвенция будет доказуемой.Определение. Две формулы Фи= w),значаем Фw назовем эквивалентнымиесли в ИВ доказуемы две секвенции ФОтметим, что символ= не1-(обоw и w1- Ф.является символом языка исчислениявысказываний.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
