1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 45
Текст из файла (страница 45)
Дляформул вида :3хФ, \lхФ выбираем переменную у, не имеющую вхождений в :3хФ, Г,и применяем индукционное предположение к формуле0,[Ф]~- Тогда, например, из доказуемости Г[Ф]~, Г1-- 0,1-- 0следует доказуемостьи квазивывод[ФJ~.г 1-- 0:3хФ, Гпоказывает, что :3хФ, Г1-- 0тоже доказуема.1-- 0оВ заключение отметим ряд простых свойств, которыми в дальнейшем будем пользоваться без явного на них указания.1.ЕслиГ1-- 0· Л 1-,' ,Г 1--0Л"есть переход, соответствующии одномуиз правил вывода, то для любой формулы Ф такой, что Ги А1--Ф, Л являются секвенциямиГ1--Ф,0; Л 1-- Ф, ЛГ' 1-- Ф, 0 11-- 0, ФG,Г, Ф1-- 0;Л, ФГ1 ,1-- 0Ф,1--Л1суть переходы, соответствующие тому же правилу вывода.2.Есливывода, ФГl--0-,--, - переход, соответствующий одному из правилГ 1--0- формула такая, что Г, Ф 1-- 0 - секвенция G и пе-ременные х и у не свободны в Ф в случае, когда этот переходсоответствует правилу8илито9,Г,Фl--0ГI--Ф,0Г'-1--Ф,01'Г', Ф1-- 0 1переходы, соответствующие тому же правилу вывода.3.Если Г 1-- ~ (Л ~ Л) - переход, соответствующий одному изГ1--0правил вывода, и Ф входит в Г'Г*1-- 0Г'*(Л*1-1--0 1Л)(0 1 ),то переход( Гl--0*(Л1--Л*))Г'1-- 0'*'Гл.
б. Теория доказательств220где Г*, Л*Л*) получены вычеркиванием из Г, Л(0*,фиксированного вхождения Ф в Г'(0')а Г'*(0'),(0'*)Л) предков(0,получено из Г'вычеркиванием этого вхождения Ф, является либо переходом,соответствующим тому же правилу вывода, либо тривиальнымпереходом (т. е. секвенции над чертой совпадают с нижней секвенцией этого перехода).УпражненияПоказать,1.что для любойформулыФ исчисленияпредикатовИПЕ существует эквивалентная ей формула '11, удовлетворяющаяусловию несмешанности переменных.2.
Проверить, что любая формула ИПЕ, находящаяся в пренекснойнормальной форме, удовлетворяет условию несмешанности переменных.Расширим язык исчисления3.допуская формулы и секвенцииG,и без условия несмешанности переменных. Установить, что тождественно истинная секвенция Р(х)в получившемся исчисленииПоказать, что если4.формулы QхФ, гдене доказуемасобственная обобщенная подформула'11 -Q-f- 3y'v'xP(y)G*.квантор, то существует термдля х в Ф и такой, что'11 -t,свободныйобобщенная подформула формулы (Ф)f.§ 6.2.Обратимость правилБольшинство правил вывода исчисленияGобладают еще однимпримечательным свойством, которое можно использовать при поискевывода в исчислении.
Свойство этообратимость, выражающаяся-(несколько огрублен но) в том, что секвенция, стоящая под чертойв правиле, доказуема тогда и только тогда, когда доказуемы секвенции(секвенция), стоящие над чертой.Сформулируем и докажем это свойство сначала для пропозициональных правил.Предложение6.2.1. 1).Если доказуема секвенция Гто доказуемы и секвенции г2).4).f- 0,Ф,Л'11,то доказуема и сеf- 0V '11,то доказуема и се'11, Г f- 0,то доказуемы и сеf- 0,Фw.Если доказуема секвенция Ф Vквенции Ф, Гf- 0, '11.'11, Г f- 0,f- 0.Если доказуема секвенция Гквенция Гf- 0, Фи гЕсли доказуема секвенция Ф Лквенция Ф, '11,Г3).f- 0, фи'11, Г f- 0.Обратимость правил§ 6.2.5).Если доказуема секвенция Гция Ф,Г6).ция Гf- 0, ·Ф,221то доказуема и секвенf- 0.Если доказуема секвенция ·Ф, Гf- 0,то доказуема и секвенf- 0, Ф.До к аз ат ель ст в о.Проверкавсехутвержденийпредложенияутомительна и однообразна. Поэтому докажем типичные случаи, например, утвержденияи1)Проверку будем вести индукцией по6).высоте доказательства (см.
также доказательство леммыУтверждение1.9.5).будем доказывать в чуть более общей форме и1)только для формулы Ф: если секвенция Гдоказуема и секвенция Гf- 0, Ф /\Ф, Л доказуема, тоФ, Л, причем существует доказательствоf- 0,с меньшим числом переходов, чем в доказательстве исходной.ПустьдоказательствосеквенцииDГf- 0,Ф/\Ф, ЛимеетвидDo;D1сЕсли Ф/\Фглавная формула последнего перехода, то-доказательство секвенции Гпоследовательность формул) иЕсли Ф/\Ф-Ф, Лf- 0,Do(в этом случае Лимеет меньше переходов, чемf-0о, Ф/\Ф, Ло и Г1вхождения Ф/\f- 01,ФФ в Со и С1дения формулы Ф/\f- 01, Ф, Л1DoиD1имеют вид/\Ф, Л1 соответственно, где выделенные-это предки рассматриваемого вхожФ в секвенцию С.
По индукционному предположению существуют доказательстваи Г1D.не главная формула последнего перехода, то заключительные секвенции Со и С1 доказательствГоDo пустая-DbиD~секвенций Го f- 0о, Ф, Лосоответственно. Тогда дерево секвенцийDb; D~Гf-0,Ф,Лбудет доказательством. (Так как Ф/\Ф не была главной формулойпереходаГоf- 0о, Ф /\ Ф, Ло; Г1 f- 01, Ф /\ Ф, Л1Гf-0,Ф/\Ф,Лто переходГоf- 0о, Ф, Ло; Г1 f- 01, Ф, Л1Г f- 0, Ф,Лосуществляется по тому же правилу, что и первый.)Пусть доказательство секвенции С имеет видDoсЕсли последний переход осуществляется не по правилумененному к Ф/\ Ф, а Со=Гоf- 0о, Ф /\ Ф, Ло -13,призаключительная222Гл.6.Теория доказательствDo,секвенция доказательствато по индукционному предположениюD 0 секвенциисуществует доказательствоГоf-0о, Ф, Ло и деревоDoГf-0,Ф,Лесть доказательство.Пусть последний переход в деревеDестьГf-0,Ф/\Ф,Ф/\Фге, Фf-!\wПо индукционному предположению существует доказательствоквенции Гf- 0, Ф !\D 0 сеD0Ф, Ф, причем число переходов доказательстваменьше числа переходовDo.Снова по индукционному предположениюDl секвенции Г f- 0, Ф, Ф.существует доказательствогТогдаD"оf- е, Фесть нужное доказательство.Докажем теперь утверждениеквенции СозательстводереваD=D~Ф, Гf- 0;Пусть6).по лемме6.1.4=Л'f-доказательство сеобладает свойством чистоты переменных.
Перейдем отк деревуD',сделав следующие преобразования: заменяемкаждое вхождение секвенции С= ЛС'D -можно считать, что докаf-Ф, д на вхождение секвенцииФ, д', где Л' и д' получаются из Л и д вычеркиваниемвсех предков формулы ~Ф заключительного вхождения секвенции Со,имеющих вид Ф или ~Ф. (Замечание. Легко с помощью индукциипроверить, что предок формулы ~Ф вида ~Ф может быть только в левойчасти секвенции, а предок вида ФчтоD' -для доказуемости секвенции Гто Л'Л'f-=-только в правой части.) Проверим,квазивывод секвенции Гf- Ф, 0.
Это, очевидно, достаточноf- 0, Ф. Если С= Л f- д - аксиома,Л; если последняя формула из д есть предок ~Ф вида Ф, тоФ, д' получается из аксиомы Лf-д применением только правилаперестановки; если последняя формула изд не есть предок ~Ф вида Ф,то Л'f-д'-ния (леммааксиома и Л'6.1.5)f-Ф, д' получается из нее правилом утончеи перестановками.Посмотрим теперь на переходы дереваесли в переходе дереваDD'.Легко проверяется, чтони один предок формулы ~Ф вида Ф или~Ф не является главной формулой, то соответствующий переход вD'будет осуществляться по тому же правилу вывода. Рассмотрим теперьслучаи, когда предок ~Ф вида Ф или ~Ф является главной формулойперехода.
Тогда этот переход может быть только по правилам6, 7, 9или по структурным правилам11-14.1, 3, 5,Обратимость правил§ 6.2.223Разбор всех случаев вряд ли поучителен. Рассмотрим случаи применения правил1, 5, 6, 9, 13.D имеет видПусть переход вд1-л,ди Ф= w t\ Хнижняял,1-w t\ хесть предок ~Ф, тогда переход вд'иw; д 1- л, хсеквенциявведения конъюнкцииПусть переход вD1-Ф, Л',w;д'1-может(1),д'D'будетФ, Л', Х1-Ф,Л'бытьполучена из верхнихперестановки(11)и сокращенияправилами(13).имеет видФ,дl-Л1-ди Ф= ~ir,л,~ir,есть предок ~Ф, тогда переход вw,д'D'будет1- Ф,Л'д'I-Ф,Л''нотак как Ф= ~ir,,тонижняя секвенция получается из верхнейприменением правил введения отрицаниякращения(5),перестановки(11)и со(13).Пусть переход вDимеет виддЛ, Ф1-~Ф,дl-Л'а Ф и ~Ф-предки формулы ~Ф (из заключительной секвенции), тогдасоответствующий переход вбудетD'д'Ф,Л'1-д'I-Ф,Л''т.
е. тривиален.Пусть переход вDимеет видд 1- Л,ди Ф= 'vxw -1-[w]tЛ, 'vxwпредок ~Ф, тогда соответствующий перевод вд'1д'ф Л''1-'[w]xуФ,Л'D'будетГл.224Теория доказательств6.и нижняя секвенция получается из верхней применением правил9(это применение законно, так как Л' и Л' являются частями Л и Ли у отлично от всех свободных переменных формулы Ф по свойствучистоты переменных вD), 11и13.Пусть, наконец, переход вDтаков:Лf-Л,Ф,Фли Фf-л, ф- предок ~Ф, тогда в D' соответствующий переходЛ'f-Ф,Л'Л'f-Ф,Л'обудет тривиальным.Обратимся теперь к кванторным правилам.Предложение6.2.2. 1).то для любого термаtсеквенция доказуема в2).Если в((Ф )t', Г f-е-секвенцияG,f-е,этаG.Если доказуема секвенция Гтакого, что Г f- е, Ф )t'доказуема секвенция :3хФ, ГGтакого, что-f- е, УхФ, то для любого терма tG, эта секвенция доказуема в G.секвенцияДо к аз ат ель ст в а этих утверждении аналогичны, поэтому приведем только доказательство утвержденияПусть уо,...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
