1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 26

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 26)

Формулы Ф и \J.Iназываются конгруэнтными {обозначается Ф ,...., \J.I), если существуеттакая последовательность формул Фо, ... , Фп, что Фо = Ф, Фп = \J!,заменой связанной переменной,а Фk+I,k< п,Примересли Фполучается изполучается из Фk заменой связанной переменной.Рассмотрим формулы Ф4.2.5.= Vvз::!v2r( vз, v2).показывает, что ФПредложениеVv2::!vзr( v2, vз) и\J.I=,. ._, \J.I.а). Отношение4.2.6.стью на множестве формул сигнатурыб). Если Ф,....,=Последовательность\J.I,то Ф= \J.I.,.

._,~-является эквивалентно­=Доказательство. а). Из свойства [[1J.11]l]~\J.11 для любой фор­\J.11, для которой выполняются условия на запись [1J.11]l, следует,мулычто если\J.Iполучается из Ф заменой связанной переменной, то Фтакже получается из\J.Iзаменой связанной переменной. Отсюда полу-Гл.1264.Исчисление предикатовчаем симметричность отношения"'отношенияб).="'·Рефлексивность и транзитивностьочевидна.В силу теоремы о замене достаточно показать, что QхФ 1Qу[Ф 1]l,=Q Е {\f, 3}. Но это уже доказано в предложении 4.2.2 ж), з).оКак уже отмечалось, нас будут интересовать формулы в основном<<С точностью>> до эквивалентности, поэтому будут допускаться записивида Ф1 А...А Фn,VФk и др., по которым формулы восстанавли­k~nваются неоднозначно, но при любых расстановках скобок получаютсяэквивалентные формулы.Упражнения1.2.3.Показать, что отношение= является эквивалентностью наДоказать утверждения б), г), е) и з) предложенияF(E).4.2.2.Показать, что для любой формулы Ф и любых переменных х1,....

. . , Xn существует такая формула Ф, что Ф = Ф и {х1, ... , xn} ~~ FV(Ф).§ 4.3.Нормальные формыТак как нас, в основном, будут интересовать формулы «с точно­стью>> до эквивалентности, то полезно выбирать такие подмножестваР ~F(E)формул, устроенных по возможности более просто по сравне­нию с произвольными формулами и чтобы для любой Ф Ествовала Ф ЕР, для которой Ф=F(E)суще­Ф. Некоторые из таких подмножествбудут определены в настоящем параграфе.Будем говорить, что формула Ф сигнатуры Е находится в дизъюнк­тивной нормальной форме (сокращенно д.

н. ф.), если она получаетсяиз формулы Ф исчисления высказываний заменой всех входящих в Фпропозициональных переменных Р1,формулы Ф1,... , Фn... , Pnнанекоторые атомарныесигнатуры Е соответственно.Определение. Будем говорить, что формула Ф сигнатуры Е нахо­дится в пренексной нормальной форме, если она имеет видQ1x1 ... QnxnФ1,гдеQi, iЕ{1, ...

, п}, -кванторы, а Ф1 находится в д. н. ф. Формулу Ф1в этом случае назовем матрицей, а словоQ1x1 ... Qnxn -кванторнойприставкой формулы Ф.Теорема4.3.1.Для любой формулы Ф сигнатуры Е существуетформула Ф сигнатуры Е, находящаяся в пренексной нормальнойформе и эквивалентная Ф.Нормальные формы§ 4.3.127До к аз ат ель ст в о.

