1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 28
Текст из файла (страница 28)
(См. подстрочное примечание на с.133.)Упражненияl.Привести пример формулы Ф исчисления предикатов, для котороймножества2.{Ф}и {~Ф} непротиворечивы.Вывести теорему компактности из теорем§ 4.5.4.1.5и4.4.5.Исчисление предикатов гильбертовского типаЗафиксируем произвольную сигнатуру Е. Все зависящие от сигнатуры понятия этого параграфа будут относиться к сигнатуре Е.В этом параграфе мы рассмотрим исчисление ИПf, которое называется исчислением предикатов гильбертовского типа, и покажем егоравносильность (теорема 4.5.6) исчислению ИПЕ подобно тому, как в§ l .8 была показана равносильность ИВ и ИВ1.Формулами ИПf будут формулы сигнатуры Е за исключением того,что в алфавите ИПf нет символа логической константы i и, соответственно, в определении формулы отсутствует п.
О). Секвенций в ИПfнет.Аксиомы ИПf получаются из следующих 14 схем заменой переIJi, Х конкретными формулами сигнатуры Е; t, q - термамименных Ф,сигнатуры Е:l.2.Ф----,(IJi----, Ф),IJi)----, ((Ф----, (IJi----,IJi)----, Ф,IJi)----, IJi,(IJi----, (Ф л IJi)),(Ф----,Х))----, (Ф----, Х)),3. (Ф Л4. (Фл5. Ф----,6. Ф-(Фvw),7. Ф ----, ( l]i V Ф),8. (Ф----, Х)----, ((IJi----, Х)----, ((Ф V IJi)----,9. (Ф----, w)----, ((Ф----, ~w)----, ~Ф),10.l l.~~Ф----, Ф,\iхФ----, (Ф)f,Х)),Гл.1364.Исчисление предикатов12.
(Ф)f-+ :3хФ,13. t ~ t,14. t ~ q-+ ((Ф)f-+ (Ф)~).Правила вывода ИПf:l Ф, Ф-+.ww'где в правилах22и3w-+ Ф. w -+ \iхФ'ф-+ ф'3.---,3хФ -+ wпеременная х не входит свободно вw.Доказательством в ИПа формулы Ф называется такая последовательность Фа, ... , Фп формул ИПf, что Фп=Ф и для каждого i ~ пформула Фi удовлетворяет одному из следующих условий:l) Фi - аксиома ипf,2) Фi получается из некоторыхj < i,Ф1 ,по одному из правилl-3.Если существует доказательство в ипf формулы Ф, то Ф называется доказуемой в ИПf или теоремой ИПf (обозначаем r> Ф).Выводом в ИПf формулы Ф из множества формул G называетсятакая последовательность Фа, ...
, Фп формул ИПf, что Фп = Ф и длякаждого i ~ п формула Фi удовлетворяет одному из следующих условий:l) Фi доказуема в ипf,Фi принадлежит G,3) Фi получается из некоторых2)Ф1 ,причем при применении правилвходить ни в одну формулу изj < i, по одному из правил l-3,2 и 3 переменная х не должнаGсвободно.Если существует вывод в ИПf формулы Ф из множества G, то Фназывается выводимой в ИПf из G. При этом G называется множеством гипотез. Очевидно, что доказуемость формулы эквивалентнаее выводимости из пустого множества гипотез.
Поэтому выводимостьФ изGможно обозначать черезG[> Ф. В этом параграфе, если неоговорено противное, под доказательством ивыводом понимаются доказательство и вывод в ипf.Правило выводафназывается допустимым в ИПf, если его добавление к исчислениюИПf не изменяет множества доказуемых формул.Предложение 4.5.l. Следующие правила допустимы в ИПf:Ф.а) \iхФ'(Ф)f.б) :3хФ'(Ф)f-+ W.в) \iхФ -+ w'Д о к а з а т ел ь ст в о. а).
Пустьжение, тогда в силу аксиомыl,w-r)w-+ (Ф)fw-+ 3хФ ·некоторое доказуемое предлодоказуемости Ф и правилаlимеемИсчисление предикатов гильбертовского типа§ 4.5.1>ФФ. По правилу----,2\iхФ следует по правилуполучаем 1>Ф----,137\iхФ. Отсюда доказуемостьl.в). Формулу \iхФ----, Ф получаем из аксиомы \iхФ----, (Ф)f и теоремы( Ф )f----,Ф с помощью аксиомДоказательство(упражнениеl, 2и правилаутвержденийб)иг)l.мыоставляемчитателюDl).Формулы Ф и Ф называются эквивалентными в ИПf, если в ИПf1доказуемы формулы Ф----, Ф и Ф----, Ф (обозначаем это через Ф- Ф).В силу правила l из Ф 1 Ф вытекает, что доказуемость Ф в ИПfравносильна доказуемости Ф в ИПf.Предложение4.5.2.Любая тавтология Ф, не содержащая символа логической константы, доказуема в ИПf.Доказательство.Пусть Фоснова Ф.
В силу теоремы-l.8.lформула Ф доказуема в ИВ1. Ясно, что, заменив пропозициональныепеременные в доказательстве в ИВ 1 формулы Ф на соответствующиеформулы ИПf, получим доказательство Ф в ИПf.Следствие4.5.3.Если Ф и ФD- пропозиционально эквивалентныеформулы ипf' то доказуемость ф в ипf равносильна доказуемости Ф в ИПf.DТеорема 4.5.4 (о дедукции для ИПf).
Если G u {Ф, Ф} - множество формул ипf, то из G u {Ф} 1> Ф следует G 1> Ф----, Ф.До к аз ат ель ст в о проведем индукцией по длинеn минимальногоG U {Ф }. Случай, когда п = l (т. е. Фдоказуема в ИПf или принадлежит G u {Ф}), а также случай, когдаФ п получается по правилу l, ничем не отличаются от соответствующихслучаев для ИВ 1 и уже рассмотрены в доказательстве теоремы l .8.3.вывода Ф1,... , Фnформулы Ф изВ силу минимальности вывода осталось рассмотреть случаи, когда Фполучается из Фn-1 по правиламПустьG 1> Ф ----t Фn-1·Ч'n-1 = (81 ----t 82) иили23.По предположению индукциимы уже имеемФ= (81----t\ix82).При этом в силуопределения выводах не входит свободно в Ф, элементыкак Ф----, (Х1----,Х2) и (Ф/\ Х1)----,Gи0 1.ТакХ2 пропозиционально эквивалентныдля любых формул Х1, Х2, то в силу следствия4.5.3последовательностьможно дополнить до вывода Ф----, Ф изG.Пусть теперь Ф получается по правилуи Ф=(:3х01----, 82),3.Тогда Фn-1где х не входит свободно в Ф,82= (81 ----, 82)и элементыG.Гл.1384.Исчисление предикатовВ силу пропозициональных эквивалентностей Ф----, Фn-l s 0 1 ----, (Ф----,___, 82) и :3х01 ___, (Ф ___, 82) s Ф ___, (:3х01 ___, 82) следующую последовательность:можно дополнить до вывода Ф----, Ф из G.Следствие 4.5.5.
Пусть Ф 1 ,{Ф1,... , Фn} 1>... ,DФп, Ф -формулы ИПf. ТогдаФ равносильно 1> Ф,----, (Ф2 ----, ... (Фn ----, Ф) ... ), чтов свою очередь равносильно 1> (Ф1 /\ ( ... (Фn-1 /\ Фn) ... ))----, Ф.До к аз ат ель ст в о. Для первой эквивалентности n раз применяется теорема 4.5.4 и правило 1. Для второй эквивалентности - те жерассуждения, что и в следствии 1.8.4.ОТеорема 4.5.6. Пусть Ф - формула, Г - конечная последовательность формул исчисления ИПf.
Для того чтобы формула Фбыла выводима в ИПf из множества всех членов Г, необходимои достаточно, чтобы секвенция Г 1-- Ф была доказуема в ИПЕ.В частности, для формул ИПf их доказуемость в ИПf равносильнаих доказуемости в ИПЕ.Доказательство. В силу правил 7 и 8 ИПЕ секвенция Ф 1 , ..•. . . , Фп 1-- Ф доказуема в ИПЕ тогда и только тогда, когда доказуема1-- Ф1 ----, (Ф2 ----, ... (Фп ----, Ф) ... ).
Тогда из следствия 4.5.5 получаем,что для доказательства необходимости можно ограничиться случаемГ = 0. Легко проверить, что аксиомы ИПf тождественно истинны,а правила вывода ИПf сохраняют тождественную истинность. Поэтомунеобходимость следует из теоремы Гёделя о полноте.Достаточность. Пусть дерево D - доказательство в ИПЕ секвенции ГI--Ф. Если ГI--Ф - аксиома ИПЕ, то в силу аксиом 13 и 14исчисления ИПf мы имеем Г 1> Ф. (Здесь и далее мы допускаем некоторую вольность в обозначениях: следовало бы писать {Ф1,если Г= Ф1, ... , Фn.)Пусть Фа-...
, Фn} 1>Ф,какое-нибудь предложение сигнатурыне содержащее логической константы i. Пусть D 1 получается изD заменой логической константы i на формулу Фа 1\ ~Фа. Ясно, чтоначальные секвенции в D останутся аксиомами ИПЕ, а переходы поr;,правилам, отличным от9и10, останутся переходами по тем же пра9 и 10 станут переходами по правиламвилам. Переходы по правиламГ, ~Ф9,·1--Фа 1\ ~ФаГ1--ФlO''Г1--Ф; Г1--~Ф· Г 1-- Фа 1\ ~ Фа ·Поэтому осталось показать, что если в правилах вывода1-8и11-16исчисления ИПЕ и правилах 9' и 10' заменить знак 1-- на 1>, то изистинности утверждений над чертой будет следовать утверждение подЧистое исчисление предикатов§ 4.6.139чертой. Для правил l-8 и l l, 12 исчисления ИПI; и правил 9' и 10'проверка - та же самая, что и в теореме l.8.l.
Для правил 13 и 15при Г = 0 это верно в силу предложения 4.5. l, а), б). Для остальныхслучаев это следует из следствия 4.5.5, правил 2, 3 исчисления ИПf ипредложения4.5.l,в),г).DИз этой теоремы и теоремы4.1. 7получаемСледствие 4.5.7. Если Е 1 ~ Е, то исчислен.ие ИПf являетсякон.сервативн.ым расширен.ием исчислен.ия ИПf 1 •DИз теоремыИПfIследует также, что для формул Ф и Ф исчисленияэквивалентности Ф I Ф и Ф Ф равносильны.4.5.6=Следствие 4.5.8.
Пусть Х U { Ф} - мн.ожество формул исчислен.ия ИПf 1 , а У - мн.ожество всех перемен.н.ых, входящих свободн.охотя бы в одн.у формулу из Х U { Ф}. Для того чтобы имело местоХ 1> Ф, н.еобходимо и достаточн.о, чтобы выполн.ялось следующееусловие: для любой алгебраической системы 12{ сигн.атуры Е и ин.терпретацииф Е Х, то 12{,:У----, А, если имеет место 12{F Ф["f].FФ['У] при любомДо к аз ат ель ст в о. Так как вывод содержит лишь конечное множество формул, то Х1> Ф равносильно тому, что Х1 1> Ф для некоторого конечного Х 1 ~ Х. Необходимость тогда следует из теореми4.1.5.F Ф['У], Ф Е Х,Если из 12{12{ сигнатуры Е и,:Ули.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
