1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 46
Текст из файла (страница 46)
, Yk -2).все свободные переменные термадоказательство секвенции Гf-tи пустьD -е, УхФ, обладающее свойством чистотыпеременных и такое, что любая переменная, исчезающая в этом доказательстве, отлична от переменных Уо, ... , Yk· Пусть [Ф];0 , ••• , [Ф];. все предки вида [Ф]~ вхождения формулы УхФ в заключительную секвенцию. Построим дерево секвенциивхождение секвенции С вD'следующим образом. Каждоезаменяем на вхождение секвенции С',Dполученной из С заменой всех предков формулы УхФ вида УхФ на ( Ф )t'и подстановкой термаtвместо всех вхождении переменныхЛегко проверяется, что все начальные секвенции деревааксиомами, а все переходыD'D,либо являются тривиальнымипереходами.
Последнее случается, когда вDсоответствующий переходЛ f- Л, [Ф];,Ли УхФzo, ... , z 8 •являютсялибо совершаются по тем же правилам,что и в соответствующем переходеестьD'-образом,f-предок формулы УхФD'Л, УхФзаключительной секвенции.есть квазивывод секвенции Гf- е, (Ф)t'.ТакимО§ 6.3. Сравнение исчислений ИПЕ и GСледствиеПусть переменная у не имеет вхождений ни6.2.3.в одну из формул секвенции Г::JхФ, Гдоказуемаf- 8)225f- 8, УхФ;эта секвенция (секвенциятогда и только тогда,когда доказуемасеквенция Г f- 8, [Ф]t (секвенция [Ф]t, Г f- 8).Для правил7инет (см.
упражнениеD10 хорошей формулировки свойства обратимости1), хотя оно справедливо в некотором <<распределенном по всему доказательству,> виде (ер. доказательство теоремы обустранении сечения в следующем параграфе).Упражнения1.Доказать,квенцияto, ... , tkчто не существует термов=3хР(х) f-(P)f0 ,••• ,(P)fkдоказуема,таких, что сехотясеквенция=3хР(х) f- =3хР(х) доказуема.2.3.Доказать вGПоказать,чтопредложениеупражнениемсеквенциюв::JzP(z) f- ::Jy\lxP(y).G* (см. упражнение 3 § 6.1)исчислении6.2.2 несправедливо. (Указание.2 и упражнением 3 из §6.1.)Воспользоваться§ 6.3.
Сравнение исчислений ИПЕ и GВ этом параграфе докажем, что секвенция исчисления ИП:r:, которая является и секвенцией исчисления--+импликациииравенства ~и(т. е. не содержит знаковGудовлетворяет условиюнесмешанности переменных), доказуема в ИП:r: тогда и только тогда, когда онадоказуема вG.В основе доказательства этого утверждения лежит следующая важная теорема об исчисленииG.Теоремаи Ф, Л6.3.1 (об устранении сечения).
Пусть Г f- 8, Фf- Л - доказуемые секвенции исчисления G. Если Г, Л f- Л, 8 -секвенция исчисленияG,До к аз ат ель ст в о.то она доказуема.Докажемтеоремусначаладляатомарнойформулы Ф индукцией по числу существенных переходов в доказательстве секвенции Гf- 8, Ф,понимая под существенными переходамите переходы, которые осуществляются по правилам, отличным от правил перестановки11и12.Если Г f-существенных переходов, то Гf- 8,8, Фимеет доказательство безФ отличается от аксиом толькоперестановкой формул.
Рассмотрим два возможных случая.1.Ф Е Г; тогда секвенция Г, Лзуемой) секвенции Ф, Лчения (лемма86.1.5)f-f- Л может быть получена из (докаЛ применением производного правила утони правил перестановки.Ю. Л. Ершов. Е. А. Палютин226Гл.Теория доказательств6.Существует формула Ф такая, что Ф Е Г и Ф Е2.ция Гf- 88;тогда секвендоказуема (перестановка аксиомы) и секвенция Г, Лf-Л;8получается из нее утончениями и перестановками.Предположим, что для секвенций Гf- 8, Ф,имеющих доказательство с менее чем п>ведлива. Пустьдоказательство секвенции ГD -О существенными переходами, теорема спраf- 8, Ф,имеющее псущественных переходов; будем предполагать, что доказательствоDобладает свойством чистоты переменных.Рассмотрим самый нижний существенный переход в доказательствеD.1°.Возможны следующие случаи.Переход имеет видГоЗдесь Г''f- 8 0, Ф, 8 0; Г1 f- 8 1, Ф, 8 1Г' f- 8', Ф, 8"(6.1)- перестановка Г; 8', 8" - перестановка 8; указанные вхождения формулы Ф являются предками вхождения Ф в заключительнуюсеквенцию Гf- 8, Ф.Секвенции Гоf- 8 0, 8 0, Фи Г1доказательство с числом существенных переходовлучаются перестановкой из секвенций ГоПоэтому доказуемы секвенции Го, Лf-f- 8 1, 0r, Ф<пимеют(так как они поf- 8 0, Ф, 8 0 и Г1 f- 8 1, Ф, 0n8 0, 8 0 и Г1, Л f- Л, 8 1, 0r.Л,Дерево секвенцийf- Л,8 1 ,8r8', 8"Го,Л f-Л,8 0 ,8 0 ; Г1,ЛГ', Лf-Л,Г,Лf-Л,8является квазивыводом, такглавной формулой перехода2°.как атомарная формула Ф не является(6.1).Переход имеет видГ'f-Г'Здесь Г'-перестановка Г,8' -8',Ф,Фf- 8, Ф .перестановка8,а указанные вхождения Ф являются предками вхождения Ф в заключительную секвенцию.ЕслиD' -квенции Г'вкаждойподдерево дереваf- 8', Ф,D, определенное вхождением в D сеD" получается из D' вычеркиваниемФ, то пустьсеквенции всехпредковзаключительной секвенции Г'правогоf- 8', Ф, Ф.вхожденияформулыНа вершинах дереваD"Фбудутсеквенции, отличающиеся от аксиом только перестановкой.
Переходыбудут либо тривиальны, либо происходить в соответствии с теми жеправилами, что и вD'.Простой перестройкой издоказательство секвенции Г'ство секвенции Гf- 8, Ф)f- 8', ФD"можно получить(а следовательно, и доказательс числом существенных переходов, равным§ 6.3. Сравнение исчислений ипr: и Gчислу существенных переходов впереходов вменьше чем вD'D'.227Так как число существенныхто по индукционному предположениюD,секвенция Г, Лf- д, 0 доказуема.3°. Переход имеет видГоГЗдесь Г'f- 0 0, Ф, 0 0f- 8', Ф, 0" .- перестановка Г; 0', 0" - перестановка 0; указанные вхождения Ф являются предками Ф из заключительной секвенции дереваDи Ф не является главной формулой этого перехода.0 0, 0 0, Ф получается из Го f- 0 0, Ф, 0 0 перестаСеквенция Го f-новкой, поэтому эта секвенция имеет доказательство с числом существенных переходовn - 1.секвенция Го, Л0f-д,Тогда по индукционному предположению0,0 0 доказуема.
Дерево секвенцийГо, Л f- д, 0 0, 0оГ',Лf- д,0',0"Г,Лд,0f-есть квазивывод.Итак, для секвенций Гf- 0,Ф с атомарной формулой Ф теоремаустановлена.Продолжим доказательство теоремы, применяя индукцию по построению формулы Ф.Предполагая, что для собственных (т. е. неравных Ф) обобщенных подформул формулы Ф и любых Г, Л,0, дтеорема справедлива, установим ее справедливость и для Ф.Пусть Фа Г, Л=ч:,/\f- 0, Ф -сти (предложениеЧ!, Х, Лf-Х; Гf- 0, Ф и Ф, Л f- д -секвенцияисчисленияG.доказуемые секвенции,Посвойству обратимо6.2.1) доказуемы и секвенции Г f- 0, Ф; Г f- 8, Х;д. Используя индукционное предположение, получаем, чтодоказуемы и секвенции Г, Х, Л f- д,0;и, наконец, доказуема секвенция Г, ЛСлучаи Ф= Ч:, V Х,=Пусть теперь Фквенции, Г, Лf-д,0 -Ф=Х, Г, Л f- д,Г, Г, Л f- д, е, е~ч:, разбираются аналогично.v'хФ; Г f-0, Ф и Ф, Л f- д -секвенция исчислениязательство секвенции Ф, Л0;f- д, 8.G.доказуемые сеПустьD -докаf- д.
Будем предполагать, что D обладаетсвойством чистоты переменных и что любая переменная у, котораяисчезает вD,отлична от всех переменных формул списка Г,новим индукцией по глубине вхождения в деревовхождения Л' f- д' секвенции вDD,секвенция Л *, Г f-0. Устачто для любого0, д' доказуема,где Л * получается из Л' вычеркиванием всех предков формулы Фзаключительной секвенции вида Ф.в•228Гл.Теория доказательств6.Ясно, что для самых верхних вхождений (Л'соответствующая секвенция Л', Г1-Л'менениями правила утончения). Рассмотрим переход вЛо1-Ло; л,А'1--аксиома)е, Л' доказуема (получается при1-1-Dл,Л'и предположим, что соответствующие верхним вхождениям секвенцииЛ0 , Г1-е, Ло и Лi, Г1- 81, Л1л0 , г1-доказуемы, тогдае, Ло; Лi, г1-е, л,Л*,Гl-8,Л'как нетрудно проверить, будет переходом по тому же правилу выводаи, следовательно, квазивыводом.
Аналогично обстоит дело для однопосылочных переходов, за исключением переходов вида(Ф)f, ЛоУхФ, Логде вхождение Ф=1- Ло1- Ло''vхФ в нижнюю секвенцию есть предок формулыФ заключительной секвенции деревасоответствуют секвенции (Ф)f, Л 0 , Гположим, что секвенция (Ф)f,Л 0 ,Гтеоремы Г1- 8, 'vхФ -доказуемаяD. Вхождениям в1- е, Ло и Л 0 , Г 11- 8,Ло доказуема.этот переходе, Ло. ПредПо условиюсеквенция, тогда понию 6.2.2 будет доказуема и секвенция Г1- 8,предложе(Ф)f.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