В силу предложенияи ~Ф1V Ф2формулы Ф1 ---+ Ф24.2эквивалентны для любых Ф1, Ф2 Е F(Щ. Следовательно,для любой Ф ЕF(~).получить формулу Ф 1применяя несколько раз теорему= Ф,4.2.4,можноне содержащую знака ---+. Индукцией нодлине формулы Ф 1, не содержащей ---+, покажем, что существует Ф2= Ф 1 имеющая видгде ФзФ1=бескванторная формула, и длина Ф2 равна длине Ф1. Если-бескванторная, то в качестве Ф2 берем Ф1.то нужная Ф2существует поЕсли Ф 1предположению индукции=QхФ',и теореме4.2.4. Таким образом, осталось рассмотреть 2 случая: 1) Ф 1 = ~w' и2) Ф1 = (Ф'тФ"), т Е {Л, V}, где Ф' имеет кванторы и находится в видеQoxo ...

QпxnX, где Х - бескванторная формула. (Здесь мы восполь­зовались эквивалентностью (Ф'тФ")= (Ф"тФ') для того, чтобы утвер­= :JхФ4. Случай с другимждать, что Ф' имеет кванторы). Пусть Ф'квантором рассматривается совершенно аналогично. Из предложения4.2.2, а),получаем для случая1)эквивалентность Ф 1= Vх~Ф4.

НужнаяФ2 для случаясуществует тогда по индукционному предположениюи теоремеРассмотрим случай1)4.2.4.входящая в Ф1. Из предложенияФ1= (:Jу[Ф4]lтФ").имеем Ф1Из эквивалентностей в) и д) того же предложения= :Jу([Ф4]~тФ").Требуемая Ф2 найдется теперь по индукци­онному предположению и теоремеДля2). Пусть у - переменная, не4.2.2, з), и теоремы 4.2.4 получаем4.2.4.завершения доказательства теоремынужно для бескванторной Фз найти Ф'= Фз,всилуДля этого заменим все атомарные подформулы Фо,на пропозициональные переменные Ро,... Pnтеоремы4.2.4находящуюся в д.

н. ф.... , Фпформулы Фзсоответственно, получимформулу Х исчисления высказываний. Пусть Х1-формула ИВ, на­ходящаяся в д. н. ф. с теми же переменными, что и Х, для которойХ1 f- Х и Х f- Х1теоремы ИВ. Пусть Ф' получается из Х1 заменой-Ро, ... , Pn на Фо, ... , Фп соответственно, тогда Ф' s Фз, следовательно,по предложению4.2.1Ф'= Фз.Определение. Говорим,Очто формула Ф сигнатуры ~находитсяв приведен.ной нормальной форме, если все ее атомарные подформулыявляются атомными. (См.Предложение4.3.2.§ 3.2 для определения атомной формулы.)Для любой формулы Ф сигнатуры ~ су­ществует формула Ф сигнатуры~.находящаяся в приведен.нойнормальной форме.До к аз ат ель ст в о.В силу теоремы4.2.4достаточно доказатьпредложение для атомарной формулы Ф. Проведем индукцию по числуГл.1284.Исчисление предикатовп(Ф) вхождений сигнатурных символов в Ф.

Если п(Ф) ~атомная формула и доказывать нечего. Если п( Ф)ет вхождение термаt,имеющего вид> 1,f (vi., ... , Vik ).1,то Ф-то в Ф существу­Тогда Ф= (Ф')f,где Ф' получается из Ф заменой этого вхождения на переменную у, невходящую в Ф.Следующие квазивыводы:Ф f--- Ф; f---tt~у~ t,Ф' f--- ФФf---(Ф'/\у~t)У.Ф f--- :3у( Ф'показывают, что ФФ' /\у~/\ у ~ t) '= :3у(Ф' /\у~ t).предположение к Ф' и теоремуЗаметим, что в теоремеtf--- Ф:3у(Ф 1 /\у~t)f---Ф'Теперь применяем индукционное4.2.4.4.3.1Dбез изменения доказательства можнопотребовать, чтобы формула Ч' находилась в приведенной нормальнойформе, если Ф находится в приведенной нормальной форме.

Поэтомуимеет местоСледствиеет формула\J!4.3.3.Для любой формулы Ф сигнатуры ~ существу­сигнатуры~. находящаяся в пренексной приведеннойнормальной форме и эквивалентная Ф.DВ дальнейшем для краткости вместо <<пренексная (приведенная)нормальная форма•> будем писать «пренексная (приведенная) н. ф.•.Упражнения1.Показать, что в теореме4.3.1можно потребовать, чтобы у формулФ и Ч' было одно и то же число вхождений кванторов.2.Показать, что в теореме4.3.1можно потребовать, чтобы формулаЧ' имела вид :3xo\fx1 ... :3xn-l 'v'xn Ф'.3.Проверить, что в теоремебовать, чтобы FV(Ф)§ 4.4.4.3.1и предложении4.3можно потре­= FV(\J!).Теорема о существовании моделиОпределение.

