1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 49
Текст из файла (страница 49)
Образуем дерево секвенцийD каждого вхождения секвенции S на секвенцию S*. Докажем индукцией по глубине дерева,что все секвенции из D* доказуемы.Если S - аксиома, то S* получается из S утончениями и перестановками. Если в D переход осуществляется по одному из правил l-6,то соответствующий переход в D* может быть получен несколькимии положимD*,которое получается заменой в деревеутончениями, перестановками и применением того же правила.Для примера рассмотрим случай, когда в деревеществляется по правилуDпереход осуl:(6.4)240Гл.гдеSo= Го1--- Во, Фо,S0 = ГоS1 =Теория доказательств6.Го 1--- Во, Ф1,= Го 1--- Во, Фо А Ф1.S2Тогда1--- В 0 , Фо, Ео(Го, Во), Ео(Фо), Ф*,= Го 1--- В 0 , Ф1, Ео(Го, Во), Ео(Ф1), Ф*,s:;_ = Го 1--- в;;, Фо А Ф1, Ео(Го, Во), Ео(Фо А Ф1), Ф*.SjЗаметим, что формулы Фо, Ф1 и Фо А Ф1 не могут быть специальными.ТогдаiE(So) == о, 1,D*,ЩS1)= ЩS2).Поскольку правиладопустимы, квазивыводсоответствующий переходуs;s·s,•.Oосуществляет переход в дереве1(6.4) в D.Рассмотрим случай, когда переход в деревеправилуDосуществляется по8:So(6.5)S1'где So=[Фо]~,Го 1--- Во,S1 =0=Возьмем секвенции S:3иФо,Го 1--- Во.[Фо]~.
Го 1--- В 0 , Ео([Фо]~. Го, Во), Ф* и Sj===:3иФо, Го 1--- В 0 , Ео(:3иФо, Го, Во), Ф*.=Ео(:3иФо). Включение 2 очевидно. Предположим, что Ео([Фо]~)Тогда формула :3иФо содержит связанное вхождение g иПокажем,чтоЕо([Фо]~):f.:f. Ео(:3иФо).по замечанию6.4.12и лемме6.4.16не должна входить в левую частьсеквенции Sj. Чтобы утверждать, что переходпоправилу8,нужнопроверить,чтоs;s·осуществляетсяпеременнаяинеимеетсвободных вхождений в Го, В 0 , Ео(:3иФо, Го, Во), Ф*. Действительно,переменная и, очевидно, не входит свободно в Ео(:3иФо), не входитсвободно в Ф * по свойству чистоты переменных, не входит свободнов Го, Во, а, следовательно, и в Ео(Го, Во) по замечанию 6.4.19, такs;s·sкак S~ -переход по правилу 8. Итак, переходв дереве D*осуществляется по правилу 8.Рассмотрим теперь случай, когда переход (6.5) в дереве D осуществляется по правилу 9, где So = Го 1--- Во, [Фо]~.
S1 = Го 1--- Во, \fиФо.Формула \fиФо не является, очевидно, специальной. Если формула[Фо]~ специальна, тоgимеет связанное вхождение в [Фо]~. Но тогдаимеет связанное вхождение в \fиФо и, следовательно, по леммеg6.4.16является специальной, что, как уже замечено, невозможно. Покажем,что Ео([Фо]~) = Ео(\fиФо).
Включение Ео([Фо]~) 2 Ео(\fиФо) очевидно.Если Ео([Фо]~) :f. Ео(\fиФо), то формула \fиФо имеет связанное вхож-§ 6.4. Теорема Эрбранадениеg241и, следовательно, \iиФо специальна, что невозможно. Далее,рассуждая как в случае правила8,устанавливаем, что соответствующий переходГо f-- 880Siв деревеD*0, :Ео(Го, 80, [Фо]t)(= I;о(Го, 80, \iиФо)), [Фо]t, w*Го f-- 8 0, :Ео(Го, 80, \iиФо), \iиФо, w*осуществляется по правилу9.(6.5) в дереве D осуществляетсяпо правилу 7, где So = Го f-- 80, (Фо)f, 81 = Го f-- 80, 3иФо. ПредвариРассмотрим случай, когда переходтельно установим следующие два утверждения.Лемма6.4.20.Если вГо f-- 80,символgGдоказуема секвенция3x\lyw(x, у, z), w(t, g(t), z),не имеет связанных вхождений в эту секвенцию ине имеет вхождений в Гоg(t)f-- 80, 3x\lyw(x, у, z), то в G доказуемасеквенцияГоf-- 80, 3x\lyw(x, у, z).До к аз ат ель ст в о.Го f-- 8 0 , 3x\lyw(x, у, z),ПустьD w(t, g(t), z); хо -доказательствосеквенциипеременная, не встречающаяся впаройD. Если s - синтаксическое преобразование, определенное(xo,g(t)), то по предложению 6.4.10 дерево sD являетсядоказательством (секвенцииГо f-- 80,по предложению6.4.8).3x\lyw(x, у, z), w(t, хо, z)Следовательно, секвенцияГо f-- 80, 3x\lyw(x, у, z), (w(x,, ...
, Хп, хо, z))fдоказуема. Легко проверить, что дерево секвенцийГо f-- 80,3x\lyw(x, у, z), [(w(x, у, z))~/:··:t:nJ~0Го f-- 80,3x\lyw(x, у, z), (\iyw(x, у, z))~,1:···.t:пГоf-- 80, 3x\lyw(x, у, z), 3x\lyw(x, у, z)Го f-- 80,является квазивыводом.3x\lyw(x, у, z)D242Гл.Следствие6.4.21.Теория доказательств6.Если вGдоказуема секвенцияГо f- 0о, :3хVуФ(х, у, z), Ф(t 1 , g(t 1), z), ... , w(t 8 , g(t8 ), z),символ g не имеет связанных вхождений в эту секвенцию и g(ti)не имеет вхождений в Го f- 0о, :3xifyw(x, у, z), то в G доказуемасеквенция Го f- 0 0 , :3xifyw(x, у, z).Для доказательства нужно расположить термы g(t'), ... , g(t 8 ) в порядкенеубывания длины,по s и леммуприменить индукционноеОВернемся к рассмотрению правиланеявляютсяреходалав(Фо)fпредположение6.4.20.специальными,D*тоустанавливаетсяявляетсякакспециальной,переход7.Если формулы (Фо)f и :3иФодопустимостьввыше.соответствующегоВслучае,когдаформула :3иФо такжеD*деревеспециальнаисоответствующийГоf- 0 0, (Фо)f, Ео((Фо)f, Го, 0о), Ф* над чертой совпадает с записьюпод чертой.
Рассмотрим случай, когда :3иФотривиален,пеформу-т. е.записьспециальная формула,а формула (Фо)f не является специальной. Тогда (Фо)f имеет вид(Ф(х, g(x), z))f- Если последняя формула входит в Ео(Го, 0о), то рассматриваемый переход в D* тривиален. Если же (Ф(х, g(x), z))f невходит в Ео(Го, 0о), то этот переход имеет вид0 0, (w(x, g(x), z))f, Ео(Го, 0о), Ф*Го f- 0 0, Ео(Го, 0о), Ф*Го f-и является квазивыводом по лемме(6.6)6.4.20.Для завершения доказательства теоремы осталось рассмотреть переходы по правилу= (Фо)f, Го f-0о,S110,т.
е.переходы= \lиФо, Го f-(6.5)в деревеD,гдеSo=0о. Тогда по определениюВо= (Фо)f,Го f- 0о,Ео((Фо)f,Го,0о), Ф*,Si = \lиФо, Го f- 0 0, Ео(\lиФо, Го, 0о), Ф*.По замечанию 6.4.12 и лемме 6.4.16 формулыспециальными. Следовательно, E(So)являютсячто Eo(So);;2Eo(S1).i= 1, ... , m,-Пусть( Фо)f и \lиФо неE(S,). Заметим,=w,, ... ,Wm, где Wi=(W(x,g(x),z))[,список всех формул из Eo(So) \ Eo(S1), т. е.
Eo(So)Переход= Eo(S1), Ф1, ... , Wm.(Фо)f, Го f\lиФо, Го f-0 0, Eo(So), Ф*0 0, Eo(So), Ф*=243§ 6.4. Теорема Эрбранаявляется переходом по правилу1О,а переход1- 0 0, :Eo(S1), W1, ... , Wm, W*1- 0 0, :Eo(S1), Ф*(Фо)t', Го\iиФо, Гоявляется квазивыводом по следствию6.4.21.Следовательно, переходВо(Фo)f,Гol-0 0 ,:Eo(So),W*Si\iиФо, Го1- 0 0, :Eo(S,), Ф *является квазивыводом.СкаждойОW,формулойнаходящейсявпренексной нормальнойформе, свяжем некоторую :3-формулу Ф н, которую назовем эрбрановой формой формулы Ф,по следующему правилу.Если Ф есть=:3-формула, то ФнФ; если Ф имеет вид :Jx, ...
:3xn \iyW(x, у, z) иg - п-местный функциональный символ, не встречающийся в Ф, тоФн= (:Jx, ... :3xnW(x,g(x),z))н.Индукцией по числу кванторов всеобщности устанавливается, что это определение корректно.Теорема Эрбрана. Пусть ФФ, где-формула в пренексной нормаль= :Jx, ... :3xn W(x, z) -ной форме, Фнэрбранова форма формулыбескванторная формула. Формула Ф доказуема тоW -гда и только тогда, когда существуют такие последовательно_, _11•-k _kkдфсти термов-1t - t 1, • •• , tn, ... , t - t 1 , ••• , tn,чтооказуемаормула-kW(t ,z) V ... V W(t ,z).До к аз ат ель ст в о.Используя индукцию (по числу квантороввсеобщности) и предыдущую теорему, получаем, что формула Ф доказуема тогдаитолько тогда,когда доказуемаформула Фн.Длязавершения доказательства теоремы установим следующееПредложение6.4.22.Формула Ф= :Jx, ...
3xn W(x, z),где Ф-бескванторная формула, доказуема тогда и только тогда, когдасуществует такая последовательность п-наборов термовчто доказуема формула W(t 1, z) V ... V Ф(i, z).-1-kt , ... , t ,До к аз ат ель ст в о. По свойству обратимости (правило 3 и предложение 6.2.1) формула W(t 1, z) V ...
v W(t\z) доказуематогда и толь_,-kко тогда, когда доказуема секвенция 1- W(t , z), ... , W(t , z).Пусть эта секвенция доказуема, тогда, многократно применяя правиловведенияквантораказуемую секвенциюсуществованиявзаключение,1- :JxW(x, z), ... , :JxW(x, z).Изс помощью правила сокращения получаем секвенциюустанавливается достаточность.получаемэтойдосеквенции1- :JxW(x, z).ТакГл.244Необходимость. ПустьнииGТеория доказательств6.D -доказательство формулы Ф в исчисле-со свойством чистоты переменных. Пустьборы п-термовt таких,t , ...
, -kt --1это все на-D встречается формула \Ji(t, z). Заметим,что все такие формулы дерева D являются предками формулы Ф. Пустьдерево D* получается из D заменой каждого вхождения секвенцииГо f- Ло на секвенцию Го f- \Ji(t 1, z), ... , \Ji(t\ z), Л1, где Л1 получаетсяиз Ло вычеркиванием всех формул вида (:3xs+I ... 3хп \Ji(x, z))fi:.::·.'t:s,О::;; s < п. Без труда проверяется, что полученное дерево D* будетквазивыводом (секвенции f- \Ji (t 1, z), ... , \Ji (i, z)). Действительно, навершинахстоятчто всеквенции,полученныеизаксиомперестановками.Переходу, соответствующему пропозициональным правилам, соответствуют переходы по тому же правилу (быть может, с сокращениеми перестановками).
Кванторные правила, за исключением правилав деревеDне используются; переходам по правилутривиальные переходы вответствуют переходы,Итак,D* -D*.77,соответствуютПереходам по структурным правилам сополученные применением структурных правил.квазивывод секвенции-1-kf- \Ji(t , z), ... , \Ji(t , z)и необходи-мость установлена.DСила теоремы Эрбрана состоит в том, что вопрос о доказуемостипроизвольной формулы сводится к вопросу о доказуемости формулы изнекоторой эффективно порождаемой последовательности бескванторных формул.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
