1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 11

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 11)

Ф-+ (~Ф-+ J).Показать, что имеет место равносильность исчислений ИВ2 и ИВ,а именно, справедлива теорема, получающаяся из теоремызаменой ИВ1 на ИВ2. Следует отметить, что аксиомыболее тесно связаны с правилами9и109'ИВ, чем аксиомыl .8. l10'9 и 10иисчисления ИВ1.§ 1.9.Консервативные расширения исчисленийПусть даны два языка:языкаL 1•Исчисление(обозначаемlo< 11),11Lo~L1,и два исчисления:loязыкаLoиназовем консервативным расширениемесли выражение Ф языкаи только тогда, когда Ф доказуемо в11.Loдоказуемо вlo11loтогдаОчевидно, что отношение<непротиворечиво, то11рефлексивно, транзитивно и имеет местоПредложение1.9.1.Еслиlo<11непротиворечиво.Пусть ив<-)-+вита символа-иloОисчисление, полученное из ИВ удалением из алфа­7 и 8.и удалением правилПредложение 1.9.2.

ив<-)< ИВ.§ 1.9.Консервативные расширения исчисленийДо к аз ат ель ст в о. Пусть а:: F -+ F51отображение, определенноеследующим образом:а) если Ф не содержит символаб) если Ф=(Ф-+ Х), то а:(Ф)в) если Ф=·l]i, то а:(Ф)г) если Ф=(ФтХ), где т Е {А,=-+,то а:(Ф)Са:(Ф)==Ф;V а:(Х));·а:(Ф);V},то а:(Ф)=(а:(Ф)та:(Х)).Продолжим а: на последовательности формул и секвенции:а:((Ф1,... ,Фп)) = (а:Ф1, ... ,а:Фп),а:(ГТак как а:(Ф)=Ф)1-= а:(Г) 1- а:(Ф).Ф для формулы Ф, не содержащей импликации, то до­статочно показать, что если секвенцияS доказуема в ИВ, то секвенцияa(S) доказуема в ивС-)_ Если D - доказательство секвенции S в ИВв виде дерева, то индукцией по высоте D будем строить квазивыводD* секвенции a:(S) в ивС-).

Если D - аксиома ИВ, то очевидно, чтоD* = a(D) - аксиома ив С-). ПустьD = D1; ... ; DпsЕсли последний переход вот правил7и8,D.осуществляется по правилам, отличнымто очевидно, чтоD*= D *·1,. D*пa(S)···,будет квазивыводом в ив(-), у которого последний переход осуществ­D. Еслиляется по тому же правилу, что и угдеD1, D2 -доказательства в ИВ секвенций Гсоответственно, то в качествеD*·а:(Ф), а:(Ф), ··а:(Ф)·а:(Ф)D*·!•1-·а:(Ф)·а:(Ф), а:(Ф)а:(Г), ·а:(Ф)Если1-а:(Г), ·а:(Ф) 1- ·а:(Ф)а:(Г)1-Ф, Г1-берем следующее дерево:1-1- Jа:( Ф)D1D=ГI-Ф-+Ф'1- J·а:(Ф)D*2Ф-+Ф52гдеГл.D1 -Исчисление высказываний1.доказательство в ИВ секвенции Г, Фf--Ф, то в качествеD*берем следующее дерево:а(Г),Dja(w) f- ~a(w)У а(Ф)~a(w) f- ~a(w)а(Г)У а(Ф)f- a(w) У ~a(w)f- ~a(w) У а(Ф)оПусть ив<-,v) -исчисление, полученное из ИВ удалением изалфавита символов --+, V и удалением правилПредложение 1.9.3.

