1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 44
Текст из файла (страница 44)
, Xk-1-списокразличных переменных такой, чтоFV(Ф) ~ {х}={хо,... ,Хk-1}-Тогда оператор г:[х] переводит Е-предикаты на 210 в Е-предикаты.До к аз ат ель ст в о. Пусть Q ~ А~ - Е-предикат, t.p - Е-формуласигнатуры ао такая, что Q = t.pQ![z], и Ф° =::; (Ф(Р+)):[z]· Тогда Ф° является Е-формулой сигнатуры ао и для любой интерпретации 'У: {х} -+ АоFимеет место эквивалентность (210, Q)Ф['У] {==с} 210= ф(2lo,Q)[x] = 210 [x] - Е-предикат на 2.(о.wr:[xi(Q)Предложениесистема5.9.4.сигнатурыПустьао,F Ф°['У]-ПоэтомуОограниченная алгебраическая210 -предикатныйсимволРв Е-формулу Ф сигнатуры ао U (Pk) позитивно, х( ф.=ао)хо,входит...
, Xk-1-список различных переменных такой, что FV(Ф) ~ {х}. Тогда операторы г:[х] и г:~Ф<">[х] действуют одинаково на Е-предикатахQ ~ А~ на 210.До к аз ат ел ь ст в о.ПустьQ=t.pQl0 [у] ~ А kЕ-формулы сигнатуры ао. Тогда импликация :3иФ<иЗдлянекоторой~ s Ф приводитк соотношению Г~~Ф<">[х/Q) ~ г:[х](Q). Из доказательства предложения5.9.3следуют равенстваг:[х] (Q) =q,21o [х]'г:~Ф<">[х/Q) = Ф°~ 0 [х],Так как210ограничена, а Ф°,т,'1'-0= ( ф ):пл'Ф°о = (:3иФ<и)):ml·Е-формула, имеем,т,(и)= Q( ::i:::JU'I'_q,_-(::i:::JU ф(и))Рcp(u)[yJ·§ 5.9.Позитивные формулы и монотонные операторы213В силу импликации rр(и) ==;,5 rp справедлива импликацияСледовательно,Ф ==;,Qlo Фо,г:[х](Q) = фQ!O(;r] ~ wi0 [x] = г:~ф(и)[х/Q).Поэтому г:[х](Q) = Г~~Ф<иJ[хJ(Q).оПринцип Е-параметризации.
Пусть ~оограниченная алгеб-раическая система сигнатуры ао, предикатный символ Р( fJ.ао)входит позитивно в Е-формулу Ф сигнатуры а= ао U (Pk). Предпоrp(x, у) = rp(x, уо, ... , Yk-1) -ложим, чтоQ'P ==; (:3xrp)Q! 0 [y]Qa ==;и из а= {а 1~ F :3xrp(x,a)},1~о F rp(a,a)},{аД о к аз ат ель ст в о.Q'P)F Ф['У]-ао Е А такой, что (~о. Qa0 )F Ф['У],существует элементНе уменьшая общности, можно считать чтоЛо-формула.
Действительно,Зхrр(х, у)=Еслиrpo(u,y)==; Зх ~Qt0:3u:3x ~ urp(u)(x, у).urp(u)(x,y),тоQ'Po ==; :3иrpi0 [y] = {а 1~оQ~ ==; {а 1~оF :3urpo(u, а)}= Q'P,F rpo(a,a)}Q~ ~ Q~,, аиа Е А,~ 21 а' следует Qa ~ Qa'· Тогда для любой интерпретациит FV(Ф) --+ Ао такой, что (~о.rp -Е-формула сигнатуры ао,rpo~ Qa, а Е Ао,~Qloа',является Ло-формулой.Пусть Ф ::=; (Ф(Р+));х<р(х,у)[у]· Тогда Ф -Е-формула сигнатуры ао,справедливо FV(Ф) ~ FV(Ф) и для любой интерпретации 'У: FV(Ф)--+--+ Ао имеет местоТакнокакФ~о= Q!0интерпретация~оF Ф['У]ограниченаЗuФ(и)_и ~оиЗаметим,Фчтот FV(Ф) --+ АоF :3uwCи) ['У]-Е-формулаw(и)такова,=сигнатурыао,(Ф(и));х,(и<р(х,у)[у]·что(~о.Q'P)FверЕслиФ['У],тоСледовательно, существует интерпретацияГл.214,у':FV(w)u {и}- Ао5.Теория моделейтакая, ЧТО"( 1r FV(w) = 'У и ~о F w(и)[,у']. Еслиао ==т ,у'(и), то~ОF (Ф(и)):х(и<р(х,у)[у]['У'],(~o,Q~ 0 )гдеQ~ 0 ==т {а 1~оF 3х (; аоср(х, а)}=F ф(и)[,у'],UQa <:::: Qao·а,(0.оа 0Так как ф(и) ~ s Ф, имеем (~о.
Q~ 0 ) р= Ф[,у'], (~о. Q~ 0 ) р= Ф[,у], а поскольку(~, Qa0 )РвходитF Ф[,у].вФпозитивноиQ~0 <;:;; Qa 0 , заключаем, чтоОГлава6ТЕОРИЯ ДОКАЗАТЕЛЬСТВ§ 6.1.ИзученныеранееГенценовская системаисчисленияпредставляютGсобойестественныеформализации правил логики. Однако для более глубокого изучениясамого понятия доказательства более удобными являются другие формыисчислений. В настоящем параграфе мы изучим одноисчисленийG,из такихблизкое к исчислению, предложенному Генценом.Алфавит исчисленияGотличается от алфавита исчисления предикатов гильбертовскоrо типа, изученного в гл.отсутствием знаков4,импликации и равенства.
Понятие формулы исчисленияотличаетсяGот соответствующего понятия формулы ИПf: 1) отсутствием правилобразования формул вида (Ф-+ Ф),несмешанностиных,переменных,имеющих как свободные,мулу. СеквенцииG -t 1 ~ t2котороеивыполнением условия2)означаетотсутствиеперементак и связанные вхождения в форэто выражения вида Гf-е, где Г и еконечные, возможно пустые, последовательности формул исчислениятакие, что для Гf-Gе выполнено условие несмешанности переменных,определяемое для секвенции так же, как и для формул.
Соглашенияо сокращенной записи формул и некоторые обозначения, используемыениже, имеют тот же смысл, что и в гл.4.Определение. Аксиомами исчисленияФ, Ге, Ф, где Фf--Gявляются секвенции видаатомарная формула, Г и е-последовательности(быть может, пустые) атомарных формул.Определение. Правилами вывода исчисления1f-г·ЗгГ.Гwе, Ф А w ·е, Ф; гf-f-f- е, Ф, Фf- 6, Ф V Ф'е,Gбудут следующие:Ф,Ф,Гf-62. Ф /\ Ф, Г f- е'Ф, г4.f-е;w, г f- еФVФ,Гf-6'Гл.216Ф, Г6.Теория доказательствгf- 0Б. Гf-0,~Ф'6·[ФJ~,г f- е? Гf-0,(Ф)f. Г f- 0, :3хФ 'S.Г f- 0, [Ф]~9·Г f- 0, \lхФ'мулы из г и е,·141-1 О0'мулы из г и е,Г,Ф,Ф,Лf-0f- 0, Ф, Фг f- е, Ф 'Правила'12 _ Г,Ф,Ф,Лf-0,Гf-Л,Ф,Ф,0Г:3хФ Г f-где у не входитсвободно в форlO (Ф)f, Г f- 0. \lхФ,Г f- 0'где у не входитсвободно в форll.
Гf-Л,Ф,Ф,е,13е, Фf-~Ф, г f- е'Ф,Ф,Гf-0.Ф,Гf-0.называются основными, а правилатурными. Структурные правила11и1211-14 -струкназываются правилами перестановки или перестановками, а правила13и14 -правилами утончения или утончениями. Понятие доказательства (линейного и в видедерева) определяется так же, как для исчисления предикатов.Отметим ряд особенностей этого исчисления. Во-первых, это большая симметричность правых и левых частей секвенции Гемых заключением или сукцедентом(0)f-е (называи посылкой или антецедентом (Г) соответственно). Во-вторых, каждое основное (в отличие отструктурных) правило под чертой содержит более сложную формулу,получаемую из формул посылки (эту формулу будем называть главнойформулой правила).
Третья особенностьсти-На вхожденияхсеквенций в доказательствоIопределим операциюlвхождение вl(I) = I;чертой, тоD,l(I)вхожденияхJобразом: еслиS(J)свойство подформульно-требует введения новых понятий.тоследующим образом: еслиеслив виде дереваDзаключительноесодержится в переходе Р надесть вхождение секвенции из перехода Р под чертой.
Наформул в деревоJвходит в секвенциюопределим операциюне входит вISследующимнекоторой секвенции, тоJ входит в последовательностьS(J) равно тому же вхождениюно уже в секвенции l(I); для основныхГ и е, то S(J) есть главная формулаl(I);формулы в Г или е (или Л),JDсодержится во вхожденииГ или е (или Л) в секвенцииправил, еслиII -еслиI,топерехода, для структурных правил, еслиJне входит в Г, е или Л,§ 6.1. Генценовская система Gто в обозначениях правил11-14черезzn(I)в деревеI1=имеем S(Ф)для некоторого положительного п имеемвхождение217является предкомЕсли Ф -аJ2,l ...
l(I),J2гдеltG,х-Ф. ЕслиI2.(Здесьповторено п раз.) Если= J2,является потомкомформула исчислениябудем говорить, что терм=то говорим, чторасположено выше вхожденияDобозначается значениедля некоторого положительного п имеем sп(J 1 )JiФ,S(Ф)= /2,zn(I1)то говорим, чтоJi.переменная,t -терм, тосвободен для переменной х в формуле Ф,если Ф не имеет свободных вхождений переменной х или если ни однапеременная термаtне имеет связанных вхождений в Ф.Расширим понятие подформулы, считая обобщенными подформулами формул :3хФ, \lхФ и формулы (Ф)f, где термЗамечаниеи переменнаяv6.1.1.tсвободен для х в Ф.Если Ф есть обобщенная подформула формулы Фимеет связанное вхождение в Ф, то она имеет связанноевхождение и в Ф.Назовем булевой сложностью j3(Ф) формулы Ф число вхожденийсимволов из множестваЗамечание6.1.2.{~, л, v} в Ф.Если Ф является обобщенной подформулой формулы Ф, то j3(Ф)::;; /3(Ф).Справедливо следующее свойство подформульности.Лемма6.1.3.Отношение предок-потомок удовлетворяет следующим условиям: если вхождение секвенции Со находится вышевхождения секвенции С 1 , то для любого вхождения формулы в Сосуществует единственный ее потомок в С 1 ; для любого вхожденияформулы вCiсуществует по крайней мере один его предок в Со.Любой предок является обобщенной подформулой потомка.Справедливость леммы легко устанавливается индукцией.Хотя в определении понятий формулы и секвенциигалосьусловиенесмешанностипеременных,этогонеGОпредполапредполагаетсяв определении доказательства (в виде дерева).
Тем не менее, можнодаже требовать большего. Будем говорить, что доказательство (в видедерева)Dревавыполнено условие несмешанности переменных и для любогоDперехода вобладает свойством чистоты переменных, если для деDпо правилам8или9соответствующая переменная увстречается только в секвенциях, находящихся выше заключительнойсеквенции этого перехода.Лемма6.1.4.Для любой доказуемой вGсеквенции существует доказательство этой секвенции со свойством чистоты переменных.Гл.218Теория доказательств6.До к аз ат ель ст в о. ПустьD -доказательство секвенции С вСкажем, что переменная у исчезает в переходе Р дереваG.если уD,имеет по крайней мере одно свободное вхождение в секвенцию надчертой и не имеет свободных вхождении в секвенцию под чертой в этомпереходе. Заметим, что переменная может исчезать лишь в переходах,соответствующих одному из правилисчезаетправильно,ет вхождения веслиу7-10.исчезаетвСкажем, что переменная унекоторомпереходеииметолько в секвенции, находящиеся выше нижнейDсеквенции этого перехода.
Заметим, что если переменная у исчезаетправильно, то она имеет только свободные вхождения в деревеD.D исчезают правильно, то D имеетЕсли D имеет неправильно исчезающиеЕсли все исчезающие переменные всвойство чистоты переменных.переменные, то найдем переход Р, в котором некоторая переменная уисчезает неправильно; пустьнижней секвенции этогосеквенции исеквенций иВыберем переменнуюz,D' -перехода,поддеревот. е.переходов,соответствующееD,дерево,состоящее из этойнаходящихся вышеотличную от всех переменных ввнее вD, ииз D'D.заменимD поддерево D' на дерево [D']¾, которое получаетсязаменойiI1 на [Ф]¾. Легко проверить, что получившееся дерево D* остается доказательством и это доказательство таково, что переменная z исчезает в D* правильно. Ясно, что за конечноечисло таких преобразований (D на D*) мы получим доказательство,каждого вхождения формулыв котором все исчезновения переменных правильные.Следующая лемма позволит ввести в исчислениеОGполезное допустимое правило (правило утончения).Лемма6.1.5.Пусть Гмула такая, что Ф, ГФ, Гf-- 0и Гf-- 0,f--f--е-доказуемая секвенция и Фе является секвенциейФ доказуемы вD --фортогда секвенцииG.До к аз ат ель ст в о.
Пусть хо,формулы Ф. ПустьG,... , Хп-все свободные переменныедоказательство секвенции Гf--е со свойствомчистоты переменных. Как видно из доказательства леммыпредполагать, что все исчезающие переменные вD6.1.4,можноотличны от хо,...... ,Xn.Докажем лемму индукцией по построению формулы Ф.атомарна, а(D,секвенции Лf--Ф)-Л на вхождения секвенции Л, Фрованных выше предположениях относительнодоказательство секвенции Г, ФперестановкиФ, Гf--12Если Фдерево, полученное заменой каждого вхожденияf--несколько раз,f--Л, то (при сформулиD)дерево(D,Ф) естье.
Применяя структурное правилополучим доказательство секвенциие. Аналогично определяется дерево (Ф,D)(Лf--Л заменяетсяГенценовская система§ 6.1.на ЛG2190; исполь1-- 0, Ф.Пусть Ф = Фо V Ф 1 . По индукции из доказуемости Г 1-- 0 следуетдоказуемость секвенций Фо, Г 1-- 0; Ф 1 , Г 1-- 0; Г 1-- 0, Фо; Г 1-- 0, Фо, Ф 1 ,1--Ф, Л), которое есть доказательство секвенции Гзование правилатогда111--Ф,завершает доказательство секвенции ГквазивыводыФо,ГФо1-- 0; Ф1, Г 1-- 0Г 1-- 0, Фо, Ф1V Ф1, Г 1-- 0' Г 1-- 0, Фо V Ф1показывают доказуемость секвенций ФоV Ф 1 , Г 1-- 0Аналогично проверяется утверждение для Ф = Фои Г/\ Ф11-- 0, Фо V Ф,.и Ф = ~Фо.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
