1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 25
Текст из файла (страница 25)
, Xn - переменные, то через (t)li:.::;'t:n обозначаем результатподстановки вместо х,,Предложение... , Xn4.1.6.сигнатуры I:, Ф -термовПустьt,, ... , tnсоответственно.t,q,s; q,, ... ,qn; s,, ... ,sn -термыформула ИПЕ, удовлетворяющая условию наГл.120Исчисление предикатов4.запись (Ф )~i':.::·:;nn и на запись (Ф )~i':.::·;:;:. Тогда в ИПЕ доказуемыследующие секвенции:а) f- t ~ t,6) t ~ q f- q ~ t,в)t~ q, q ~ sf- t~ s;Г) QJ ~ SJ, ••• , Qп ~ Snf- (t)XI,... ,Xnql,···,Qnд) QI ~ SJ, •.. , Qп ~ Sn, (Ф)Xl,···,XnQI , ••• ,Qn~(t)Xl,... ,Xn;s,, ... ,Snf-(Ф)Xl,•··,Xn.S1 , ••• ,SnДо к аз ат ель ст в о.
а). СеквенцияПусть х, х1, у, z -f- t~tявляется аксиомой.попарно различные переменные. Рассмотрим деревоf-х ~ х; х ~ у,(z~ х)~f- (z ~ xnx~yf-y~xt~qf-q~tТак как начальные секвенции у него- аксиомы, а переходы 4.1.4, то рассматриваемое дерево6). Доказуемость в) получаем анаприменения правил из предложенияявляется квазивыводом секвенциилогично из квазивыводау~x1)t' f- (х ~ х1); 1х ~ у, у ~ z f- х ~ zt ~ q, q ~ s f- t ~ sz,(х ~г). Пусть У1, ... , Уп; z1, ...
, Zn отличные от х 1 , ••• ,хп,не входящиев формулу Ф. Из а), предложения((t);/ );:попарно различные переменные,в термыq1, ... ,qn,s1, ... ,sn,tи4.1.4, в), и из того, что термы (t)t! иравны, получаем, что деревоf- (t)t: ~ (t)t:; YI ~ZJ,YI ~ZJ(t)t: ~ ((t);:);: f- (t)ti' ~ (t);i'f- (t)l) ~ (t)';i'является квазивыводом в ИПЕ. Если п > 1, то в силу предложения4.1.4, и), в ИПЕ доказуема секвенция У1 ~ z1 f- (t)ti'::: :;: : ; (t);i':l;- Применяя к этой секвенции и аксиомеправила а) и6)из предложения4.1.4,получаем секвенциюПроделав несколько таких шагов, получаем доказуемость в ИПЕ секвенции~у 1 r,....,z 1, ···, уn~r-,...,zn f- (t)Xl,···,Xny,, ... ,yn~r-,...,(t)Xl,•••,Xnz1 ,Zn •1 •••§ 4.1.Аксиомы и правила вывода121Из этой секвенции с помощью правила и) из предложения4.1.4получаем секвенцию г).д). Так как справедливо равенство ((Ф)х,.х 2 ····•Хn)У 1,Y2,···,Yn z1У1=(Ф)х,.х2, ...
,хn, тоz1 ,Y2,···,Ynсеквенцияявляется аксиомой. Если п>то из этой аксиомы и аксиомы1,по правилам а) и в) из предложенияYI~z1,У2 ~z ,4.1.4получаем(Ф)х',x2,X3, ... ,XnYI ,У2,УЗ,···,Уn2f-(Ф)Х',X2,X3, ... ,Xn.ZI ,Z2,YЗ,···,YnПроделав несколько таких шагов, получаем доказуемость в ИПЕ секвенцииуl~r-..Jz 1, • • •' уn~r-..Jzn,f-(Ф)х,, ...
,ХnУl,·•·,УпОтсюда в силу правила и) из предложения(Ф)х,, ... ,ХnZl,•••,Zn •следует доказуемость4.1.4В ИПЕ секвенции д).0Следующая теорема является, конечно, следствием упомянутой выше теоремы Гёделя, однако ее легко доказать и непосредственно.Теорема 4.1.7. Если ~ 1 ~ ~. то исчисление ИПЕ является консервативным расширением исчисления ИПЕ'.До к аз ат ель ст в о. Пусть D - дерево доказательства в ИПЕсеквенции С, являющейся также секвенцией ИПЕ'. Пусть у - переменная, не входящая ни в одну формулу из D. Определим отображениеа: Т(~)--+ Т(~1) индукцией по длине термаа) еслиб) еслив) еслиЕсли Ф1)-t Е Т(~):t - переменная, то at = t;t = f(t1, ...
.tn), где f - символ из ~1, то at = f(at1, ... atn);t = f(t1, ... , tn), где f - символ не из ~1, то at = у.атомарная формула сигнатурыформуленатуры2)3)r(at1, ... , atn),если Ф~.то пусть аФ равняется:= r(t1, ... , tn)иr -символ сиг~1;формулеat1~atz,если Фформуле \/у(у ~ у), если Ф= t1 ~ t2;= r(t1, ... , tn),гдеr-символ не из~!-Для любой формулы Ф сигнатуры ~ определим формулу аФ сигнатуры ~1 как результат замены в формуле Ф всех атомарных подформул Ф на аФ. Пусть а D получается изФ 1, ... , Ф nf-Ф на аФ 1, ...
, аФ nf-Dзаменой всех секвенцийаФ. Очевидно, что начальные секвенции aD будут аксиомами ИПЕ'. Легко проверяется, что все переходыГл.122вCJ D4.Исчисление предикатовбудут применениями тех же правил, что и соответствующиепереходы вD.В самом деле, проверка для правилвиальна, а для правил14и15=формулы Ф заметить (учитывая х -=f у), что CJ(Ф)tв свою очередь индукцией по длине термаt2установить равенствоCJ(ti )f21-13и16тринужно сначала индукцией по длине= (CJt1 )~t2 •формул Ф из секвенции С, то дерево(CJФ)~t• для чегоt1 нужно для любого термаCJ DТак как СJФ=Ф для всехбудет доказательством Св ипЕ,_оВ дальнейшем мы свободно будем пользоваться теоремой4.1. 7,чтобы не упоминать исчисление ИПЕ, когда речь идет о доказуемостинекоторой секвенции С.
В частности, мы будем говорить, что секвенция С доказуема в исчислении предикатов или просто доказуема,если С доказуема в некотором ИПЕ.Упражнения1.Пусть сигнатура ~ содержит все пропозициональные переменныеисчисления ИВ в качестве нульместных предикатных символов.Показать, что ИПЕ является консервативным расширением ИВ.(Указание. Воспользоваться теоремой полноты для ИВ и теоремой2.4.1.5.)Показать, что если в одном из правил13-16убрать ограничениена применения этого правила (в частности, для правил14и15снять условие на запись (Ф)f), то в полученном исчислении будетдоказуема не тождественно истинная формула.3.Показать, что если в правилахнаприменения этих правил,ленияJ13и16убрать все ограничениято все теоремы полученного исчисбудут 1-общезначимыми, в частности,Jбудет непротиворечивым.§ 4.2.Эквивалентность формулВсе изучаемые нами свойства алгебраических систем инвариантныотносительно изоморфизма,многие же интересующие нас свойстваформул инвариантны относительно определенного ниже отношения эквивалентности.Зафиксируем на дальнейшее произвольную сигнатуру~-Все формулы и алгебраические системы в этом параграфе имеют сигнатуру~.а доказательства рассматриваются в исчислении ИПЕ.Определение.
Формулы Ф и iiт называются эквивалентнымизначается Ф= Ф),если доказуемы две секвенции Ф/-iiт и Ф1-Ф.(обо§ 4.2.Эквивалентность формулОчевидно, что отношениестве= являетсяэквивалентностью на множеи все доказуемые формулы из F(Щ образуют один классF(~)эквивалентности. В силу теоремылюбой системысвойство1232lдля любых формул Ф4.1.5и любой интерпретации т (FV(Ф)2lF Ф[1]равносильно свойствуЗаметим, что в силу теоремы2lF Ф[1].отношение Ф4.1.
7= Ч',U FV(\J!)) ----,= Ч'Ане зависит от~-сигнатурыОпределение. Формулы Ф и Ч' называются пропозиционально эквивалентными (обозначается ФФ), если Ф----, Ч' и Ч'----, Ф - тавтоsлогии.Из предложенияПредложениеФ и\J!и правила4.1.24.2.1.8получаемПропозиционально эквивалентные формулыэквивалентны.Предложениесвободно в\J!.4.2.2.DПусть Ф, Ч'-формулы и х не входитТогда имеют место следующие эквивалентности:= \lх~Ф;в) :3хФ А Ч' = :3х(Ф А Ф);д) :3хФ V Ч' = :3х(Ф V Ф);ж) \lхФ = Vy[Ф]t;= :3х~Ф;г) \lхФ А Ч' = \lх(Ф А Ф);е) \lхФ V Ч' = \lх(Ф V Ф);з) :3хФ = :Jy[Ф]tб) ~vхФа) ~:3хФДо к аз ат ель ст в о.
Приведем квазивыводы для эквивалентностейа), в), д) и ж), оставляя проверку остальных читателю.~фа)f-\lх~Ф~фf-f- ~vх~Фf- ~vх~Ф\lх~Ф f- ~:JхФ'ФЧ', ФЧ', Фf-f-f-f-Ч'ф:3хФ~:3хФf-f-~Ф\lх~Ф.ФА Ч':3х(Ф А Ф)\J!, :JхФ f- :Jx( Ф:3хФf-~:JхФ:3хФв)f-фФ~ФА Ф)----, :Jx (ФА Ч'):3хФ----, (Ф----, :3х(Ф А Ф)):3хФ А Ч'f-Ч'____,:3хФ А Ч'f-:3х( Ф А Ф):3хФ А Ч'f-:3х(Ф А Ф):3хФ:3хФ А Ч'f-Ч'Гл.1244.Исчисление предикатовФA iJ!f---ФФ А1J! f---ЭхФФ АФ А1J! f---3хФ АЭх( ФАiJ!) f---~1J! f--- 1J!1J!ЭхФ А1J!Фf---ФViJ!ФЭхФV 1J! f---ЭхФf---Эх(ФV iJ!)ЭхФV 1J!ЭхФf--- Эх( Ф V iJJ)V 1J! f--- Эх(Ф V iJJ)1J! f---Эх(ФV iJ!)Фf---ФФФViJ!f---ФViJ!f---ЭхФФf---~ФViJ!iJ!f---~ФViJ!Ф VЭх(Фж)ili F :3хФ V iliV iJJ) f--- ЭхФ V w·[Ф]l f--- [Ф]l\iхФ\iхФf---f--- [Ф]tVy[Ф]t.Заметим, что [[Ф]l]~=Ф.
Это равенство следует из условий на запись [Ф]l.[[Ф]l]~Vy[Ф]tVy[Ф]tПредложениеи1.5,если Ф,4.2.3.wиf--- Фf--- ФDf--- \iхФ.Имеют место все эквивалентности из§ 1.4Х считать формулами сигнатуры~-Д о к аз ат ель ст в о очевидно, так как при замене пропозициональных переменных на tормулы ИП:Е доказательства в ИВ перейдут вдоказательства в ИП .DТеорема4.2.4 (о замене для ИП:Е). Если формула Ф получается1J! заменой некоторого вхождения подформулы iJJ' наформулу Ф' и Ф' = w', то Ф = iJ!.из формулыДо к аз ат ел ь ст в о проводим индукцией по длинетоутверждениетривиально.Если1J! =~w1илиw.1J! =Если Ф'1J!1тФ2,= 1J!,где§ 4.2.
Эквивалентность формулт Е { /\, V,--+},125то доказательство индукционного шага не отличаетсяот соответствующих случаев теоремы о замене для ИВ(§ 1.4).Такимобразом, для завершения доказательства в силу индукционного предположения осталось рассмотреть случаи, когда::Jx\J.I'.По условию секвенции Ф' f-\J.Iимеет вид\ix\J.1 1 илиIJ.I' и IJ.I' f- Ф' доказуемы.
В силусимметричности Ф' и IJ.I' достаточно доказать секвенции \ix\J!' f- \iхФ' и::!x\J.I' f-::!хФ'. Приведем их квазивыводы:IJ.I' f- Ф'IJ.I' f- Ф'\ix\J!' f- Ф'\ix\J!' f- \iхФ' '\J.1 1 f- ::!хФ'::Jx\J.I' f- ::!хФ' ·оВ определении истинности формул на системах связанные вхождения переменных играют совершенно другую роль, чем свободные.В частности, проверка истинности формул \iхФ и Vy[Ф]l одна и та же.В оставшейся части этого параграфа будет показано, что замена связанных переменных преобразует формулу в эквивалентную ей, еслипри этом новое вхождение переменной связывается тем же вхождениемквантора и никакое свободное вхождение переменной не становитсяпри такой замене связанным. Перейдем к точной формулировке такогопреобразования.Определение. Говорим, что формула Ф получается из формулы\J.I\J.I заменойнекоторого вхождения подформулы Qx\J.11 на формулу Qy[\J.I 1]l (здесьQ Е {V, :3} и выполняются условия на запись [1J.11]l).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
