1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (Ю.Л. Ершов, Е.А. Палютин - Математическая логика), страница 5

Из двух начал одного и того же слова одно изних есть начало другого (нужно взять начало меньшей длины). Значит,Фо-началоилиWo,начало Фо. В любом случае применимоWo -индукционное предположение и, следовательно, ФоначалоW1.что Ф1= W1= Wo, т = т' и Ф1-Снова, применив индукционное предположение, получаем,и Ф=(ФотФ1)=(Woт'W1)= W.Доказательство предложениячинается с символаD1.2.1.Если формула Ф на­то доказывать нечего. Пусть Ф представлена·,в виде (ФотФ1), где т - один из символов /\, V или - , а Фо, Ф1 формулы ИВ, и в виде (Ф 0 т'Ф; ), где т' - один из символов /\, Vили - , а Ф 0 , Ф; - формулы ИВ.

Тогда Фо - начало Ф 0 или Ф 0-начало Фо. По лемме Фо = Ф 0 поэтому т = т' и Ф1представление Ф = (ФотФ 1 ) единственно.Следствие= Ф;.Следовательно,D1.2.3. Пусть Ф - формула ИВ. Тогда с каждым вхож­( или • в формулу Ф однозначно связано некотороедением символавхождение подформулы формулы Ф, первым символом которого яв­ляется рассматриваемое вхождениеДо к аз ат ель ст в о.вхождением символа(ние подформулы, а лемматакого вхождения.Предложениев Ф подформулИндукциейили(илипо•соответственно.длинеформулыскаждым• можно связать некоторое такое вхожде­1.2.2 позволяет утверждать единственностьD1.2.4.

Если Ф - формулаW, Х соответственно, тоИВ, 'Г/,вхождения0 -либо 'Г/ и0не имеют§ 1.2.Язык исчисления высказываний21общих вхождений символов алфавита ИВ, либо одно из них целикомсодержится в другом.До к аз ат ель ст в о. Если 'Г/ и0 имеютобщие вхождения символов,то первое вхождение первого символа 'Г/ или0должно быть общим.Пусть первое вхождение первого символа 'Г/ входит в0.Если Ф-атомарная формула, то утверждение очевидно.

Пусть Ф не атомар­на, тогда первый символ Ф естьили(~.По следствию1.2.3этотсимвол однозначно определяет вхождение некоторой подформулы Ф'в Х. Но эта подформула будет под формулой и в Ф.с рассматриваемым вхождением символа(В формуле Фили ~ связано вхождение 'Г/подформулы Ф. В силу единственности Ф должна совпадать с Ф',следовательно, 'Г/ целиком содержится вО0.Если все вхождения подформулы Ф в формулу Ф заменить на фор­мулу Х, то получим новую формулу, которую обозначим через (Ф)~.Такое определение корректно, так как из предложения1.2.4следует,что два различных вхождения подформулы Ф в Ф не имеют общихвхождений символов алфавита ИВ.Определение.

Секвенцией ИВ называется слово алфавита ИВ видаФ1, ... ,Фnгде Ф1, ... , Фn, Фчто при п=-f- Ф,формулы ИВ, п -натуральное число. Отметим,О это слово будет иметь видf- Ф.Часто секвенции будут обозначаться через Гf- Ф, где Г обозначаетпоследовательность формул ИВ, может быть, пустую.Если формулы ИВ можно рассматривать как <,формы,> сложныхвысказываний нашего языка, то секвенции являются <<формами>> утвер­ждений (теорем), в которых можно отчетливо выделить условия (по­сылки) и заключение. А именно, рассматривая знакгического) следования, секвенцию Фо,... , Фп f-утверждение видапосылок Фо,<<Из (истинности)f- как знак (ло­Ф можно понимать как... , Фn(логически)следует высказывание Ф».Правила вывода ИВ, которые будут описаны в следующем пара­графе, отражают (формализуют) некоторые простейшие стандартныелогические способы рассуждения, позволяющие переходить от однихистинных утверждений (теорем) к другим истинным утверждениям(теоремам).Упражнения1.Используя предложение1.2.1,показать, что для любого слова о:алфавита ИВ мы через конечное число шагов сможем определить,является ли о: формулой ИВ или нет.22Гл.1.Исчисление высказыванийЗаменим в определении формулы ИВ п.2.иформулы, то (Ф) А'11 -формулы.('11),(Ф)на следующий: если Ф2V ('11),утверждения, аналогичные предложениям-------t (W)и ·(Ф)-и1.2.11.2.4.Система аксиом и правил вывода§ 1.3.В(Ф)Показать, что при таком определении имеют местодальнейшеммычастобудемиметьделонесконкретнымиформулами и секвенциями, а с так называемыми схемами формул исеквенций.

Буквы Ф,W,Х (буквы Г, д,0),возможно с индексамииз множества натуральных чисел, будем называть переменными дляформул (последовательностей формул). Пусть алфавит В содержиткроме символов алфавита ИВ переменные для формул и последова­тельностей формул.Схемой секвенций (формул) ИВ мы будем называть такое словов алфавите В, что при любых подстановках в это слово вместо пе­ременных для формул и последовательностей формул соответственноконкретных формул и последовательностей конкретных формул полу­чаются конкретные секвенции (формулы) ИВ. Результаты таких под­становок будут называться частными случаями этой схемы.

Например,W,Гf--ФV 1}!и Ф-(Х1 А Х2) будут схемами секвенций и формулсоответственно, аАQo'Q1, 'Qo, '(Q2 - Q1) f--((Q1 -------t 'Q1)АQo) -------tQз(Qз АV (QoА'Q1),'(Q2 V 'Qo))- частными случаями соответствующих схем1).Определение. Схема секвенцийф f--фназывается схемой аксиом ИВ. Частный случай схемы аксиом будемназывать аксиомой.Правилами вывода ИВ являются следующие:Гl.21)f--Ф; Гf-- W'Гf--ФАФ.Гf--Ф'Г,Фf--W7Гf--ФАW·rf--Ф-------tW'8Г.f--f-- Ф -------t Wf-- 1}!'Ф; ГгКогда значения переменных для формул и последовательностей формулв схеме С секвенций (формул) в тексте зафиксированы, схему С будем назы­вать просто секвенцией (формулой).§ 1.3.Система аксиом и правил выводаЗ Гf-Ф/\W.гf-9. г, ·ф f- J'Гf-w23Гфf-Ф,Ф V ф''lO.

Г f- Ф; Г f- ·Фг f- J,г f- ф'5 ·гf-Фvw'll Г,Ф,w,Г1 f-X·г,w,Ф,Г1 f-X'4 · Г f-б Г, Ф.f-Х; Г,w f-- Х;гf-Гf-Ф Vwгf-ф12. Г , w f-- Ф.,хКак отмечалось в конце предыдущего параграфа, правила выво­да ИВ формализуют определенные стандартные логические способырассуждений. Прокомментируем на содержательном уровне, не оченьстрого, правилаПравила1-121-3 -с этой точки зрения.это просто правила, разъясняющие смысл союза tИ»(конъюнкции).Правила4, 5так же относятся к пояснению смысла союза <<или»(дизъюнкции).Правило6формализует способ рассуждения <<разбором (двух) воз­можных случаев,>.

Если при выполнении посылок Г справедливо Фили Х, аw справедливопри выполнении условий Г и Ф, а также привыполнении условий Г и Х, тоw всегдасправедливо при выполне­нии посылок Г. Это устанавливается рассмотрением двух возможныхслучаев (один из которых обязательно выполняется):условия Г и условие Ф,Правило72)1)выполненывыполнены условия Г и условие Х.формализует прием эквивалентной переформулировкитеоремы, позволяющий одно из условий теоремы помещать в ее заклю­чение в виде посылки.Правилоэто одно из логических правил (правило8-rnodus ponensили правило отделения), отмеченных еще Аристотелем; оно указывает,как можно освобождаться от посылки в заключении.Правило9формализуетправилоtрассужденияотпротивного,>.Предположим, что условия Г и ·ф могут одновременно выполнять­ся; приходя к противоречию, выражаемому логической константойJ,заключаем, что из выполнимости условий Г всегда вытекает выполни­мость Ф.Правило10 -это правило <<Обнаружения (выведения) противоре­чия,> для последовательности посылок Г.Правило11носит совершенно технический формальный характер:перестановка посылок не влияет на истинность заключения.Правило12,называемое иногда <,утончением,> или правилом лишнейпосылки, отражает тривиальный факт, что, добавляя к условиям теоре­мы лишнее условие, мы не нарушаем истинности заключения теоремы.Гл.241.Исчисление высказыванийЕсли в правилах вывода в качестве Г и Г1 берутся конкретныепоследовательности формул ИВ, а в качестве Ф,Х'11,-конкретныеформулы, то получаются частные случаи (или применения) правилвывода.