ив<-,v)4-8.< ИВ.До к аз ат ель ст в о. Обозначим через р(->) множество формулИВ, не содержащих символа --+. Определим отображение /3: р(->) --+--+ р(->) следующим образом:а) если Ф не содержит символа= (Ф V Х),б) если Фто /З(Ф)V,то /З(Ф)=Ф;= ~(~/З(Ф) /\ ~;з(Х));в) если Ф = ~Ф, то /З(Ф) = ~;з(Ф);г) если ФПродолжим= (Ф /\ Х),/3то /З(Ф)= (/З(Ф) /\ /З(Х)).на последовательности формул и секвенции:/3( (Ф1, ...

, Фп)) =/З(Г f-- Ф)В силу а) определения/3и=(/ЗФ1,... , /ЗФп),/З(Г) f-- /З(Ф).предыдущего предложения достаточнопоказать, что если секвенция S доказуема в исчислении ив<_,), то/З(S) доказуема в ив<-,v)_1Инд кцией по высоте для любого доказательстваDсеквенцииSв ив<_, в виде дерева будем строить квазивывод D* секвенции /З(S)в ив(->,V)_ Если D - аксиома ив<-), то очевидно, ЧТО D* = /З(D) аксиома ив(->,V).

ПустьD = Do; ... ; DпsЕсли последний переход вот правил4-6D.осуществляется по правилам, отличнымИВ, то очевидно, чтоD*= D О•*·. D*п••• '/З(S)будет КВаЗИВЫВОДОМ В ИВ(->,V).§ 1.9. Консервативные расширения исчислений53Прежде чем рассмотреть случаи применения правилДОПУСТИМОСТЬ В ИВ(->,V) СЛедуЮЩИХ правил:)Г, Ф, Г1f-Фб) г, ф f-а------·Г, ··Ф,Г1f-Ф'Гf-J.·Ф'f·Ф f-г, ф4-6,докажемфв)---.Г,·ФДопустимость в ивс-,v) правила а) будем показывать индукциейпо высоте доказательства D в ивс-.v) секвенций Г, Ф f- Ф. Если D аксиома Х f- Х, то квазивыводом в ивс-.v) секвенции ··х f- Х будетследующее дерево:·хf-·х; "Х"Х, ·хf-f-ХЕсли последний переход в деревеD"Х1-3или10,f-3:"Х·является применением правилто доказуемость секвенции Г, ··фf-Ф сразу следует изиндукционного предположения. Если последний переход в деревеявляется применением правил9, 11или12,Dто доказуемость секвенцииГ, ··фf- Ф следует из индукционного предположения и применений11 и 12.Пусть секвенция Г, Ф f- J доказуема в ивс-.v).

Тогда по правилу а)получаем доказуемость Г, ··ф f- J и по правилу 9 получаем доказу~емость в ив(-,v) секвенции Г f- ·Ф. Покажем теперь допустимостьв ив(-->,V) правила в). Из доказуемой в ив(-->,V) секвенции Г, ф f- фи аксиомы ·ф f- ·ф с помощью правил 10-12 получаем секвенциюГ, ·Ф, Ф f- J.

Из допустимости в ивс-.v) правила б) получаем доказу­емость в ив(-->,V) секвенции Г, ·ф f- 'Ф.правилПустьи последний переход вИВ. ТогдаDiDосуществляется по правилубудет квазивыводом секвенции ,В(Г)пустимости правила б) в качествеD*f-4исчисления,В(Ф) и в силу до­можно взять следующее дерево:Dj; ·,В(Ф) /\ ·,В(Ф) f- ·,В(Ф),В(Г), ·,В(Ф) /\ ·,в Ф) f- J,В(Г) f- ·(·,В Ф) /\ ·,В(Ф)).Аналогично рассматривается случай, когда последний переход восуществляется по правилуD5.Пусть теперь- доказательство в ивс-,v), последний переход в котором осуществ­6.

