1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 48
Текст из файла (страница 48)
, tn) и t # to,t = to, то s(t) = хо.Замечаниео6.4.3.и переменную хо. Определим теперь преобразованиеб) еслиgОтоg), то s(t)= t;s(t) = f(s(t1), ... , s(tn));не имеет вхождений термаto,тоs(t) = t.Следующая лемма показывает взаимоотношения преобразованияsс подстановкой.Лемма6.4.6.Если х#хо иg rf. Fx(t),то для любого термаt'имеет место равенствоs((t)f,)До к аз ат ель ст в о.по построению терма= (s(t));(t')'Доказывать это равенство будем индукциейt. Если х не входит в t, то х не входит и в s(t),поэтому s((t)f,) = s(t) = (s(t));(t')' Пусть х входит в t, тогда t # to,так как если t = to = g(t1, ...
, tk), то g Е Fx(t). Если t = х, тоs((x)f,) = s(t') = (x);(t') = (s(x));(t')' Если t = h(t1, ... , tn), то (t)f, == h((t1)f,, ... , (tп)f,) и s((t)f,) = s(h((t1)f,, ... , (tп)f,)) = h(s((t1)f,), ..... . , s((tп)f, )), так как h Е Fx(t), g rf. Fx(t) и, следовательно,235Теорема Эрбрана§ 6.4.h((t1 )'t,, ... , (tп)f,) -/= to. Из индукционного предположения получаемh(s((t1)f,, ...
, s((tп)f, )) = h((s(t1)):(t')' ... , s(tn)):(t')) = (s(t)):(t')·ОЗамечаниеВ условиях леммы выполняется6.4.7.ветствии с замечаниемs(t) = tв соот6.4.5.Преобразование термов s можно распространить естественным образом и на формулы, секвенции и деревья секвенций, полагая, например, для формула) s(Ф) =P(s(t1), ... ,s(tn))для атомарной формулы Ф =P(t1, ...... .tn);б) s(Ф)= ~s(W)в) s(Ф)= s(Фо)тs(Ф1)г) s(Ф)= Qxs(W)= ~i:i,;для Фдля Фдля Ф== ФотФ1,ЕQxW, Qт Е {V, А};{V, :3}.Следствием предыдущей леммы будетПредложениелюбого термаtПусть переменная хо не имеет связанных6.4.8.вхождений в Ф; х-/=хо -такая переменная, чтоформулы Ф. Тогда для любого термаg (t Fx(t)t',длясвободногодля х в Ф, имеет место равенствоs((Ф)f,)=(s(Ф)):(t')(это соотношение включает в себя и утверждение, чтосвободенs(t')для х в s(Ф)).ООчевидно, справедливо следующееПредложение6.4.9.Пусть переменная хо не имеет связанныхвхождений в Ф; х1, ... , Хп -g (t Fx, (t), iбых термов=такие переменные, отличные от хо, что1, ...
, п, для любого терма t формулы Ф. Тогда для лю-t~, ... , t~,свободных для х1, . .. , Хп в Ф соответственно,имеет место равенствооУстановим следующее важное свойство преобразованияs,действующего на доказательствах.ПредложениеG,6.4.10.ЕслиD -доказательство в исчислениипеременная хо не встречается вDвхождений в заключительную секвенциюдоказательством вf- s8,sФ-gто деревоне имеет связанныхsDявляетсяG.Доказательство. Если С= Ф, ГsГиD,также аксиома.f- 8,Ф-аксиома, тоsC =sФ,Гл. б.
Теория доказательств236Дляиликаждогоперехода,соответствующегоструктурному правилу,s-переход (т. е. переход влегкоге, Ф; г1--гsD/\1---соответствующийпо тому же правилуw1---е,е, ФАwсоответствующий переход естьsГНо s(ФпропозициональномучтоsD) осуществляетсяD переход таков:вывода. Например, пусть втогда впроверить,Ф)=s(Ф)/\1--- s8, sФ; sГ 1--- s8, sФsГ 1--- s8, s(Ф /\ Ф)s(Ф), следовательно, это переход по тому жеправилу (введение конъюнкции в заключение).Рассмотрим теперь переходы, соответствующие кванторным правилам.
Пусть переход вDтаков:Гl---8,(Ф)fГТогда вsD1--- 8, :3хФ.соответствующий переход будетsГsГПо следствию6.4.4 g1--- s8, s((Ф)f)1--- s8, s(:3хФ).не имеет связанных вхождений в формулу:3хФ; следовательно, для любого термаt'формулы Ф имеем gТогда по предложению=(sФ)~(t)· Итак, в дереве6.4.8s((Ф)t')(j. Fx(t').sDпереходом будетsГ 1--- s8, (sФ)~(t)sГ 1--- s8, :3х(sФ)'но это переход по правилу введения квантора существования в заключение.Рассмотрим теперь переход вDпо правилу8:[ФJ;,г1---е:3хФ,Гl---8'где у не имеет свободных вхождений в Г,ходом вsD8.Соответствующим перебудетs[Ф]l, sГ 1--- s8s(:3хФ),sГ1--- se·Как и выше, устанавливается, что s[Ф]l = (sФ)~(у = (sФ)l = [sФ]~и что переменная у не встречается свободно вs~, s8.Последнее237Теорема Эрбрана§ 6.4.утверждение вытекает из того, что для любой формулы Ф формула sФможет содержать только одну новую свободную переменную, а именно,хо, которая вDне встречается, в частности, хо =/=- у. Тогда вsDпереходимеет вид[sФ]~, sГ f--s8:3х(sФ), sГ f-- s8'где у не входит свободно в sГ,правилуs8.Следовательно, это переход по8.Аналогично рассматриваются правила9и1О.DПриступим теперь к рассмотрению основного утверждения настоящего параграфа.
Для сокращения записи последовательность термовt1, ... , tn будет обозначаться через t; :3х означает :3х1 ... :3хп; z последовательностьz1, ... , Zn.Теорема 6.4.11. Пусть секвенция С= Г f-- 0, Ф такова, что Ф =:3x'v'y\J!(x, у, z), и п-местный функциональный символ g не имеетвхождений в С. Секвенция С доказуема в G тогда и только тогда,когда в G доказуема секвенция С* = Г f-- е, :3x\J!(x, g(x), z).=Необходимость. Отмеченной формулой назовем всякую формулу Фо исчисленияGвидаявляющуюся обобщенной подформулой формулы Ф. Если Фо-отмеченная формула, то через Ф 0 обозначим формулуПустьD -переменных.доказательство секвенции С со свойством чистотыПусть деревосеквенцийкаждого вхождения каждойD*получено изотмеченной формулыФо,Dзаменойявляющегосяпредком вхождения Ф в заключительную секвенцию С, на формулуФ 0 .
Заметим, что заключительной секвенцией дереваПокажем, чтоD*D*будет С*.является квазивыводом.На вершинах дереваD*будут стоять те же аксиомы, что и вD,так как отмеченные формулы не являются атомарными (содержат кванторVy).Всем переходам дереваD*Dбудут соответствовать переходы деревапо тем же правилам вывода, за исключением переходов видаz))x,,... ,XnJYt,, ... ,tn U(Vy\J!(x у, z))x,, ... ,Xn'лf--Л, [(Ф(х, у,лf--л''tl,···,tn(6.2)238Гл.6.Теория доказательствгде главная формула перехода является отмеченной и предком формулы Ф.Этому переходу вD*соответствует переходЛ' 1--- Л', [(Ф(х, у,z))x,,XnJYt,, .......
,tnU(6.3)А' 1--- Л', (Ф(х, g(x), z))fВоспользуемся индукцией по глубине вывода и будем предполагать,что секвенция, стоящая над чертой в переходе (6.3), является доказуемой. Так как и не имеет вхождений в Л, Л и Л', Л' имеет те жепеременные, что и Л, Л, то и не имеет вхождений в Л', Л'; следовательно, доказуема секвенция Л' 1--- Л', \fу(Ф(х, у, z))f. По предложению6.2.2тогда доказуема и секвенцияЛ'но ((Ф(х, у, z))f):(t)=1---Л', ((Ф(х, у, z))f):(t)'(Ф(х, g(x), z))f, следовательно, секвенция, стоящая под чертой в переходе(6.3), доказуема.Необходимость установлена.Достаточность. Специальной формулой назовем всякую формулу вида (3xs+l ...
3хп Ф(х,лу 3хФ(х,g(x), z)Замечаниеg(x), z))fi':.::·.t:•, О~ s < п. Обозначим формучерез Ф*.6.4.12.Если Фоспециальная формула, то g имеет-связанное вхождение в Фо.Замечание=6.4.13.Если Фо6.4.14.Если Фоспециальная формула, то (3(Фо)=(3(Ф*).Замечаниеобобщенная подформула формулы-Ф*, которая имеет связанное вхождениеg,то формула Фо являетсяспециальной.ПустьD -доказательство секвенции С* со свойством чистотыпеременных.Замечание6.4.15.Если Фоспециальная формула, то Фо не-является главной формулой переходов в деревеправиламЛемма6.4.16.Если Го 1--- 0осеквенция из-Го, 0о имеет связанное вхождениеФо является предком формулыдереваD,осуществляемых по1-6.g,'1i *то Фо-Dи формула Фо изспециальная формула,из заключительной секвенцииD и Фо Е {0о} \ {Го}.До к аз ат ель ст в о. Пусть Фо имеет связанное вхождение g, Ф 1 потомок Фо в заключительной секвенции.
Тогда по следствию6.4.3§ 6.4.Теорема Эрбранаформула Ф1 имеет связанное вхождение239g. Но в заключительной секвенции только формула Ф* имеет связанное вхождение g. Следовательно, Фо является предком этой формулы. Тогда по замечанию6.4. l 4формула Фо является специальной.Предположим теперь, что Фо Е {Го}. Так как потомок Фо в заключительной секвенции лежит в правой части этой секвенции, то вDнайдется переходГ1,Ф1Г2такой, что Ф 1 и Ф2l--81I-- Ф2, 82потомки Фо. Легко проверить, что тогда этот-переход осуществляется по правилувыше Ф1 и Ф25и Ф2= ~Ф1.По установленномуспециальные формулы.
Имеем ,В(Ф2)-это невозможно, поскольку по замечанию= ,В(Ф*) = ,В(Ф2).6.4.13= ,В(Ф1) + l,справедливо ,В(Ф1)но=В силу полученного противоречия лемма доказана. ОДля формулы Фо обозначим через Ео(Фо) список всех формул вида(Ф(х, g(x), z))f таких, что термЕсли Гоg(t)имеет свободное вхождение в Фо.список формул, то через Ео(Го) обозначим список, состоя-щий из всех формул, входящих в списки Ео(Фо), где ФоГо. ЕслиS= ГоЗамечаниеформулы из-1-- Во - секвенция, то Eo(S) ;=: Ео(Го, Во).6.4.17.Если Фо-специальная формула, то Ео(Фо)-пустой список.Замечание6.4.18. Если формула Фо имеет вид Ф1тФ2, т Е {/\, V},U Ео(Ф2); если Фо = ~Ф1, то Ео(Фо) = Ео(Ф1).то Ео(Фо) = Ео(Ф1)ЗамечаниеЕсли ХЕ Ео(Фо) и переменная и имеет свобод6.4.19.ное вхождение в Х, то и имеет свободное вхождение в Фо или в Ф *.ПустьE(S))S=Го 1-- Во-секвенция изD.Через Е(Во) (соответственнообозначим список всех специальных формул из Во (из Го, Во).Обозначим через Во список всех формул ИЗ Во, не входящих в Е(Во).S* ;=: Го 1-- 8 0, Ео(Го, Во), Ф*.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