Правиланазываются основными, а правила1-1011-12 -структурными.Еслиприменение правила вывода0 -секвенция, стоящая в епод чертой,стоящих над чертой, по правилуто будем говорить, чтоk,получается из секвенций,k.Определение. Линейным доказательством в ИВ называется ко­нечная последовательность Во,... , Bnсеквенций ИВ, которая удовле­творяет следующему условию: каждая секвенцияется аксиомой, либо получается из некоторыхправил выводап, либо явля­по одному из1-12.Секвенция В называется доказуемой весли существует линейное доказательство Во,Bn =Bi, i:::;;< i,Bj, jИВили теоремой ИВ,...

, Bnв ИВ, у которогоВ. Формула Ф ИВ называется доказуемой в ИВ, если в ИВдоказуема секвенцияПусть Во,Ф.f-... , Bn -линейное доказательство в ИВ. Из определениялегко следует, что для любогоi :::;;п последовательность Во,будет линейным доказательством в ИВ; и если В0 ,доказательство в ив, ТО последовательность Во,... ,В~-... , Biдругое... , Bn, Во, ... , в~ -тоже линейное доказательство в ИВ.Определим индуктивно понятие дерева:Всякая секвенция является деревом.1).2).ЕслиDo, ...

, Dn -деревья и В- секвенция,Do; ... ; Dптов- также дерево1).Одна и та же секвенция может входить в дерево несколько раз. Се­квенцию вместе с ее местом расположения в деревевхождением секвенции в деревоD.Dбудем называтьВхождение секвенции в деревоD,над которым нет горизонтальной черты, будем называть начальнымвВхождение секвенции вD.D,под которым нет горизонтальной чер­ты, будем называть заключительным вслово<<секвенция,>вместо<<вхождениеD.Часто будет употреблятьсясеквенции,>,еслиизконтекстаясно, о каком вхождении идет речь.