По индукционному предположению существу-ляется по правилу54Гл.Исчисление высказываний!.ют квазивыводы Di, D 2 и D 3 в исчислении ивс-.v) секвенций;Э(Г), ;Э( Ф)1-;Э(Ф); ;Э(Г), ;Э(Х)1-;Э(Ф) и ;Э(Г)1- ~(~;3( Ф) /\~;3(Х)) со-ответственно. В силу допустимости в ивс-.v) правила в) следующеедерево будет квазивыводом в ивс-.v) секвенции ;Э(Г) 1- ;Э(Ф):D*D*;Э(Г), ~;3(Ф) 1- ~;3(Ф) ;Э(Г), ~;3(Ф) 1- ~;3(Х);Э(Г), ~;3(Ф)1-/\~;3(Ф)/:J(Г), ~ц(Ф);Э(Г)~;3(Х)D*3F~1- ;Э(Ф).оДо этого мы рассматривали расширения языков исчислений лишьпутем расширения алf авитов.

Рассмотрим теперь расширениеLGязыка исчисления ИВ -,,v), у которого алфавит и формулы те жесамые, что у ивс-.v), а секвенции определяются так: если Г и е конечные последовательности формул исчисления ивс-.v), то Г 1- еявляется секвенцией языкаLG.Определим теперь исчислениесеквенции вида Р, Г1-Go-е, Р, где РязыкаLG.АксиомамиGoбудутатомарная формула, а Г, е-последовательности атомарных формул. Правилами вывода исчислениябудут следующие:GoI) г 1- е,Ф;Г 1- е, Фг2)1-е, ФА ФS) Г 1- д, Ф, Ф, 0Гl-д,Ф,Ф,0''Ф,Ф,Гl-0б) Г,Ф, Ф,д 1- е,Ф/\Ф,Гl-0'Г, Ф,Ф,д?) Г 1- 0, Ф, Фг 1- е, Ф 'З) Ф,Гl-0г1-е, ~Ф'4 ) Гl-0,ФВ) Ф,Ф,Гl-0~Ф,Гl-0'где Ф, ФФ,Гl-0переменные для формул-1- 0последовательностей формулGo,а Г, е, д-'переменные дляGo.В оставшейся части параграфа формулами и секвенциями, еслине оговорено противное, мы называем формулы и секвенции исчисле­нияGo.Лемма1.9.4.Пусть секвенция Гдовательности Г 1 и011-е доказуема вG0 ,а после­содержат среди своих членов все члены по­следовательностей Г и е соответственно.

Тогда секвенция Г 1доказуема в1- 0 1Go.До к аз ат ель ст в о. Индукцией по длине Ф покажем, что для лю­бых последовательностей формул Г, е из доказуемости вGoсеквенции§ 1. 9. Консервативные расширения исчисленийГf- 0следует доказуемость всеквенций Ф, ГGo55и Гf- 0Утверждение леммы отсюда получим, используя правилаf- 0, Ф.5)-8).Если Ф- атомарная формула, а D - доказательство в Go се­f- 0, то очевидно, что, заменив в D каждую секвенциюГ' f- 0' на Г', Ф f- 0' (на Г' f- Ф, 0'), получим доказательство в Goсеквенции Г, Ф f- 0 (секвенции Г f- Ф, 0). Применяя правила 5), 6),получим доказуемость секвенций Ф, Г f- 0 и Г f- 0, Ф.Пусть Ф = Ф /\ Х и секвенции Х, Г f- 0; Г f- 0, Ф; Г f- 0, Х дока­зуемы в Ga. Из индукционного предположения получаем доказуемостьФ,Х,Г f- 0, а с помощью правила l) получаем доказуемость Г f- 0, Ф.С помощью правила 2) получаем также Ф, Г f- 0.Если Ф = ~Ф и секвенции Ф, Г f- 0; Г f- 0, Ф доказуемы в Go, тодоказуемость в Go секвенций Ф, Г f- 0 и Г f- 0, Ф получаем с помощьюправил 3) и 4).Оквенции ГЛемма1.9.5.а).

