1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 12
Текст из файла (страница 12)
Существенным переходом в доказательствеввидедереваперестановкиПусть Фназывается5)-ипереходпоправилам,отличнымотDправил6).атомарная формула. Будем доказывать лемму в этомслучае индукцией по числу существенных переходов в доказательствеDсеквенции ГЕслиf- 8, Ф.не имеет существенных переходов, то ГDf- 8, Фотличаетсяот аксиом только перестановкой формул.
Тогда либо Ф Е Г, либо Ф Е Г,Ф Едля некоторой атомарной формулы Ф. В первом случае доказу8емость Г,Г'следует из доказуемости Ф,Г'f- 8,8'Во втором случае доказуемость Г, Г'с помощью леммыf- 8, 8'f- 8и леммы1.9.4.f- Фследует из аксиомы Ф1.9.4.Пусть доказательствоDсеквенции Гf- 8, Фимеет п>О существенных переходов. Пусть последний существенный переход являетсяприменением правилаГ,f-1):81,Ф,82, Ф; Г1Г1f- 81,Ф,82,Хf- 81, Ф, 82, Ф /\ Хгде последовательности Г1 ими последовательностей Г и(81, Ф, 82, Ф /\ Х) являются перестановка(8, Ф). Из индукционного предположения,используя правила перестановки,Г,Г'f- 81,82,8',Ф и Г,Г'f-получаем доказуемостьсеквенций81,82,8',Х.
Применяя правилоправила перестановки, получаем доказуемость секвенции Г, Г'1) иf- 8, 8'.Случаи применения других правил в последнем существенном переходедля атомарной формулы Ф рассматриваются аналогично.Продолжим доказательство леммы, применяя индукцию по длинеформулы Ф. Пусть ГЕсли ФГf- 8, Х=Ф/\f- 8, Фи Ф, Г'Х, то по леммеи Ф, Х, Г'f- 8'.f- 8' доказуемы в Со.1.9.5 доказуемы секвенцииГf- 8,Ф;Из индукционного предположения получаемсначала доказуемость секвенции Г, Х, Г'f- 8, 8', а затем секвенцииf- 8, 8' получаем теперь с помощью структурных правил 5)-8).Если Ф = ~Ф, то по лемме 1.9.5 доказуемы секвенции Ф,Г f- 8 иГ' f- 8', Ф. По индукционному предположению получаем доказуемостьГ', Г f- 8', 8, а значит, и Г, Г' f- 8, 8'.ОГ, Г, Г'f- 8, 8, 8'.ЕсличерезДоказуемость секвенции Г, Г'8 - последовательность Ф,, ... , Фn формул исчисления~0 будем обозначать последовательность ~Ф1, ...
, ~Фп.Со, тоГл.58Лемма~е, Гf- J1.9.7.1.Исчисление высказыванийЕсли секвенция Гдоказуема в Со, то секвенцияf- 0доказуема в ИВ.До к аз ат ель ст в о.квенции Гf-Индукция по высоте доказательстваDсее в Со. Предлагаем читателю применить свой опыт подоказательствам в исчислении ИВ, полученный при чтении предыдущих параграфов.DПредложение 1.9.8. ив<-.v)< С0 .До к аз ат ель ст в о. Если в Со доказуема секвенция Гсодержит один член, то из леммыl.9.7и предложенияf- е, где еl.9.3 следуетдоказуемость г f- ев ив(-,v)_Рассмотрим секвенцию S, доказуемую в ив(-.v). Индукцией по высоте доказательства D секвенции S в ив<-.v) покажем доказуемостьS в Со.Пусть D - аксиома Ф f- Ф исчисления ив(-.v)_ Если Ф - атомарная формула, то Ф f- Ф - аксиома Со. Если Ф = Ф /\ Х и секвенцииФ f- Ф, Х f- Х доказуемы в С 0 , то по лемме l.9.4 и правилам l) и 2)получаем доказуемость Ф f- Ф в Со.
Если Ф = ~w и секвенция Ф f- Фдоказуема в Со, то по правилам 3), 4) и 6) получаем доказуемость в Сосеквенции Ф f- Ф.Пусть высотаравна пD>Ои для всех секвенцийS',имеющихдоказательство в ив<-.v) с высотой < п, доказуемость S' в Со установлена. Если последний переход в D осуществляется по правилам l)или l l) исчисления ИВ, то доказуемость S в Со следует из индукционного предположения с помощью правил l) и 6) исчисления Go.Если D имеет один из следующих видов:D'Гf-ФАwгто доказуемостьлеммыl.9.5Sf-фги правилалеммыSf-фв Со следует из индукционного предположения,6).Если последний переход вто доказуемостьD'D'Гf-Ф/\WDосуществляется по правилу12ИВ,в Со следует из индукционного предположения иl.9.4.Рассмотрим последний из возможных случаев, когдаD'~.гправила6), 8),f-имеет видD"~f-JИз индукционного предположения и леммыемость в Со секвенций ГDФ и Ф, Гf- J.l.9.5следует доказуПрименяя леммуполучаем доказуемость в Со секвенции Гf- J.l .9.6иD§ 1.9.Консервативные расширения исчислений59Исчисление Со является частью исчисления С, предложенного Генценом.
Исчисления генценовского типа по сравнению с изученныминами исчислениями являются более удобными при анализе и поискеформальных доказательств. Это объясняется основной особенностьюэтих исчислений, которая, грубо говоря, состоит в том, что сложностьформул при применении правил может только возрастать. ИсчислениеС будет подробно изучаться в гл.6.Здесь мы лишь применим отмеченное выше свойство исчисления Со для получения непротиворечивостиИВ, не прибегая к понятию интерпретации исчисления.В самом деле, рассмотрим секвенциюлегко заметить, что еслиD -f- Qo.Индукцией по высотедоказательство секвенциинии Со и существует вхождение формулы вD,Sсвязку/\ или~, то эта логическая связка обязана входить весли секвенцияf- Qoв исчислесодержащее логическуюS.Поэтомудоказуема в С 0 , то она может быть полученаиз аксиомы с помощью только правил5)-8),что очевидным образомневозможно.
Следовательно, исчисление Со непротиворечиво. Применяя предложенияl.9.l, l.9.3, l.9.8,получаем непротиворечивость ИВ.Упражненияl. Показать, что ив(->,Л) < ив, где ив(->,Л) получено из ив(->)удалением из алфавита символа /\ и соответствующих правил.2. Используя теорему~ полноты для ИВ, показать, что ивс-.v.~) << ИВ, где ив(->,V,) получается ИЗ ив(-.v) удалением из алфавита символа ~ и соответствующих правил.Глава2ТЕОРИЯ МНОЖЕСТВ§ 2.1.Предикаты и отображенияВсе изучаемые в этой книге объекты являются множествами, хотяназываются онипо-разному:слова,символы, совокупности,числа,функции, формулы и др.С интуитивной точки зрения, конечно, не все математические объекты суть множества, например, трудно думать о скобке или пропозициональной переменной как о множествах.
Однако посредствомподходящих соглашений (кодирования) их можно отождествить с множествами. В частности, скобку можно отождествить с множеством{{ 0}}.Этот метод является плодотворным, и в этой книге принимается такое соглашениепринимаемдвааксиомумножества,1).В качестве аксиомы теории множеств мыэкстенсиональности,имеющиходинаковыекотораяэлементы,утверждает,равны,-чтодругимисловами, любое множество определяется своими элементами.Если а1,... , ап -все элементы множества А, то в силу аксиомыэкстенсиональности множество А можно обозначать черезПри этом не предполагается, что а1,... , ап{ а 1 , ... , ап}попарно различны.
Ясно,что одно и то же множество А может иметь много таких обозначений,например,{а, Ь, а}= {а, Ь, Ь} = {а, Ь} = {Ь, а}.Множества0, {0}, {0, {0}}и т. д. (каждое последующее состоит извсех предыдущих) называются натуральными числами и обозначаются соответственно через О,чисел обозначаем черезl, 2и т. д. Множество всех натуральныхw. Слова а1а2 ... ап и конечные последовательности а1, а2, ...
, ап будут отождествляться с упорядоченным набором1)Для некоторых объектов, с интуитивной точки зрения не являющихсямножествами, мы фиксируем их кодировку через множества (например, длянатуральных чисел), для других мы кодировку не уточняем, так как в нашихрассуждениях она не участвует-важно лишь выделение этих объектов средидругих множеств, встречающихся в книге.§ 2.1.(а,,... , ап)ей ПОПредикаты и отображенияэлементов а,,... , ап,61который сейчас определим индукциn.Определение. Упорядоченный набор()пустого множества элементов равен 0.
Упорядоченный набор (а) одного элемента а равен а.Упорядоченный набор (а, Ь) двух элементов а и Ь называется упорядоченной парой и равен {{а},{а,Ь}}. Если пный набор (а,,((а,,... , ап)элементов а,,... , ап>то упорядочен2,равен упорядоченной паре... , ап-1), ап).Упорядоченный набор (а,,жем, а число п()пустого кортежа... , ап)иногда будем называть кортедлиной кортежа(а,,... , ап);равна нулю.
Кортеж длины ппри этом длина>2будем называтьупорядоченной п-кой или просто n-кой (тройкой, четверкой и т. д.).Отождествление слов и последовательностей с упорядоченными наборами возможно в силу следующего предложения.Предложение... , ап2.1.1.Если (а,,... ,ап)=(Ь,,... ,Ьп),то а,= Ь,,...= Ьп.До к аз ат ель ст в о. Из определения упорядоченного набора следует, что достаточно доказать предложение для п(а,, а2)==2.Из условия(Ь1, Ь2) и определения упорядоченной пары имеем {а,} ЕЕ (Ь1,Ь2). Так как (Ь1,Ь2)= {{Ь1},{Ь1,Ь2}}, то {а,}= {Ь1} или {а,}== а,.
Легко заметить, что если {х, у} = {х, z }, то у = z. Тогда из установленного равенства{{а,},{а,,а2}} = {{а1},{а1,Ь2}} получаем сначала {а,,а2} = {а1,Ь2},а затем а2 = Ь2.О={Ь1,Ь2}, поэтому Ь, Е {а,}, т.е. Ь,Определение. а). Множество {(а,,... , ап)1а, Е А,,называется декартовым произведением множеств А,,... , ап...
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
