1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 47
Текст из файла (страница 47)
Так как (Ф)fявляется собственной обобщенной подформулой формулы Ф='vхФ,то, применяя индукционное предположение о справедливости теоремыдля собственных обобщенных подформул формулы Ф к доказуемымсеквенциям (Ф)f, Л 0 , ГГ, Л 0 , Г1-1-е, Л 0 и Г1-е, (Ф)f, получаем, что секвенцияе, Л 0 , е доказуема. Используя правила перестановок и сокращения, из доказуемости последней секвенции получаем доказуемостьсеквенции Л 0 , Г1-е, Ло.Итак, для каждого вхождения секвенции Л'ющая секвенция Л *, ГдереваD1-1-Л' вDсоответствуе, Л' доказуема. Заключительной секвенциибудет соответствовать доказуемая секвенция Л, Г1-е, Л.Используя правила перестановки, отсюда получаем доказуемость секвенции Г, Л1-Л,8.Случай, когда Ф имеет вид :3хФ, рассматривается аналогично.Замечание6.3.2.Можно считать, что теоремадопустимость следующего правилаГ-6.3.1правила сечения1- 8, Ф; Ф, Л 1г,л 1- л, еЛПриступим к доказательству основного утверждения.Оустанавливает§ 6.3.
Сравнение исчислений ипr: и GЕсли= Ф1, ... , Фп -0чать список ~Ф,,229список формул, то через ~е будем обозна-... , ~Фп.ПредложениеЕсли секвенция С= Г6.3.3.то секвенция С'= г, ~е f-f- 0 доказуема в G,J доказуема в ипЕ.До к аз ат ель ст в о. Доказывать будем индукцией по высоте доказательства в исчисленииG. Если Ф, Г f- 0, Ф - аксиома, то секвенцияФ, Г, ~е f- Ф доказуема в ИПЕ с использованием аксиомы Ф f- Ф и правила добавления лишней посылки; наконец,Ф, Г, ~еf-f-Ф; ~ФФ,Г, ~е, ~ф~Фf-Jесть квазивывод нужной секвенции в ИПЕ.Теперь для каждого правила вывода исчисленияGнужно проверить, что если секвенции Со (и С,), стоящие над чертой в правиле,таковы, что С0 (и с;) доказуемы в ИПЕ, то и секвенция С', соответствующая секвенции С под чертой, тоже доказуема в ИПЕ.
Проверкавсех правил достаточно утомительна, поэтому проверим это только дляправил2, 3, 5, 7, 8, 10:2). Пусть секвенция Ф, Ф, Г, ~е f- J доказуема в ипЕ, тогда следующее дерево секвенций есть квазивывод в ИПЕ:Ф/\ФФ/\Ф/\Фf-Ф/\ФФ /\ ir, f- Ф;f-Ф/\Фf-Ф·ФФ, Ф, Г, ~еf- Jf-~ФФ Г ~еФ/\Ф,Ф,г,~еf-;уФ /\ Ф,Г, ~е f- ~ir,ФAw,r,~ef-J3). Пусть секвенция г, ~е, ~Ф, ~ir, f- J доказуема в ипЕ, тогдаследующее дерево секвенций есть квазивывод в ИПЕ:~w f- JГ, ~е, ~Ф f- wг, ~е. ~Ф,f-ФV~Ф;Ффf-фf-ФVФ;г, ~еf-Г, ~е, ~ФФvf-ФVWw;~(ФV w) f- ~(Ф V w)5). Пусть секвенция Ф, Г, ~е f- J доказуема в ипЕ, тогдаФ, Г, ~еГ, ~еf-f- J~Ф;г, ~е.
~~Фесть КВаЗИВЫВОД В ИПЕ.f-~~Фf-i~~ФГл.230Теория доказательств6.7). Пусть секвенция г, ~е, ~(Ф)f f- J доказуема в ипЕ, тогдаГ, ~е, ~(Ф)ff- JГ, ~еf-(Ф)fГ, ~еf-:3хФ;f-~зхФf- JГ, ~е, ~зхФесть КВаЗИВЫВОД В ИПЕ.8). Пусть секвенция (ФJi, Г, ~е f-~зхФJ доказуема в ИПЕ, переменная уне имеет свободных вхождений в Г, ~е, тогдаf- J[Ф]~, Г, ~е:3у[Ф]~. Г, ~е:3хФf-:3у[ФJ~;г, ~е:3хФ, Г, ~еесть КВаЗИВЫВОД В ИПЕ.10). Пусть секвенция (Ф)f, Г, ~е f-f- J~зу[Ф]~f-f- JJ доказуема в ИПЕ, тогда(Ф)f,Г, ~е\lхФ, Г, ~еf- Jf- Jесть КВаЗИВЫВОД В ИПЕ.Проверка оставшихся правил вполне аналогична уже рассмотренным.
Индукция по высоте доказательства вGзавершает доказательство предложения.ПредложениеD6.3.4.Если секвенция С исчисленияGдоказуемав ИПЕ, то она доказуема и в исчислении G.До к аз ат ель ст в о. Установим сначала доказуемость вGаксиомФ f- Ф исчисления ИПЕ индукцией по построению формулы Ф. ЕслиФ-атомарная формула, то Фформул Ф и Ф вследующие квазивыводы вфf-Ф, ФФ/\Фf-Ф-аксиома исчислениядоказуемы секвенции ФGФ, ФФ/\Фf- Фf- ФФf-Ф,ФФf-Ф/\ Ф f- Ф/\ Фf-G.~Ф, Фf-Фf-Ф,ФФVФf-ФVФ~ф'[ФJi f- [ФJi(ФJi f- [ФJi~-:3хФ:3хФ f- 3хФ'УхФ f-УхФУхФf- [Ф]t·Пусть дляФ. РассмотримФVФ; Фf- ФVФфФ, ~ф~фf-фf- фf- Фf- Ф;ff-Ф и ФG:ффf-§ 6.3.
Сравнение исчислений ИПЕ и G231В двух последних квазивыводах переменная у выбрана так, что онане имеет никаких вхождений в Ф. Эти квазивыводы показывают, чтоможно завершить индукционное доказательство того, что всеции вида ФФ, где Фf---формула исчисленияG,доказуемы всеквенG.Теперь необходимо для каждого правила вывода исчисления ИПЕ(за исключением правил,касающихся импликации)если секвенции, стоящие над чертой, доказуемы встоящая под чертой, также доказуема вG.G,проверить, чтото и секвенция,Правила1, 11, 13-16исчисления ИПЕ являются частными случаями правил вывода G. Дляправил2и3Гf--Ф/\ФГf--Ф/\ФГf--ФГf--Фнеобходимое утверждение следует из соответствующего свойства обратимости (предложение6.2.2).Для правила 4Гf--ФГквазивывод вGf--(ФVФГ(5)Гf-- Ф )f--ФVФ( ГСФ)Гf--ФГf--Ф,ФГf--Ф,ФГf--Ф,ФГf-- ФVФГf--ФVФустанавливает необходимое свойство.
Рассмотрим теперь правилоГf--ФV Ф;f--Г, ФХ; Г, Фf--6:ХГf--ХЕсли секвенции, стоящие над чертой, доказуемы вдерево,G,то следующееиспользующее допустимое правило сечения (см.после доказательства теоремы6.3.1 ),есть квазивывод вГ,Фf--ХГ,Фf--ХФ,Гf--Х;Ф,Гf--ХГf--ФVФ;замечаниеG:ФVФ,Гf--ХГ,Гf--ХГf--Х.Правилу9соответствует утверждение об обратимости правила введения отрицания.Для правила10,если Гтимости) доказуема вGf--Ф и Гсеквенция Г, Гf--,правилаустановлена ранее.12вGf--~Ф доказуемы всеквенция Ф, Гf--,а по теоремеа следовательно, и секвенция Гf--.G,то (по обра6.3.1доказуемаДопустимость232Гл.Теория доказательств6.Индукция по высоте доказательства секвенции С в исчисленииИПЕ и завершает доказательство.Следствием предложенийО6.3.3и6.3.4и является основное утверждение этого параграфа.Теорема 6.3.5.
Секвен.ция исчислен.ия ИПЕ, являющаяся и секвен.цией исчислен.ия G, доказуема в ИПЕ тогда и только тогда,когда он.а доказуема в исчислен.ииОG.Упражнение1.Показать, что в исчислении6.3.1G* ( см. упражнение 3 § 6.1) теореманесправедлива. (Указание. Воспользоваться результатамиупражненияи упражнением3 § 6.23 § 6.1.)Теорема Эрбрана§ 6.4.В этом параграфе мы установим весьма важную теорему Эрбрана,которая, в частности, является теоретической основой современныхмашинныхметодовпоискадоказательствависчислениипредикатов.Один из таких методов основан на исчислении резольвент, котороебудет рассмотрено в следующем параграфе.
Теорема Эрбрана обосновывает обнаружение этим методом доказуемости любой доказуемой формулы ИПЕ; последнее свойство называется полнотой метода. Теоремаэта также придает определенный конструктивный смысл произвольнымпредложениям исчисления предикатов.Начнем параграф с изучения некоторых синтаксических связей.С каждым термомFx(t)tи переменной х свяжем некоторое множествофункциональных символов:а) если х не входит вб) если х входит вtили хиtt -f.функционального символа= t,hиFx(t) = 0;= h(t1, ... , tn)термов t1, ... , tn;тох, тоtдля некоторыхполагаем тогдапFx(t) = {h} U U Fx(ti).i=lЛемматермаt6.4.1.Если хДо к аз ат ел ь ст в омаt.-f.у и х н.е входит вt',то для любогоимеет место равен.ствопроводитсяиндукцией попостроению терО§ 6.4.ПредложениеЕсли QхФ6.4.2.233Теорема Эрбрана(QЕ{\i, ::3}) - обобщенная подto формулы Ф найдетсяформула формулы Ф, то для любого терматакой термиt1формулы Ф, чтонаходится в области действия квантораt1До к аз ат ель ст в о.Qx.Так как QхФ является обобщенной подформулой формулы Ф, то существует такая последовательность формул=ФоФ, Ф1,...
, Фп=i < nQхФ, что для любоговыполнено одно изусловий:(1)Фi(2) Фi= ~Фн1;= Фн1тФн1=(ФiФн1тФн1) для подходящей формулы Фн1и т Е {V,/\};(3) Фi = Q'yXi, Фн1 = (Xi)i для подходящих формулы Xi, переменной у, терма t, свободного для у в Xi, и Q' Е {\i, ::3}.Предположим теперь справедливость предложения длявкачестве Ф взять формулу Ф1. . .
, Фп =маиttoпоследовательности Фоформулы Ф в Ф1 можно указать термудовлетворяет условиюили(1)(2),tQx.ЕслиФ, Ф1,...t1(3),такой, чтоFx(to) = Fx(t)Если переход от Фо к Ф1то Ф1 является подформулой (а нетолько обобщенной подформулой) формулы Фусловие=QхФ, то по индукционному предположению для любого тервходит в область действия квантораискомогоn - 1.= Фо,нужно взять соответствующий термпоэтому в качествеt.Если выполненото рассмотрим три возможных подслучая.Подслучай (За): у= х.
Тогда Ф=Q'xX, Ф1=(X)f для подходящейформулы Х. Так как Ф1 (и, следовательно, Х) имеет (по индукционномупредположению) связанные вхождения переменной х, то по свойствунесмешанности переменных х не имеет свободных вхождений в Хи Ф1=Х, Ф=Q'xX; Ф1 есть подформула Ф.Подслучай (Зб): у =1- х и х входит в t. Тогда Ф 1 = (X)J;, Ф = Q'yXдля некоторой формулы Х. Формула Ф1 имеет связанные вхожденияпеременной х; если бы Х имела свободные вхождения у, то нарушалосьбы условие свободы термаtдля переменной у в формуле Х.
Итак, у неимеет свободных вхождений в Х и Ф1= (X)J: = Х;Ф=Q'уФ1; Ф1 естьподформула Ф.Подслучай (Зв): учто Ф1=J хих не входит вt. Пусть Х - такая формула,= (X)J;, Ф = Q'yX. Для любого терма t2 формулы Ф1соответствующий терм t1 формулы Х такой, что t2еслиt2входит в область действия какого-либосуществует=(t1)J:, причемквантора в Ф 1 , то t 1входит в область действия такого же квантора по той же переменной.По лемме 6.4.1имеемFx(t2)=Fx((t1)J:)=Fx(t1);если t2 выбранГл.
б. Теория доказательств234в Ф 1 дляtoв соответствии с заключением предложения, то соответствующий термt1будет удовлетворять заключению предложения дляформулы Ф.Предложение доказано.ОБудем говорить, что функциональный символgимеет связанноевхождение в формулу Ф, если Ф содержит подформулу вида QхФ и Фимеет вхождение термаtтакого, чтоg Е Fx(t).Укажем два следствия предложенияСледствиеЕсли Ф6.4.3.и функциональный символобобщенная подформула формулы Ф-g6.4.2.имеет связанное вхождение в Ф, тоимеет связанное вхождение и в Ф.СледствиеленииG6.4.4.ЕслиD -доказательство секвенции С в исчиси функциональный символgне имеет связанных вхожденийни в одну из формул секвенции С, тодений ни в одну из формул дереваgне имеет связанных вхожD.По свойству подформульности и следствиюЗафиксируем термg,to,начинающийся с функционального символазависящее от выбора парыа) если t -в) если(to, хо))6.4.5.Если термts(существеннотермов так:переменная или константа (отличная отt = f(t1, ...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