Если вG0доказуемы также секвенции Гб). Если вG0Если вЕсливГf- 0,GoФ, тото доказуемаf- 0,f- 0, ~Ф,тодоказуемаf- 0.доказуема секвенциятакже секвенция Гf- 0, Ф /\Ф.f- 0.доказуема секвенция ГGoтакже секвенция Ф, Гг).f- 0, Фидоказуема секвенция Ф /\ Ф, Гтакже секвенция Ф, Ф, Гв).доказуема секвенция Г~Ф, Гf- 0,то доказуемаб).Доказательстваf- 0, Ф.До к аз ат ель ст в о.Докажемутверждениеостальных утверждений проводятся аналогично, и мы их оставляемчитателю в качестве упражнения.Переход в доказательствеоносуществляется5), 6). Если D -побудем называть существенным, еслиDправилам,отличнымдоказательство вобозначим дерево, полученное изDGoотправилперестановкив виде дерева, то черезD*удалением всех секвенций, распо­ложенных ниже секвенции, являющейся заключением при последнемсущественном переходе вD.Индукцией по числу существенных переходов в дереведоказывать следующее утверждение: есликвенции Г1,Ф/\ Ф,Г2D -Dдоказательство вбудемGoсе­D1 секвенцииГ1,Ф,Ф,Г2 f- 0, причем число существенных переходов в D1 меньшеf- 0,то существует доказательствочисла существенных переходов вD.ПустьD'Ф, Ф,Г' f- 0Ф/\Ф, Г'1f- 0' .D*имеет следующий вид:Гл.561.Исчисление высказыванийТогда в качестве требуемогоD 1 можно взять некоторое дерево D1, длякоторогоD'= ( Ф, Ф,Г'DjПустьD*f- 8')*имеет следующий вид:D'Ф !\ Ф, Ф А Ф, Г' f- 8 7Ф !\ Ф, Г' f- 8'Обозначим через по число существенных переходов вционному предположению существует доказательствоФ, Ф, Ф !\ Ф, Г'D.D2По индук­секвенцииf- 8' с числом существенных переходов < по - 1.

Опятьпо индукционному предположению существует доказательство Dз се­квенции Ф, Ф, Ф, Ф, Г'Тогдав качествеГ1, Ф, Ф, Г2f- 8' с числом существенных переходов< по - 2.можно взять такое доказательствоD1f- 8, чтоDiсеквенцииестьDзФ, Ф, Ф, Ф,Г'f- 8'Ф,Ф,Ф,Г'f-8'Ф, Ф, Ф, Г'Ф, Ф, Ф, Г'Ф, Ф,Г'f- 8'f- 8'f- 8'Ясно, что число существенных переходов в D1 меньше по ПустьD*2+2 =D'г;, Ф А Ф, г 2D"'г;' ф !\ l}i' Г2 f- 8'' х 1г; ф !\ l}i' Г2 f- 8'' Х2f- 0', х 1 А Х2По индукционному предположению существуют доказательстваD;'по.имеет следующий вид:секвенций г;, Ф, Ф, Г 2D;иr;, Ф, Ф, Г 2 f- 8', Х2 соответствен­переходов в D;, D;' меньше числа суще­f- 8', Х1 ино, и число существенныхственных переходов в деревьяхD'г;' ф !\l}i'D"Г2 f- 8 1 ' х 1'г;' ф !\l}i'соответственно. Тогда в качестве требуемоготельство секвенции Г1,Ф, Ф,Г2f- 8Г2 f- 8 1 ' Х2D1для которогоберем такое доказа­57Консервативные расширения исчислений§ 1.9.Оставшиеся виды последнего существенного перехода врассмат-Dриваются аналогично.ЛеммаОЕсли секвенции Г1.9.6.в Со, то секвенция Г, Г'f- 8, 8'f- 8, Фи Ф, Г'f- 8'доказуемыдоказуема в Со.До к аз ат ель ст в о.

Характеристики

Список файлов книги