Множество формул Х сигнатуры ~ называется про­тиворечивым или несовместным, если в исчислении предикатов дока­зуема секвенция Г f---J,где все члены Г принадлежат Х. В противномслучае Х называется непротиворечивым или совместным.Отметим некоторые свойства введенного понятия.§ 4.4.Предложениеб). Если ХТеорема о существовании модели129а). Пустое множество непротиворечиво.4.4.1.непротиворечивое множество формул сигнатуры Е-и в исчислении предикатов доказуема секвенция Ф1,...

, Фп f--Ф, гдеФ Е F(Щ, Ф1 Е Х, ... , Фп Е Х, то Х U { Ф} непротиворечиво.в). Если Х U {::3хФ} непротиворечиво, то Х U {[Ф]t} непротиво­речиво при условии, что у не входит свободно в формулы из Х.~г). Если Xn, п Е w, непротиворечивые множества,Xn+I, п Е w, то Х = U Xn непротиворечиво.д). Если ХиXn~iEwнепротиворечивое множество формул сигнату--ры Е, то для любой Ф ЕF(E) либо Х U { Ф }, либо Х U {~Ф} непро­тиворечиво.До к аз ат ель ст в о.Утверждение а) следует из теоремыУтверждение г) очевидно.Еслисеквенция Ф1,ма, то из доказуемости секвенцииФ\J! 1, ... , \J! k,\J.11, ...

,\J.lk,Ф1, ... ,Фn f-- J, так чтоквенция Ф1, ... , Фп, [Ф]t f-- J доказуема вемость... , Фп f-f--Ф1,предложения... , Фп f--4 .1.4,г),иправилуисчислении предикатов и... , Фп f-- \iх~Ф.доказуемость Ф1, ... , Фп f--гда следуетвило10и аксиому 3хФ... , Фп,получаем13\iy~[Ф]t. Тогда из предложениязуемость секвенции Ф1,следует доказу-имеет место б). Если се-у не входит свободно ни в одну из формул Ф1,вилуJ4.1.5.Ф доказуе­то по пра­доказуемость4.2.2, г), следует дока­4.2.2, а), то­Из предложения~3хФ.

Используя теперь пра­f-- 3хФ, получаем, что Ф1, ... , Фп, 3хФ f--Jявляется теоремой исчисления предикатов, откуда получаем в). ЕслиФ1,... , Фп, Ф f-- Jитов, то по правилу\J.11, ... , \J!k,9,~Фf--предложениюказуемость секвенции Ф 1, ... , Фп,J -теоремы исчисления предика­4.1.4,г), и правилу\J! 1, •.• , \J! k f--J,10получаем до­т. е. справедливо д).DПриступим теперь к доказательству одной из важнейших теоремматематической логики.Теорема4.4.2(о существовании модели). Любое непротиворе­чивое множество Х формул сигнатуры Е имеет модель.До к аз ат ель ст в о.В силу теоремы компактностисчитать, что множество Х конечно.

Пусть х1, ... , Xn -входящие свободно в элементы Х(§ 3.3)можновсе переменные,= {\J! 1, ... , \J.I k}. Так как выполни­= {3х1 ... 3хп(Ч'1 Л ... Л \J.lk)},мость Х равносильна выполнимости Х'то можно считать, что Х состоит из одного предложения. Наконец,сигнатуру Е= (R, F, µ)можно считать конечной. (Если Е бесконечна,то нужно взять ограничение Ена множество символов,входящихв формулы из Х.)= {Сп I п Е w} n (R U F) = 0. Пусть Е1Пусть Си Смножество символов, Сп -=/=Ckдля п -=/=kполучается добавлением к Е элементовмножества С в качестве символов новых констант.

Характеристики

Список файлов книги